Bridgeland Stability Conditions

12.5. HeartEquivalence: H0Functor🔗

12.5.1. heartCoh🔗

The degree-n heart cohomology object H^n_t(E), realized as the pure truncation \tau^{[n,n]} E shifted into the heart.

Construction: Defined as \texttt{heartShiftOfPure} applied to (\tau^{\ge n} \circ \tau^{\le n})(E) with shift index n.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartCoh.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) (n : ℤ)
  (E : C) : h.t.heart.FullSubcategory
CategoryTheory.Triangulated.HeartStabilityData.heartCoh.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (n : ℤ) (E : C) :
  h.t.heart.FullSubcategory

Something wrong, better idea? Suggest a change

12.5.2. heartCohFunctor🔗

The degree-n heart cohomology assembled into a functor \mathcal{C} \to \operatorname{heart}(t).

Construction: Lifts the composite \tau^{[n,n]} \circ [-n] to the heart full subcategory via \texttt{ObjectProperty.lift}, verifying that each output satisfies both the \le 0 and \ge 0 bounds of the heart.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.heartCohFunctor.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) (n : ℤ) :
  CategoryTheory.Functor C h.t.heart.FullSubcategory
CategoryTheory.Triangulated.HeartStabilityData.heartCohFunctor.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (n : ℤ) :
  CategoryTheory.Functor C
    h.t.heart.FullSubcategory

Something wrong, better idea? Suggest a change

12.5.3. heartCohFunctor_additive🔗

The heart cohomology functor H^n_t is additive.

Proof: Follows from additivity of the truncation functors and the shift functor.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartCohFunctor_additive.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) (n : ℤ) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartCohFunctor C h
      n).Additive
CategoryTheory.Triangulated.HeartStabilityData.heartCohFunctor_additive.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (n : ℤ) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartCohFunctor
      C h n).Additive

Something wrong, better idea? Suggest a change

12.5.4. heartCohFunctor_obj🔗

H^n_t(E) = \texttt{heartCoh}(n, E) as objects.

Proof: True by definition.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.heartCohFunctor_obj.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) (n : ℤ)
  (E : C) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartCohFunctor C h
          n).obj
      E =
    CategoryTheory.Triangulated.HeartStabilityData.heartCoh C h n E
CategoryTheory.Triangulated.HeartStabilityData.heartCohFunctor_obj.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (n : ℤ) (E : C) :
  (CategoryTheory.Triangulated.HeartStabilityData.heartCohFunctor
          C h n).obj
      E =
    CategoryTheory.Triangulated.HeartStabilityData.heartCoh
      C h n E

Something wrong, better idea? Suggest a change

12.5.5. H0Functor🔗

Degree-zero heart cohomology H^0_t : \mathcal{C} \to \operatorname{heart}(t).

Construction: An abbreviation: \texttt{heartCohFunctor} at index n = 0.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.H0Functor.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) :
  CategoryTheory.Functor C h.t.heart.FullSubcategory
CategoryTheory.Triangulated.HeartStabilityData.H0Functor.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C) :
  CategoryTheory.Functor C
    h.t.heart.FullSubcategory

Something wrong, better idea? Suggest a change

12.5.6. H0Functor_additive🔗

The H^0_t functor is additive.

Proof: Inherits from \texttt{heartCohFunctor\_additive} at n = 0.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_additive.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
      h).Additive
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_additive.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor
      C h).Additive

Something wrong, better idea? Suggest a change

12.5.7. H0Functor_shiftSequence🔗

The tautological shift-sequence structure on H^0_t, used to compare the generic homological-functor API with the explicit \texttt{heartCoh} objects.

Proof: Applies \texttt{Functor.ShiftSequence.tautological}.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_shiftSequence.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
        h).ShiftSequence
    ℤ
CategoryTheory.Triangulated.HeartStabilityData.H0Functor_shiftSequence.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor
        C h).ShiftSequence
    ℤ

Something wrong, better idea? Suggest a change

12.5.8. H0prime🔗

The degree-zero cohomology object in the alternative normal form \tau^{\le 0}(\tau^{\ge 0} X).

Construction: Packages (\tau^{\le 0} \circ \tau^{\ge 0})(X) as a heart object, with the heart membership proof assembled from the truncation bounds.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.H0prime.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) (X : C) :
  h.t.heart.FullSubcategory
CategoryTheory.Triangulated.HeartStabilityData.H0prime.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (X : C) : h.t.heart.FullSubcategory

Something wrong, better idea? Suggest a change

12.5.9. H0primeFunctor🔗

The alternative H^0 in the normal form \tau^{\le 0} \circ \tau^{\ge 0}, assembled as a functor \mathcal{C} \to \operatorname{heart}(t).

Construction: Object map: \texttt{H0prime}. Morphism map: the composite truncation applied to f, wrapped in \texttt{ObjectProperty.homMk}.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) :
  CategoryTheory.Functor C h.t.heart.FullSubcategory
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C) :
  CategoryTheory.Functor C
    h.t.heart.FullSubcategory

