EulerForm.Basic — BridgelandStability Comparator Manual

7. EulerForm.Basic🔗

Module BridgelandStability.EulerForm.Basic — 10 declarations (Theorem, Definition, Structure)

7.1. `CategoryTheory.Triangulated.eulerFormObj_contravariant_triangleAdditive`🔗

Theorem | BridgelandStability.EulerForm.Basic | Source | Open Issue

theorem eulerFormObj_contravariant_triangleAdditive (E : C) :
    IsTriangleAdditive (fun F ↦ eulerFormObj k C E F)

Show proof

where
  additive := fun T hT ↦ byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
    simp only [eulerFormObj]k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    let F : C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    letI : F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤ⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    letI : F.IsHomological := linearCoyonedaObjIsHomological (k := k) (C := C) Ek:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    let δ_lin : (n : ℤ) → ((E ⟶ T.obj₃⟦n⟧) →ₗ[k] (E ⟶ T.obj₁⟦(n + 1)⟧)) := fun n ↦
      Linear.rightComp k E (T.mor₃⟦n⟧' ≫
        (shiftFunctorAdd' C 1 n (n + 1) (byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···n:ℤ⊢ 1 + n = n + 1 liaAll goals completed! 🐙)).inv.app T.obj₁)
    let r : ℤ → ℤ := fun n ↦ Module.finrank k (LinearMap.range (δ_lin n))k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    have hδ_eq : ∀ n : ℤ, ((F.homologySequenceδ T n (n + 1) rfl).hom) = δ_lin n := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
      intro nk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)n:ℤ⊢ ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin n
      ext xhk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)n:ℤx:↑((F.shift n).obj T.obj₃)⊢ (ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯)) x = (δ_lin n) x
      simpa [F, δ_lin] using
        (CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply
          (C := C) (T := T) (n₀ := n) (n₁ := n + 1) (h := rfl) (A := Opposite.op E) x)All goals completed! 🐙
    have h_ker_f_aux : ∀ m : ℤ,
        Module.finrank k (LinearMap.ker (((F.shift (m + 1)).map T.mor₁).hom)) = r m := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
      intro mk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nm:ℤ⊢ ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r m
      let f_succ : (E ⟶ T.obj₁⟦m + 1⟧) →ₗ[k] (E ⟶ T.obj₂⟦m + 1⟧) :=
        ((F.shift (m + 1)).map T.mor₁).homk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nm:ℤf_succ:(E ⟶ (shiftFunctor C (m + 1)).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C (m + 1)).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)⊢ ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r m
      have h_exact₁ : LinearMap.range (δ_lin m) = LinearMap.ker f_succ := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        simpa [f_succ, hδ_eq m] using
          (ShortComplex.Exact.moduleCat_range_eq_ker
            (F.homologySequence_exact₁ T hT m (m + 1) rfl))All goals completed! 🐙
      simpa [r] using
        congrArg (fun V : Submodule k (E ⟶ T.obj₁⟦m + 1⟧) => Module.finrank k V) h_exact₁.symmAll goals completed! 🐙
    have hrank : ∀ n : ℤ,
        (Module.finrank k (E ⟶ T.obj₂⟦n⟧) : ℤ) =
        Module.finrank k (E ⟶ T.obj₁⟦n⟧) + Module.finrank k (E ⟶ T.obj₃⟦n⟧) -
          r (n - 1) - r n := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
      intro nk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤ⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      let f_n : (E ⟶ T.obj₁⟦n⟧) →ₗ[k] (E ⟶ T.obj₂⟦n⟧) := ((F.shift n).map T.mor₁).homk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      let g_n : (E ⟶ T.obj₂⟦n⟧) →ₗ[k] (E ⟶ T.obj₃⟦n⟧) := ((F.shift n).map T.mor₂).homk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      have hexact_B : LinearMap.range f_n = LinearMap.ker g_n := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        simpa [f_n, g_n, F] using
          (ShortComplex.Exact.moduleCat_range_eq_ker
            (F.homologySequence_exact₂ T hT n))All goals completed! 🐙
      haveI : Module.Finite k (E ⟶ T.obj₂⟦n⟧) := IsFiniteType.finite_dim (k := k) E (T.obj₂⟦n⟧)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝¹:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      have h_mid := finrank_mid_of_exact k f_n g_n hexact_Bk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝¹:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      haveI : Module.Finite k (E ⟶ T.obj₁⟦n⟧) := IsFiniteType.finite_dim (k := k) E (T.obj₁⟦n⟧)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝²:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝¹:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      haveI : Module.Finite k (E ⟶ T.obj₃⟦n⟧) := IsFiniteType.finite_dim (k := k) E (T.obj₃⟦n⟧)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      have h_ker_f : Module.finrank k (LinearMap.ker f_n) = r (n - 1) := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        change Module.finrank k (LinearMap.ker (((F.shift n).map T.mor₁).hom)) = r (n - 1)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)⊢ ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift n).map T.mor₁)).ker) = r (n - 1)
        have hn : n = (n - 1) + 1 := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃ liaAll goals completed! 🐙
        rw [hn]k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)hn:n = n - 1 + 1⊢ ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (n - 1 + 1)).map T.mor₁)).ker) = r (n - 1 + 1 - 1)
        simpa using h_ker_f_aux (n - 1)All goals completed! 🐙
      have h_ker_δ : Module.finrank k (LinearMap.ker (δ_lin n)) =
          Module.finrank k (LinearMap.range g_n) := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        have h_exact₃ : LinearMap.range g_n = LinearMap.ker (δ_lin n) := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
          simpa [g_n, hδ_eq n] using
            (ShortComplex.Exact.moduleCat_range_eq_ker
              (F.homologySequence_exact₃ T hT n (n + 1) rfl))All goals completed! 🐙
        simpa using
          congrArg (fun V : Submodule k (E ⟶ T.obj₃⟦n⟧) => Module.finrank k V) h_exact₃.symmAll goals completed! 🐙
      have h_f : (Module.finrank k (LinearMap.range f_n) : ℤ) =
          Module.finrank k (E ⟶ T.obj₁⟦n⟧) - r (n - 1) := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        have := f_n.finrank_range_add_finrank_kerk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝⁴:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝³:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝²:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)h_ker_δ:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.rangethis:Module.finrank k ↥f_n.range + Module.finrank k ↥f_n.ker = Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)⊢ ↑(Module.finrank k ↥f_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) - r (n - 1)
        liaAll goals completed! 🐙
      have h_g : (Module.finrank k (LinearMap.range g_n) : ℤ) =
          Module.finrank k (E ⟶ T.obj₃⟦n⟧) - r n := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        have h1 := (δ_lin n).finrank_range_add_finrank_kerk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)h_ker_δ:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.rangeh_f:↑(Module.finrank k ↥f_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) - r (n - 1)h1:Module.finrank k ↥(δ_lin n).range + Module.finrank k ↥(δ_lin n).ker =
  Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)⊢ ↑(Module.finrank k ↥g_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) - r n
        have h2 := h_ker_δk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)h_ker_δ:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.rangeh_f:↑(Module.finrank k ↥f_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) - r (n - 1)h1:Module.finrank k ↥(δ_lin n).range + Module.finrank k ↥(δ_lin n).ker =
  Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)h2:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.range⊢ ↑(Module.finrank k ↥g_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) - r n
        simp only [r] at h2 ⊢k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)h_ker_δ:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.rangeh_f:↑(Module.finrank k ↥f_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) - r (n - 1)h1:Module.finrank k ↥(δ_lin n).range + Module.finrank k ↥(δ_lin n).ker =
  Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)h2:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.range⊢ ↑(Module.finrank k ↥g_n.range) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) - ↑(Module.finrank k ↥(δ_lin n).range)
        liaAll goals completed! 🐙
      linarithAll goals completed! 🐙
    have hr : (Function.support r).Finite := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
      refine Set.Finite.subset
        ((IsFiniteType.finite_support (k := k) E T.obj₁).image fun m : ℤ ↦ m - 1) ?_k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r n⊢ Function.support r ⊆ (fun m => m - 1) '' {n | Nontrivial (E ⟶ (shiftFunctor C n).obj T.obj₁)}
      intro n hnk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support r⊢ n ∈ (fun m => m - 1) '' {n | Nontrivial (E ⟶ (shiftFunctor C n).obj T.obj₁)}
      have hnonzero : (r n : ℤ) ≠ 0 := hnk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0⊢ n ∈ (fun m => m - 1) '' {n | Nontrivial (E ⟶ (shiftFunctor C n).obj T.obj₁)}
      have hnontrivial : Nontrivial (E ⟶ T.obj₁⟦n + 1⟧) := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        by_contra htrivk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0htriv:¬Nontrivial (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)⊢ False
        haveI : Subsingleton (E ⟶ T.obj₁⟦n + 1⟧) := not_nontrivial_iff_subsingleton.mp htrivk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝¹:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0htriv:¬Nontrivial (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)this:Subsingleton (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)⊢ False
        have hδ : δ_lin n = 0 := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
          ext xhk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝¹:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0htriv:¬Nontrivial (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)this:Subsingleton (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)x:E ⟶ (shiftFunctor C n).obj T.obj₃⊢ (δ_lin n) x = 0 x
          exact Subsingleton.elim _ _All goals completed! 🐙
        apply hnonzerok:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝¹:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0htriv:¬Nontrivial (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)this:Subsingleton (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)hδ:δ_lin n = 0⊢ r n = 0
        simp [r]All goals completed! 🐙
      exact ⟨n + 1, hnontrivial, byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0hnontrivial:Nontrivial (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)⊢ (fun m => m - 1) (n + 1) = n simpAll goals completed! 🐙⟩
    exact eulerSum_of_rank_identity (k := k) (C := C) E
      (a := fun n ↦ T.obj₁⟦n⟧)
      (b := fun n ↦ T.obj₂⟦n⟧)
      (c := fun n ↦ T.obj₃⟦n⟧)
      (r := r)
      hrank
      (byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nhr:(Function.support r).Finite⊢ {n | Nontrivial (E ⟶ (fun n => (shiftFunctor C n).obj T.obj₁) n)}.Finite simpa using IsFiniteType.finite_support (k := k) E T.obj₁All goals completed! 🐙)
      (byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nhr:(Function.support r).Finite⊢ {n | Nontrivial (E ⟶ (fun n => (shiftFunctor C n).obj T.obj₂) n)}.Finite simpa using IsFiniteType.finite_support (k := k) E T.obj₂All goals completed! 🐙)
      (byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nhr:(Function.support r).Finite⊢ {n | Nontrivial (E ⟶ (fun n => (shiftFunctor C n).obj T.obj₃) n)}.Finite simpa using IsFiniteType.finite_support (k := k) E T.obj₃All goals completed! 🐙)
      hr

