Owner bridge for t-structure hearts

This module gives repository-owned public names to the small amount of t-structure heart infrastructure that is not yet in Mathlib. It contains no stability-condition definitions.

theorem CategoryTheory.ObjectProperty.FullSubcategory.isZero_of_obj_isZero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P : ObjectProperty C} [Limits.HasZeroMorphisms P.FullSubcategory] [Limits.HasZeroObject P.FullSubcategory] {X : P.FullSubcategory} (hX : Limits.IsZero X.obj) : Limits.IsZero X

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

Degree-n cohomology in the heart of t, constructed from the pure truncation τ^[n,n] and the shift placing it in degree zero.

Equations

• t.heartCohFunctor n = t.heart.lift ((t.truncGELE n n).comp (CategoryTheory.shiftFunctor C n)) ⋯

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

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

Degree-zero cohomology in the heart of t, given by the pure truncation τ^[0,0].

Equations

• t.heartH0Functor = t.heart.lift (t.truncGELE 0 0) ⋯

instance CategoryTheory.Triangulated.TStructure.heartH0Functor_additive {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] : t.heartH0Functor.Additive

noncomputable def CategoryTheory.Triangulated.TStructure.heartH0OnHeartIso {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] : t.heart.ι.comp t.heartH0Functor ≅ Functor.id t.heart.FullSubcategory

Degree-zero cohomology is naturally the identity on the heart.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.TStructure.heart_hι {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {H : Type u'} [Category.{v', u'} H] [Preadditive H] [t.Heart H] ⦃X Y : H⦄ ⦃n : ℤ⦄ (f : t.ιHeart.obj X ⟶ (shiftFunctor C n).obj (t.ιHeart.obj Y)) : n < 0 → f = 0

Negative ambient Hom spaces between objects of a t-structure heart vanish.

theorem CategoryTheory.Triangulated.TStructure.heart_admissible {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {H : Type u'} [Category.{v', u'} H] [Preadditive H] [t.Heart H] : AbelianSubcategory.admissibleMorphism t.ιHeart = ⊤

Every heart morphism is admissible for Mathlib's abelian-subcategory criterion.

@[reducible]

noncomputable def CategoryTheory.Triangulated.TStructure.heartAbelian {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {H : Type u'} [Category.{v', u'} H] [Preadditive H] [t.Heart H] [IsTriangulated C] [Limits.HasFiniteProducts H] : Abelian H

A heart satisfying the standard finite-product interface is abelian.

Equations

• t.heartAbelian = CategoryTheory.Triangulated.AbelianSubcategory.abelian t.ιHeart ⋯ ⋯

instance CategoryTheory.Triangulated.TStructure.heart_containsZero {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) : t.heart.ContainsZero

theorem CategoryTheory.Triangulated.TStructure.heart_biprod {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (X Y : C) (hX : t.heart X) (hY : t.heart Y) : t.heart (X ⊞ Y)

instance CategoryTheory.Triangulated.TStructure.heart_closedUnderBinaryProducts {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) : t.heart.IsClosedUnderBinaryProducts

instance CategoryTheory.Triangulated.TStructure.heart_closedUnderFiniteProducts {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) : t.heart.IsClosedUnderFiniteProducts

instance CategoryTheory.Triangulated.TStructure.heart_hasFiniteProducts {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) : Limits.HasFiniteProducts t.heart.FullSubcategory

@[reducible]

noncomputable def CategoryTheory.Triangulated.TStructure.heartFullSubcategoryAbelian {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] : Abelian t.heart.FullSubcategory

The canonical abelian-category instance on the full subcategory cut out by the heart of a triangulated t-structure.

Equations

• t.heartFullSubcategoryAbelian = t.heartAbelian

theorem CategoryTheory.Triangulated.TStructure.heartFullSubcategory_shortExact_of_distTriang {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] {A B Q : t.heart.FullSubcategory} {f : A ⟶ B} {g : B ⟶ Q} {δ : Q.obj ⟶ (shiftFunctor C 1).obj A.obj} (hT : Pretriangulated.Triangle.mk f.hom g.hom δ ∈ Pretriangulated.distinguishedTriangles) : { X₁ := A, X₂ := B, X₃ := Q, f := f, g := g, zero := ⋯ }.ShortExact

theorem CategoryTheory.Triangulated.TStructure.heartFullSubcategory_shortExact_triangle {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {A B Q : t.heart.FullSubcategory} (f : A ⟶ B) (g : B ⟶ Q) (hfg : CategoryStruct.comp f g = 0) [Mono f] [Epi g] (hexact : ∀ {W : t.heart.FullSubcategory} (alpha : W ⟶ B), CategoryStruct.comp alpha g = 0 → ∃ (beta : W ⟶ A), CategoryStruct.comp beta f = alpha) : ∃ (delta : Q.obj ⟶ (shiftFunctor C 1).obj A.obj), Pretriangulated.Triangle.mk f.hom g.hom delta ∈ Pretriangulated.distinguishedTriangles

A short exact sequence in the full heart extends to a distinguished triangle in the ambient category.

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

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

theorem CategoryTheory.Triangulated.TStructure.exists_truncLT_octahedral_split {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) [IsTriangulated C] {X₁ X₂ X₃ : C} {f : X₁ ⟶ X₂} {g : X₂ ⟶ X₃} {δ : X₃ ⟶ (shiftFunctor C 1).obj X₁} (hT : Pretriangulated.Triangle.mk f g δ ∈ Pretriangulated.distinguishedTriangles) (a : ℤ) : ∃ (Z : C) (v : X₂ ⟶ Z) (w : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT a).obj X₁)) (m₁ : (t.truncGE a).obj X₁ ⟶ Z) (m₃ : Z ⟶ X₃), Pretriangulated.Triangle.mk (CategoryStruct.comp ((t.truncLTι a).app X₁) f) v w ∈ Pretriangulated.distinguishedTriangles ∧ Pretriangulated.Triangle.mk m₁ m₃ (CategoryStruct.comp δ ((shiftFunctor C 1).map ((t.truncGEπ a).app X₁))) ∈ Pretriangulated.distinguishedTriangles ∧ CategoryStruct.comp ((t.truncGEπ a).app X₁) m₁ = CategoryStruct.comp f v ∧ CategoryStruct.comp m₁ w = (t.truncGEδLT a).app X₁ ∧ CategoryStruct.comp v m₃ = g

The octahedron associated to a truncation triangle, with the three commutativities used by tilted-cohomology calculations exposed explicitly.