Something wrong, better idea? Suggest a change

12.5.10. H0primeFunctor_additive🔗

The H^0{}' functor is additive.

Proof: Follows from additivity of the two truncation functors.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_additive.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
      h).Additive
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_additive.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
      C h).Additive

Something wrong, better idea? Suggest a change

12.5.11. H0ObjIsoH0prime🔗

The two standard normal forms \tau^{\ge 0}(\tau^{\le 0} X) and \tau^{\le 0}(\tau^{\ge 0} X) for H^0(X) are canonically isomorphic.

Construction: Constructed via the shift-by-zero isomorphism composed with the canonical comparison \texttt{truncGELEIsoLEGE}.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) (X : C) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor C h).obj X ≅
    CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X
CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (X : C) :
  (CategoryTheory.Triangulated.HeartStabilityData.H0Functor
          C h).obj
      X ≅
    CategoryTheory.Triangulated.HeartStabilityData.H0prime
      C h X

Something wrong, better idea? Suggest a change

12.5.12. H0ObjIsoH0prime_hom_naturality🔗

The isomorphism H^0(X) \cong H^0{}'(X) is natural in X.

Proof: Verified by checking that both paths around the naturality square agree after composing with the faithful truncation inclusion.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime_hom_naturality.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) {X Y : C}
  (f : X ⟶ Y) :
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
            h).map
        f)
      (CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime C
          h Y).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime C
          h X).hom
      (CategoryTheory.ObjectProperty.homMk ((h.t.truncLEGE 0 0).map f))
CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime_hom_naturality.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {X Y : C} (f : X ⟶ Y) :
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
            C h).map
        f)
      (CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime
          C h Y).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime
          C h X).hom
      (CategoryTheory.ObjectProperty.homMk
        ((h.t.truncLEGE 0 0).map f))

Something wrong, better idea? Suggest a change

12.5.13. H0ObjIsoH0prime_hom_naturality_assoc🔗

Associativity-reassociated form of the naturality of the isomorphism H^0(X) \cong H^0{}'(X).

Proof: Obtained by \texttt{reassoc} from \texttt{H0ObjIsoH0prime\_hom\_naturality}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime_hom_naturality_assoc.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) {X Y : C}
  (f : X ⟶ Y) {Z : h.t.heart.FullSubcategory}
  (h✝ :
    CategoryTheory.Triangulated.HeartStabilityData.H0prime C h Y ⟶ Z) :
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Triangulated.HeartStabilityData.H0Functor C
            h).map
        f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime
            C h Y).hom
        h✝) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime C
          h X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ObjectProperty.homMk
          ((h.t.truncLE 0).map ((h.t.truncGE 0).map f)))
        h✝)
CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime_hom_naturality_assoc.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {X Y : C} (f : X ⟶ Y)
  {Z : h.t.heart.FullSubcategory}
  (h✝ :
    CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h Y ⟶
      Z) :
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Triangulated.HeartStabilityData.H0Functor
            C h).map
        f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime
            C h Y).hom
        h✝) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0ObjIsoH0prime
          C h X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ObjectProperty.homMk
          ((h.t.truncLE 0).map
            ((h.t.truncGE 0).map f)))
        h✝)

Something wrong, better idea? Suggest a change

12.5.14. H0FunctorIsoH0primeFunctor🔗

The normal forms \tau^{\ge 0} \circ \tau^{\le 0} and \tau^{\le 0} \circ \tau^{\ge 0} assemble into a natural isomorphism of functors \mathcal{C} \to \operatorname{heart}(t).

Construction: Built from \texttt{H0ObjIsoH0prime} as components, with naturality from \texttt{H0ObjIsoH0prime\_hom\_naturality}.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.H0FunctorIsoH0primeFunctor.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) :
  CategoryTheory.Triangulated.HeartStabilityData.H0Functor C h ≅
    CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C h
CategoryTheory.Triangulated.HeartStabilityData.H0FunctorIsoH0primeFunctor.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C) :
  CategoryTheory.Triangulated.HeartStabilityData.H0Functor
      C h ≅
    CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
      C h

Something wrong, better idea? Suggest a change

12.5.15. truncGE_map_comp_descTruncGE🔗

Composition of \tau^{\ge n}(g) with the descent map \texttt{descTruncGE}(f) equals \texttt{descTruncGE}(g \circ f).

Proof: Both sides lift to the same morphism after composing with the truncation projection, so they agree by the universal property of \tau^{\ge n}.

🔗theorem
CategoryTheory.Triangulated.TStructure.truncGE_map_comp_descTruncGE.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y Z : C} (g : X ⟶ Y)
  (f : Y ⟶ Z) (n : ℤ) [t.IsGE Z n] :
  CategoryTheory.CategoryStruct.comp ((t.truncGE n).map g)
      (t.descTruncGE f n) =
    t.descTruncGE (CategoryTheory.CategoryStruct.comp g f) n