7.2. `CategoryTheory.Triangulated.eulerFormInner`🔗

Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue

/-- For fixed `E`, lift `F ↦ χ(E, F)` to a group homomorphism `K₀ C →+ ℤ`
using the universal property of `K₀`. -/
def eulerFormInner (E : C) : K₀ C →+ ℤ := byk:Type winst✝⁹:Field kC:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:IsTriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:C⊢ K₀ C →+ ℤ
  letI := eulerFormObj_contravariant_triangleAdditive (k := k) (C := C) Ek:Type winst✝⁹:Field kC:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:IsTriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:Cthis:IsTriangleAdditive fun F => eulerFormObj k C E F := ···⊢ K₀ C →+ ℤ
  exact K₀.lift C (fun F ↦ eulerFormObj k C E F)All goals completed! 🐙

7.3. `CategoryTheory.Triangulated.eulerFormInner_isTriangleAdditive`🔗

Theorem | BridgelandStability.EulerForm.Basic | Source | Open Issue

/-- The outer function `E ↦ eulerFormInner E` is triangle-additive, so the Euler
form descends to a bilinear form on `K₀`. -/
instance eulerFormInner_isTriangleAdditive
    [(shiftFunctor C (1 : ℤ)).Linear k] :
    IsTriangleAdditive (eulerFormInner k C)