CategoryTheory.Triangulated.TStructure.truncGE_map_comp_descTruncGE.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  {X Y Z : C} (g : X ⟶ Y) (f : Y ⟶ Z)
  (n : ℤ) [t.IsGE Z n] :
  CategoryTheory.CategoryStruct.comp
      ((t.truncGE n).map g)
      (t.descTruncGE f n) =
    t.descTruncGE
      (CategoryTheory.CategoryStruct.comp
        g f)
      n

Something wrong, better idea? Suggest a change

12.5.16. truncGE_map_comp_descTruncGE_assoc🔗

Associativity-reassociated form of \texttt{truncGE\_map\_comp\_descTruncGE}.

Proof: Obtained by \texttt{reassoc} from the non-assoc version.

🔗theorem
CategoryTheory.Triangulated.TStructure.truncGE_map_comp_descTruncGE_assoc.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y Z : C} (g : X ⟶ Y)
  (f : Y ⟶ Z) (n : ℤ) [t.IsGE Z n] {Z✝ : C} (h : Z ⟶ Z✝) :
  CategoryTheory.CategoryStruct.comp ((t.truncGE n).map g)
      (CategoryTheory.CategoryStruct.comp (t.descTruncGE f n) h) =
    CategoryTheory.CategoryStruct.comp
      (t.descTruncGE (CategoryTheory.CategoryStruct.comp g f) n) h
CategoryTheory.Triangulated.TStructure.truncGE_map_comp_descTruncGE_assoc.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  {X Y Z : C} (g : X ⟶ Y) (f : Y ⟶ Z)
  (n : ℤ) [t.IsGE Z n] {Z✝ : C}
  (h : Z ⟶ Z✝) :
  CategoryTheory.CategoryStruct.comp
      ((t.truncGE n).map g)
      (CategoryTheory.CategoryStruct.comp
        (t.descTruncGE f n) h) =
    CategoryTheory.CategoryStruct.comp
      (t.descTruncGE
        (CategoryTheory.CategoryStruct.comp
          g f)
        n)
      h

Something wrong, better idea? Suggest a change

12.5.17. descTruncGE_zero🔗

The descent of the zero morphism through \tau^{\ge n} is zero.

Proof: Follows from the universal property: the zero morphism composed with the projection is zero.

🔗theorem
CategoryTheory.Triangulated.TStructure.descTruncGE_zero.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (n : ℤ)
  [t.IsGE Y n] : t.descTruncGE 0 n = 0
CategoryTheory.Triangulated.TStructure.descTruncGE_zero.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  {X Y : C} (n : ℤ) [t.IsGE Y n] :
  t.descTruncGE 0 n = 0

Something wrong, better idea? Suggest a change

12.5.18. descTruncGE_add🔗

The descent map \texttt{descTruncGE} is additive.

Proof: Follows from uniqueness of the lift and additivity of composition.

🔗theorem
CategoryTheory.Triangulated.TStructure.descTruncGE_add.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f g : X ⟶ Y)
  (n : ℤ) [t.IsGE Y n] :
  t.descTruncGE (f + g) n = t.descTruncGE f n + t.descTruncGE g n
CategoryTheory.Triangulated.TStructure.descTruncGE_add.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (t :
    CategoryTheory.Triangulated.TStructure
      C)
  {X Y : C} (f g : X ⟶ Y) (n : ℤ)
  [t.IsGE Y n] :
  t.descTruncGE (f + g) n =
    t.descTruncGE f n + t.descTruncGE g n

Something wrong, better idea? Suggest a change

12.5.19. toH0primeHom🔗

A morphism f : E_{\mathrm{obj}} \to X from a heart object factors canonically through H^0{}'(X) = \tau^{\le 0}(\tau^{\ge 0} X).

Construction: Lifts f \circ \pi_{\ge 0} through the truncation-\le 0 inclusion using the \texttt{liftTruncLE} universal property.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} (f : E.obj ⟶ X) :
  E ⟶ CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  (f : E.obj ⟶ X) :
  E ⟶
    CategoryTheory.Triangulated.HeartStabilityData.H0prime
      C h X

Something wrong, better idea? Suggest a change

12.5.20. toH0primeHom_hom🔗

The underlying morphism of the canonical lift satisfies \beta \circ \iota_{\le 0} = f \circ \pi_{\ge 0}.

Proof: Immediate from the lifting construction.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_hom.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} (f : E.obj ⟶ X) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E
          f).hom
      ((h.t.truncLEι 0).app ((h.t.truncGE 0).obj X)) =
    CategoryTheory.CategoryStruct.comp f ((h.t.truncGEπ 0).app X)
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_hom.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  (f : E.obj ⟶ X) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
          C h E f).hom
      ((h.t.truncLEι 0).app
        ((h.t.truncGE 0).obj X)) =
    CategoryTheory.CategoryStruct.comp f
      ((h.t.truncGEπ 0).app X)

Something wrong, better idea? Suggest a change

12.5.21. toH0primeHom_hom_assoc🔗

Associativity-reassociated form of \texttt{toH0primeHom\_hom}.

Proof: Obtained by \texttt{reassoc} from the non-assoc version.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_hom_assoc.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} (f : E.obj ⟶ X) {Z : C}
  (h✝ : (h.t.truncGE 0).obj X ⟶ Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E
          f).hom
      (CategoryTheory.CategoryStruct.comp
        ((h.t.truncLEι 0).app ((h.t.truncGE 0).obj X)) h✝) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp ((h.t.truncGEπ 0).app X) h✝)
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_hom_assoc.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  (f : E.obj ⟶ X) {Z : C}
  (h✝ : (h.t.truncGE 0).obj X ⟶ Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
          C h E f).hom
      (CategoryTheory.CategoryStruct.comp
        ((h.t.truncLEι 0).app
          ((h.t.truncGE 0).obj X))
        h✝) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp
        ((h.t.truncGEπ 0).app X) h✝)

Something wrong, better idea? Suggest a change

12.5.22. hom_ext_toH0prime🔗

Two morphisms into H^0{}'(X) from a heart object are equal if they agree after composing with the truncation inclusion \iota_{\le 0}.

Proof: Uses the universal property of \tau^{\le 0}: the inclusion is a monomorphism on morphisms from objects in \mathcal{C}^{\le 0}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.hom_ext_toH0prime.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C}
  {β₁ β₂ :
    E ⟶ CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X}
  (hβ :
    CategoryTheory.CategoryStruct.comp β₁.hom
        ((h.t.truncLEι 0).app ((h.t.truncGE 0).obj X)) =
      CategoryTheory.CategoryStruct.comp β₂.hom
        ((h.t.truncLEι 0).app ((h.t.truncGE 0).obj X))) :
  β₁ = β₂
CategoryTheory.Triangulated.HeartStabilityData.hom_ext_toH0prime.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  {β₁ β₂ :
    E ⟶
      CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h X}
  (hβ :
    CategoryTheory.CategoryStruct.comp
        β₁.hom
        ((h.t.truncLEι 0).app
          ((h.t.truncGE 0).obj X)) =
      CategoryTheory.CategoryStruct.comp
        β₂.hom
        ((h.t.truncLEι 0).app
          ((h.t.truncGE 0).obj X))) :
  β₁ = β₂

Something wrong, better idea? Suggest a change

12.5.23. toH0primeHom_eq🔗

Characterization of when a morphism \beta : E \to H^0{}'(X) equals the canonical lift: \beta = \texttt{toH0primeHom}(f) iff \beta.\mathrm{hom} \circ \iota_{\le 0} = f \circ \pi_{\ge 0}.

Proof: Immediate from \texttt{hom\_ext\_toH0prime} and \texttt{toH0primeHom\_hom}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_eq.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} (f : E.obj ⟶ X)
  (β : E ⟶ CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X)
  (hβ :
    CategoryTheory.CategoryStruct.comp β.hom
        ((h.t.truncLEι 0).app ((h.t.truncGE 0).obj X)) =
      CategoryTheory.CategoryStruct.comp f ((h.t.truncGEπ 0).app X)) :
  β =
    CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E f
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_eq.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  (f : E.obj ⟶ X)
  (β :
    E ⟶
      CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h X)
  (hβ :
    CategoryTheory.CategoryStruct.comp
        β.hom
        ((h.t.truncLEι 0).app
          ((h.t.truncGE 0).obj X)) =
      CategoryTheory.CategoryStruct.comp f
        ((h.t.truncGEπ 0).app X)) :
  β =
    CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
      C h E f

Something wrong, better idea? Suggest a change

12.5.24. toH0primeHom_comp_H0primeFunctor_map🔗

The canonical lift is compatible with post-composition: \texttt{toH0prime}(f) \circ H^0{}'(g) = \texttt{toH0prime}(f \circ g).

Proof: Both sides agree after composing with the truncation inclusion, by naturality of \iota_{\le 0} and the defining property of the lift.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_comp_H0primeFunctor_map.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X Y : C} (f : E.obj ⟶ X)
  (g : X ⟶ Y) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E
        f)
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).map
        g) =
    CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E
      (CategoryTheory.CategoryStruct.comp f g)
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_comp_H0primeFunctor_map.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory)
  {X Y : C} (f : E.obj ⟶ X) (g : X ⟶ Y) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
        C h E f)
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).map
        g) =
    CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
      C h E
      (CategoryTheory.CategoryStruct.comp
        f g)

Something wrong, better idea? Suggest a change

12.5.25. toH0primeHom_comp_H0primeFunctor_map_assoc🔗

Associativity-reassociated form of \texttt{toH0primeHom\_comp\_H0primeFunctor\_map}.