Show proof

where
  additive T hT := byk:Type winst✝¹⁰:Field kC:Type uinst✝⁹:Category.{v, u} Cinst✝⁸:HasZeroObject Cinst✝⁷:HasShift C ℤinst✝⁶:Preadditive Cinst✝⁵:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝⁴:Pretriangulated Cinst✝³:IsTriangulated Cinst✝²:Linear k Cinst✝¹:IsFiniteType k Cinst✝:Functor.Linear k (shiftFunctor C 1)T:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormInner k C T.obj₂ = eulerFormInner k C T.obj₁ + eulerFormInner k C T.obj₃
    apply K₀.hom_exthk:Type winst✝¹⁰:Field kC:Type uinst✝⁹:Category.{v, u} Cinst✝⁸:HasZeroObject Cinst✝⁷:HasShift C ℤinst✝⁶:Preadditive Cinst✝⁵:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝⁴:Pretriangulated Cinst✝³:IsTriangulated Cinst✝²:Linear k Cinst✝¹:IsFiniteType k Cinst✝:Functor.Linear k (shiftFunctor C 1)T:Triangle ChT:T ∈ distinguishedTriangles⊢ ∀ (X : C), (eulerFormInner k C T.obj₂) (K₀.of C X) = (eulerFormInner k C T.obj₁ + eulerFormInner k C T.obj₃) (K₀.of C X); intro Fhk:Type winst✝¹⁰:Field kC:Type uinst✝⁹:Category.{v, u} Cinst✝⁸:HasZeroObject Cinst✝⁷:HasShift C ℤinst✝⁶:Preadditive Cinst✝⁵:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝⁴:Pretriangulated Cinst✝³:IsTriangulated Cinst✝²:Linear k Cinst✝¹:IsFiniteType k Cinst✝:Functor.Linear k (shiftFunctor C 1)T:Triangle ChT:T ∈ distinguishedTrianglesF:C⊢ (eulerFormInner k C T.obj₂) (K₀.of C F) = (eulerFormInner k C T.obj₁ + eulerFormInner k C T.obj₃) (K₀.of C F)
    simp only [AddMonoidHom.add_apply, eulerFormInner, K₀.lift_of]hk:Type winst✝¹⁰:Field kC:Type uinst✝⁹:Category.{v, u} Cinst✝⁸:HasZeroObject Cinst✝⁷:HasShift C ℤinst✝⁶:Preadditive Cinst✝⁵:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝⁴:Pretriangulated Cinst✝³:IsTriangulated Cinst✝²:Linear k Cinst✝¹:IsFiniteType k Cinst✝:Functor.Linear k (shiftFunctor C 1)T:Triangle ChT:T ∈ distinguishedTrianglesF:C⊢ eulerFormObj k C T.obj₂ F = eulerFormObj k C T.obj₁ F + eulerFormObj k C T.obj₃ F
    letI := eulerFormObj_covariant_triangleAdditive (k := k) (C := C) Fhk:Type winst✝¹⁰:Field kC:Type uinst✝⁹:Category.{v, u} Cinst✝⁸:HasZeroObject Cinst✝⁷:HasShift C ℤinst✝⁶:Preadditive Cinst✝⁵:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝⁴:Pretriangulated Cinst✝³:IsTriangulated Cinst✝²:Linear k Cinst✝¹:IsFiniteType k Cinst✝:Functor.Linear k (shiftFunctor C 1)T:Triangle ChT:T ∈ distinguishedTrianglesF:Cthis:IsTriangleAdditive fun E => eulerFormObj k C E F := ···⊢ eulerFormObj k C T.obj₂ F = eulerFormObj k C T.obj₁ F + eulerFormObj k C T.obj₃ F
    exact IsTriangleAdditive.additive (f := fun E ↦ eulerFormObj k C E F) T hTAll goals completed! 🐙