Proof: Obtained by \texttt{reassoc} from the non-assoc version.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_comp_H0primeFunctor_map_assoc.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X Y : C} (f : E.obj ⟶ X) (g : X ⟶ Y)
  {Z : h.t.heart.FullSubcategory}
  (h✝ :
    (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).obj
        Y ⟶
      Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E
        f)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          g)
        h✝) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E
        (CategoryTheory.CategoryStruct.comp f g))
      h✝
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_comp_H0primeFunctor_map_assoc.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory)
  {X Y : C} (f : E.obj ⟶ X) (g : X ⟶ Y)
  {Z : h.t.heart.FullSubcategory}
  (h✝ :
    (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).obj
        Y ⟶
      Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
        C h E f)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          g)
        h✝) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
        C h E
        (CategoryTheory.CategoryStruct.comp
          f g))
      h✝

Something wrong, better idea? Suggest a change

12.5.26. toH0primeHom_zero🔗

The canonical lift of the zero morphism is zero.

Proof: Follows from \texttt{hom\_ext\_toH0prime} and the vanishing of 0 \circ \pi_{\ge 0}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_zero.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} :
  CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E 0 =
    0
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_zero.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory)
  {X : C} :
  CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
      C h E 0 =
    0

Something wrong, better idea? Suggest a change

12.5.27. toH0primeHom_add🔗

The canonical lift is additive: \texttt{toH0prime}(f + g) = \texttt{toH0prime}(f) + \texttt{toH0prime}(g).

Proof: Follows from \texttt{hom\_ext\_toH0prime} and linearity of composition.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_add.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} (f g : E.obj ⟶ X) :
  CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E
      (f + g) =
    CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E
        f +
      CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E
        g
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_add.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  (f g : E.obj ⟶ X) :
  CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
      C h E (f + g) =
    CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
        C h E f +
      CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
        C h E g

Something wrong, better idea? Suggest a change

12.5.28. toH0primeNatTrans🔗

For a heart object E, maps E_{\mathrm{obj}} \to X in \mathcal{C} induce maps E \to H^0{}'(X) in the heart, naturally in X.

Construction: Packages \texttt{toH0primeHom} into a natural transformation between preadditive-coyoneda functors.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.toH0primeNatTrans.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) :
  CategoryTheory.preadditiveCoyoneda.obj (Opposite.op E.obj) ⟶
    (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
          h).comp
      (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op E))
CategoryTheory.Triangulated.HeartStabilityData.toH0primeNatTrans.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) :
  CategoryTheory.preadditiveCoyoneda.obj
      (Opposite.op E.obj) ⟶
    (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
          C h).comp
      (CategoryTheory.preadditiveCoyoneda.obj
        (Opposite.op E))

Something wrong, better idea? Suggest a change

12.5.29. fromH0primeHom_of_isGE🔗

If X \in \mathcal{C}^{\ge 0}, a morphism E \to H^0{}'(X) in the heart can be read as a morphism E_{\mathrm{obj}} \to X in \mathcal{C}.

Construction: Composes the underlying morphism with \iota_{\le 0} and then with the inverse of \pi_{\ge 0} (which is an isomorphism since X \in \mathcal{C}^{\ge 0}).

🔗def
CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} [h.t.IsGE X 0]
  (β :
    E ⟶ CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X) :
  E.obj ⟶ X
CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  [h.t.IsGE X 0]
  (β :
    E ⟶
      CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h X) :
  E.obj ⟶ X

Something wrong, better idea? Suggest a change

12.5.30. fromH0primeHom_of_isGE_hom🔗

The underlying morphism of \texttt{fromH0primeHom\_of\_isGE}(\beta) composed with \pi_{\ge 0} equals \beta.\mathrm{hom} \circ \iota_{\le 0}.

Proof: Follows from \texttt{asIso} applied to the isomorphism \pi_{\ge 0} and the definition of \texttt{fromH0primeHom}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE_hom.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} [h.t.IsGE X 0]
  (β :
    E ⟶ CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
        C h E β)
      ((h.t.truncGEπ 0).app X) =
    CategoryTheory.CategoryStruct.comp β.hom
      ((h.t.truncLEι 0).app ((h.t.truncGE 0).obj X))
CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE_hom.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  [h.t.IsGE X 0]
  (β :
    E ⟶
      CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h X) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
        C h E β)
      ((h.t.truncGEπ 0).app X) =
    CategoryTheory.CategoryStruct.comp
      β.hom
      ((h.t.truncLEι 0).app
        ((h.t.truncGE 0).obj X))

Something wrong, better idea? Suggest a change

12.5.31. fromH0primeHom_of_isGE_hom_assoc🔗

Associativity-reassociated form of \texttt{fromH0primeHom\_of\_isGE\_hom}.

Proof: Obtained by \texttt{reassoc} from the non-assoc version.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE_hom_assoc.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} [h.t.IsGE X 0]
  (β : E ⟶ CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X)
  {Z : C} (h✝ : (h.t.truncGE 0).obj X ⟶ Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
        C h E β)
      (CategoryTheory.CategoryStruct.comp ((h.t.truncGEπ 0).app X) h✝) =
    CategoryTheory.CategoryStruct.comp β.hom
      (CategoryTheory.CategoryStruct.comp
        ((h.t.truncLEι 0).app ((h.t.truncGE 0).obj X)) h✝)
CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE_hom_assoc.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  [h.t.IsGE X 0]
  (β :
    E ⟶
      CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h X)
  {Z : C}
  (h✝ : (h.t.truncGE 0).obj X ⟶ Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
        C h E β)
      (CategoryTheory.CategoryStruct.comp
        ((h.t.truncGEπ 0).app X) h✝) =
    CategoryTheory.CategoryStruct.comp
      β.hom
      (CategoryTheory.CategoryStruct.comp
        ((h.t.truncLEι 0).app
          ((h.t.truncGE 0).obj X))
        h✝)

Something wrong, better idea? Suggest a change

12.5.32. toH0primeHom_fromH0primeHom_of_isGE🔗

The left-inverse identity: \texttt{toH0primeHom}(\texttt{fromH0primeHom}(\beta)) = \beta.

Proof: Uses \texttt{toH0primeHom\_eq} with the equality \texttt{fromH0primeHom\_hom}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_fromH0primeHom_of_isGE.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} [h.t.IsGE X 0]
  (β :
    E ⟶ CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X) :
  CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E
      (CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
        C h E β) =
    β
CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom_fromH0primeHom_of_isGE.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  [h.t.IsGE X 0]
  (β :
    E ⟶
      CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h X) :
  CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
      C h E
      (CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
        C h E β) =
    β

Something wrong, better idea? Suggest a change

12.5.33. fromH0primeHom_of_isGE_toH0primeHom🔗

The right-inverse identity: \texttt{fromH0primeHom}(\texttt{toH0primeHom}(f)) = f.

Proof: Cancels the round-trip using \texttt{fromH0primeHom\_hom} and \texttt{toH0primeHom\_hom} together with monicity of \pi_{\ge 0}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE_toH0primeHom.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} [h.t.IsGE X 0]
  (f : E.obj ⟶ X) :
  CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
      C h E
      (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom C h E
        f) =
    f
CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE_toH0primeHom.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  [h.t.IsGE X 0] (f : E.obj ⟶ X) :
  CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
      C h E
      (CategoryTheory.Triangulated.HeartStabilityData.toH0primeHom
        C h E f) =
    f

Something wrong, better idea? Suggest a change

12.5.34. fromH0primeHom_of_isGE_zero🔗

The map \texttt{fromH0primeHom\_of\_isGE} sends the zero morphism to zero.

Proof: Follows by \texttt{simp} from the definition involving composition with zero.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE_zero.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} [h.t.IsGE X 0] :
  CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
      C h E 0 =
    0
CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE_zero.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  [h.t.IsGE X 0] :
  CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
      C h E 0 =
    0

Something wrong, better idea? Suggest a change

12.5.35. fromH0primeHom_of_isGE_add🔗

The map \texttt{fromH0primeHom\_of\_isGE} is additive: \texttt{from}(\beta_1 + \beta_2) = \texttt{from}(\beta_1) + \texttt{from}(\beta_2).

Proof: Distributes addition through composition with the fixed maps \iota_{\le 0} and (\pi_{\ge 0})^{-1}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE_add.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X : C} [h.t.IsGE X 0]
  (β₁ β₂ :
    E ⟶ CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X) :
  CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
      C h E (β₁ + β₂) =
    CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
        C h E β₁ +
      CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
        C h E β₂
CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE_add.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) {X : C}
  [h.t.IsGE X 0]
  (β₁ β₂ :
    E ⟶
      CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h X) :
  CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
      C h E (β₁ + β₂) =
    CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
        C h E β₁ +
      CategoryTheory.Triangulated.HeartStabilityData.fromH0primeHom_of_isGE
        C h E β₂

Something wrong, better idea? Suggest a change

12.5.36. toH0primeIsoOfIsGE🔗

For X \in \mathcal{C}^{\ge 0}, morphisms E_{\mathrm{obj}} \to X are in natural additive bijection with morphisms E \to H^0{}'(X) in the heart.

Construction: Packages \texttt{toH0primeHom} and \texttt{fromH0primeHom\_of\_isGE} as mutually inverse additive maps, with the two round-trip identities from \texttt{toH0primeHom\_fromH0primeHom\_of\_isGE} and \texttt{fromH0primeHom\_of\_isGE\_toH0primeHom}.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.toH0primeIsoOfIsGE.{v, u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) (X : C) [h.t.IsGE X 0] :
  (E.obj ⟶ X) ≃+
    (E ⟶ CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X)
CategoryTheory.Triangulated.HeartStabilityData.toH0primeIsoOfIsGE.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) (X : C)
  [h.t.IsGE X 0] :
  (E.obj ⟶ X) ≃+
    (E ⟶
      CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h X)

Something wrong, better idea? Suggest a change

12.5.37. H0primeObjIsoTruncGE🔗

H^0{}'(X) is canonically isomorphic to H^0{}'(\tau^{\ge 0} X): replacing X by its \tau^{\ge 0}-truncation does not change H^0{}'.