7.4. `CategoryTheory.Triangulated.eulerForm`🔗

Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue

/-- The Euler form on `K₀`, obtained by applying the universal property of `K₀`
twice to `eulerFormObj`. -/
def eulerForm [(shiftFunctor C (1 : ℤ)).Linear k] :
    K₀ C →+ K₀ C →+ ℤ :=
  K₀.lift C (eulerFormInner k C)

7.5. `CategoryTheory.Triangulated.eulerFormRad`🔗

Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue

/-- The left radical of the Euler form on `K₀ C`. -/
def eulerFormRad [Linear k C] [IsFiniteType k C] [(shiftFunctor C (1 : ℤ)).Linear k] :
    AddSubgroup (K₀ C) :=
  (eulerForm k C).ker

7.6. `CategoryTheory.Triangulated.NumericalK₀`🔗

Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue

/-- The numerical Grothendieck group attached to the Euler form on `K₀`. -/
def NumericalK₀ [Linear k C] [IsFiniteType k C] [(shiftFunctor C (1 : ℤ)).Linear k] :
    Type _ :=
  K₀ C ⧸ eulerFormRad k C

7.7. `CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup`🔗

Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue

/-- The `AddCommGroup` instance on `NumericalK₀ k C`. -/
instance NumericalK₀.instAddCommGroup [Linear k C] [IsFiniteType k C]
    [(shiftFunctor C (1 : ℤ)).Linear k] :
    AddCommGroup (NumericalK₀ k C) :=
  inferInstanceAs (AddCommGroup (K₀ C ⧸ eulerFormRad k C))