Construction: Applies \tau^{\le 0} to the isomorphism (\tau^{\ge 0})^2(X) \cong \tau^{\ge 0}(X) (idempotency) to get an isomorphism of the \tau^{\le 0} \circ \tau^{\ge 0} outputs.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) (X : C) :
  CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X ≅
    CategoryTheory.Triangulated.HeartStabilityData.H0prime C h
      ((h.t.truncGE 0).obj X)
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (X : C) :
  CategoryTheory.Triangulated.HeartStabilityData.H0prime
      C h X ≅
    CategoryTheory.Triangulated.HeartStabilityData.H0prime
      C h ((h.t.truncGE 0).obj X)

Something wrong, better idea? Suggest a change

12.5.38. H0primeObjIsoTruncGE_hom_naturality🔗

Naturality of the isomorphism H^0{}'(X) \cong H^0{}'(\tau^{\ge 0} X) with respect to morphisms in \mathcal{C}.

Proof: Checks that both paths around the naturality square agree after using \texttt{truncGEπ\_naturality}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE_hom_naturality.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) {X Y : C}
  (g : X ⟶ Y) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
          C h X).hom
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).map
        ((h.t.truncGE 0).map g)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).map
        g)
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
          C h Y).hom
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE_hom_naturality.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {X Y : C} (g : X ⟶ Y) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
          C h X).hom
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).map
        ((h.t.truncGE 0).map g)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).map
        g)
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
          C h Y).hom

Something wrong, better idea? Suggest a change

12.5.39. H0primeObjIsoTruncGE_hom_naturality_assoc🔗

Associativity-reassociated form of \texttt{H0primeObjIsoTruncGE\_hom\_naturality}.

Proof: Obtained by \texttt{reassoc} from the non-assoc version.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE_hom_naturality_assoc.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) {X Y : C}
  (g : X ⟶ Y) {Z : h.t.heart.FullSubcategory}
  (h✝ :
    (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).obj
        ((h.t.truncGE 0).obj Y) ⟶
      Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
          C h X).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          ((h.t.truncGE 0).map g))
        h✝) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          g)
        (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
            C h Y).hom)
      h✝
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE_hom_naturality_assoc.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {X Y : C} (g : X ⟶ Y)
  {Z : h.t.heart.FullSubcategory}
  (h✝ :
    (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).obj
        ((h.t.truncGE 0).obj Y) ⟶
      Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
          C h X).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          ((h.t.truncGE 0).map g))
        h✝) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          g)
        (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
            C h Y).hom)
      h✝

Something wrong, better idea? Suggest a change

12.5.40. H0primeObjIsoTruncGE_inv_naturality🔗

Naturality of the inverse isomorphism H^0{}'(\tau^{\ge 0} X) \cong H^0{}'(X) with respect to morphisms in \mathcal{C}.

Proof: Deduced from the hom-naturality by inverting and using \texttt{Iso.eq\_comp\_inv}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE_inv_naturality.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) {X Y : C}
  (g : X ⟶ Y) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
          C h X).inv
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).map
        g) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).map
        ((h.t.truncGE 0).map g))
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
          C h Y).inv
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE_inv_naturality.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {X Y : C} (g : X ⟶ Y) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
          C h X).inv
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).map
        g) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).map
        ((h.t.truncGE 0).map g))
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
          C h Y).inv

Something wrong, better idea? Suggest a change

12.5.41. H0primeObjIsoTruncGE_inv_naturality_assoc🔗

Associativity-reassociated form of \texttt{H0primeObjIsoTruncGE\_inv\_naturality}.

Proof: Obtained by \texttt{reassoc} from the non-assoc version.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE_inv_naturality_assoc.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C) {X Y : C}
  (g : X ⟶ Y) {Z : h.t.heart.FullSubcategory}
  (h✝ :
    (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).obj
        Y ⟶
      Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
          C h X).inv
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          g)
        h✝) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          ((h.t.truncGE 0).map g))
        (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
            C h Y).inv)
      h✝
CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE_inv_naturality_assoc.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  {X Y : C} (g : X ⟶ Y)
  {Z : h.t.heart.FullSubcategory}
  (h✝ :
    (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).obj
        Y ⟶
      Z) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
          C h X).inv
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          g)
        h✝) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).map
          ((h.t.truncGE 0).map g))
        (CategoryTheory.Triangulated.HeartStabilityData.H0primeObjIsoTruncGE
            C h Y).inv)
      h✝

Something wrong, better idea? Suggest a change

12.5.42. toH0primeIsoViaTruncGE🔗

For any X, morphisms E_{\mathrm{obj}} \to \tau^{\ge 0} X are in natural additive bijection with morphisms E \to H^0{}'(X) in the heart.

Construction: Composes \texttt{toH0primeIsoOfIsGE} for \tau^{\ge 0} X with postcomposition by (\texttt{H0primeObjIsoTruncGE}(X))^{-1}.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.toH0primeIsoViaTruncGE.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) (X : C) :
  (E.obj ⟶ (h.t.truncGE 0).obj X) ≃+
    (E ⟶ CategoryTheory.Triangulated.HeartStabilityData.H0prime C h X)
CategoryTheory.Triangulated.HeartStabilityData.toH0primeIsoViaTruncGE.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory)
  (X : C) :
  (E.obj ⟶ (h.t.truncGE 0).obj X) ≃+
    (E ⟶
      CategoryTheory.Triangulated.HeartStabilityData.H0prime
        C h X)

Something wrong, better idea? Suggest a change

12.5.43. toH0primeIsoViaTruncGE_naturality🔗

The bijection \texttt{toH0primeIsoViaTruncGE} is natural in X: it commutes with post-composition by a morphism g : X \to Y.

Proof: Reduces to \texttt{toH0primeHom\_comp\_H0primeFunctor\_map} and \texttt{H0primeObjIsoTruncGE\_inv\_naturality}.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.toH0primeIsoViaTruncGE_naturality.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) {X Y : C}
  (f : E.obj ⟶ (h.t.truncGE 0).obj X) (g : X ⟶ Y) :
  (CategoryTheory.Triangulated.HeartStabilityData.toH0primeIsoViaTruncGE
        C h E Y)
      (CategoryTheory.CategoryStruct.comp f ((h.t.truncGE 0).map g)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Triangulated.HeartStabilityData.toH0primeIsoViaTruncGE
          C h E X)
        f)
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
            h).map
        g)
CategoryTheory.Triangulated.HeartStabilityData.toH0primeIsoViaTruncGE_naturality.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory)
  {X Y : C}
  (f : E.obj ⟶ (h.t.truncGE 0).obj X)
  (g : X ⟶ Y) :
  (CategoryTheory.Triangulated.HeartStabilityData.toH0primeIsoViaTruncGE
        C h E Y)
      (CategoryTheory.CategoryStruct.comp
        f ((h.t.truncGE 0).map g)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Triangulated.HeartStabilityData.toH0primeIsoViaTruncGE
          C h E X)
        f)
      ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
            C h).map
        g)

Something wrong, better idea? Suggest a change

12.5.44. toH0primeNatIsoViaTruncGE🔗

For a heart object E, the H^0{}'-evaluation functor \mathcal{C} \to \mathbf{Ab} is naturally isomorphic to evaluation of the ambient \tau^{\ge 0}-truncation functor at E_{\mathrm{obj}}.

Construction: Assembles the component isomorphisms \texttt{toH0primeIsoViaTruncGE} into a \texttt{NatIso} using \texttt{toH0primeIsoViaTruncGE\_naturality}.

🔗def
CategoryTheory.Triangulated.HeartStabilityData.toH0primeNatIsoViaTruncGE.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (E : h.t.heart.FullSubcategory) :
  (h.t.truncGE 0).comp
      (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op E.obj)) ≅
    (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor C
          h).comp
      (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op E))
CategoryTheory.Triangulated.HeartStabilityData.toH0primeNatIsoViaTruncGE.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (E : h.t.heart.FullSubcategory) :
  (h.t.truncGE 0).comp
      (CategoryTheory.preadditiveCoyoneda.obj
        (Opposite.op E.obj)) ≅
    (CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
          C h).comp
      (CategoryTheory.preadditiveCoyoneda.obj
        (Opposite.op E))

Something wrong, better idea? Suggest a change

12.5.45. H0primeFunctor_preadditiveCoyoneda_exact_iff_truncGE🔗

Exactness of the short complex after applying H^0{}' and the preadditive coyoneda is equivalent to exactness after applying \tau^{\ge 0} and the preadditive coyoneda.

Proof: Uses the natural isomorphism \texttt{toH0primeNatIsoViaTruncGE} and \texttt{ShortComplex.exact\_iff\_of\_iso} to transfer exactness between the two functors.

🔗theorem
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveCoyoneda_exact_iff_truncGE.{v,
    u}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  (h : CategoryTheory.Triangulated.HeartStabilityData C)
  (T : CategoryTheory.Pretriangulated.Triangle C)
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (E : h.t.heart.FullSubcategory) :
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).map
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).comp
          (CategoryTheory.preadditiveCoyoneda.obj
            (Opposite.op E)))).Exact ↔
    ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T
            hT).map
        ((h.t.truncGE 0).comp
          (CategoryTheory.preadditiveCoyoneda.obj
            (Opposite.op E.obj)))).Exact
CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor_preadditiveCoyoneda_exact_iff_truncGE.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  (h :
    CategoryTheory.Triangulated.HeartStabilityData
      C)
  (T :
    CategoryTheory.Pretriangulated.Triangle
      C)
  (hT :
    T ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles)
  (E : h.t.heart.FullSubcategory) :
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
            T hT).map
        ((CategoryTheory.Triangulated.HeartStabilityData.H0primeFunctor
              C h).comp
          (CategoryTheory.preadditiveCoyoneda.obj
            (Opposite.op E)))).Exact ↔
    ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle
            T hT).map
        ((h.t.truncGE 0).comp
          (CategoryTheory.preadditiveCoyoneda.obj
            (Opposite.op E.obj)))).Exact

Something wrong, better idea? Suggest a change