7.8. `CategoryTheory.Triangulated.numericalQuotientMap`🔗

Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue

/-- The quotient map `K₀(C) → N(C)`. -/
abbrev numericalQuotientMap [Linear k C] [IsFiniteType k C]
    [(shiftFunctor C (1 : ℤ)).Linear k] :
    K₀ C →+ NumericalK₀ k C :=
  QuotientAddGroup.mk' (eulerFormRad k C)

7.9. `CategoryTheory.Triangulated.NumericallyFinite`🔗

Structure | BridgelandStability.EulerForm.Basic | Source | Open Issue

/-- The category `C` is numerically finite if the numerical Grothendieck group attached to the
Euler form is finitely generated as an abelian group. -/
class NumericallyFinite [Linear k C] [IsFiniteType k C]
    [(shiftFunctor C (1 : ℤ)).Linear k] : Prop where
  /-- The Euler-form numerical Grothendieck group is finitely generated. -/
  fg : AddGroup.FG (NumericalK₀ k C)

7.10. `CategoryTheory.Triangulated.NumericalComponent`🔗

Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue

/-- A connected component of numerical stability conditions. -/
abbrev NumericalComponent [Linear k C] [IsFiniteType k C]
    [(shiftFunctor C (1 : ℤ)).Linear k]
    (cc : StabilityCondition.WithClassMap.ComponentIndex C (numericalQuotientMap k C)) :=
  StabilityCondition.WithClassMap.Component C (numericalQuotientMap k C) cc

7. EulerForm.Basic🔗

7.1. CategoryTheory.Triangulated.eulerFormObj_contravariant_triangleAdditive🔗

7.2. CategoryTheory.Triangulated.eulerFormInner🔗

7.3. CategoryTheory.Triangulated.eulerFormInner_isTriangleAdditive🔗

7.4. CategoryTheory.Triangulated.eulerForm🔗

7.5. CategoryTheory.Triangulated.eulerFormRad🔗

7.6. CategoryTheory.Triangulated.NumericalK₀🔗

7.7. CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup🔗

7.8. CategoryTheory.Triangulated.numericalQuotientMap🔗

7.9. CategoryTheory.Triangulated.NumericallyFinite🔗

7.10. CategoryTheory.Triangulated.NumericalComponent🔗

7.1. `CategoryTheory.Triangulated.eulerFormObj_contravariant_triangleAdditive`🔗

7.2. `CategoryTheory.Triangulated.eulerFormInner`🔗

7.3. `CategoryTheory.Triangulated.eulerFormInner_isTriangleAdditive`🔗

7.4. `CategoryTheory.Triangulated.eulerForm`🔗

7.5. `CategoryTheory.Triangulated.eulerFormRad`🔗

7.6. `CategoryTheory.Triangulated.NumericalK₀`🔗

7.7. `CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup`🔗

7.8. `CategoryTheory.Triangulated.numericalQuotientMap`🔗

7.9. `CategoryTheory.Triangulated.NumericallyFinite`🔗

7.10. `CategoryTheory.Triangulated.NumericalComponent`🔗