Six-term original-heart cohomology sequences

This file packages the exact sequence needed when a distinguished triangle is also a short exact sequence in an HRS-tilted heart. For a t-structure t, the six terms are

H⁻¹_t(X₁) ⟶ H⁻¹_t(X₂) ⟶ H⁻¹_t(X₃) ⟶ H⁰_t(X₁) ⟶ H⁰_t(X₂) ⟶ H⁰_t(X₃).

The construction and exactness proof are unconditional. The originalHeartCohFunctor_isHomological instance proves that degree-zero cohomology of any t-structure sends distinguished triangles to exact short complexes, without stability-function or Harder--Narasimhan hypotheses.

For objects of an HRS-tilted heart, the amplitude bounds supplied by WeakStabilityCondition/Tilting/Cohomology/Basic.lean also show that the first arrow is monic and the last is epic, giving the expected zeroes at the two ends.

Degree comparison

theorem CategoryTheory.Triangulated.Tilting.TStructure.triangleLTGE_iso_of_amp_negOne_zero {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) {X K Q : C} (hK : t.heart K) (hQ : t.heart Q) {α : (shiftFunctor C 1).obj K ⟶ X} {β : X ⟶ Q} {γ : Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj K)} (hT : Pretriangulated.Triangle.mk α β γ ∈ Pretriangulated.distinguishedTriangles) : ∃ (e : Pretriangulated.Triangle.mk α β γ ≅ (t.triangleLTGE 0).obj X), e.hom.hom₂ = CategoryStruct.id X

A distinguished triangle presenting an object with amplitude [-1, 0] is isomorphic, through the identity on its middle object, to the canonical truncation triangle.

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohNegOneIsoOfAmplitude {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) {X K Q : C} (hK : t.heart K) (hQ : t.heart Q) {α : (shiftFunctor C 1).obj K ⟶ X} {β : X ⟶ Q} {γ : Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj K)} (hT : Pretriangulated.Triangle.mk α β γ ∈ Pretriangulated.distinguishedTriangles) [t.IsGE X (-1)] : originalHeartCoh t (-1) X ≅ { obj := K, property := hK }

For an amplitude-[-1,0] presentation K[1] ⟶ X ⟶ Q, degree -1 original-heart cohomology is K.

Equations

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

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohZeroIsoOfAmplitude {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) {X K Q : C} (hK : t.heart K) (hQ : t.heart Q) {α : (shiftFunctor C 1).obj K ⟶ X} {β : X ⟶ Q} {γ : Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj K)} (hT : Pretriangulated.Triangle.mk α β γ ∈ Pretriangulated.distinguishedTriangles) [t.IsLE X 0] : originalHeartCoh t 0 X ≅ { obj := Q, property := hQ }

For an amplitude-[-1,0] presentation K[1] ⟶ X ⟶ Q, degree zero original-heart cohomology is Q.

Equations

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

@[implicit_reducible]

noncomputable instance CategoryTheory.Triangulated.Tilting.originalHeartCohFunctor_zero_shiftSequence {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) : (originalHeartCohFunctor t 0).ShiftSequence ℤ

The tautological shift sequence on degree-zero original-heart cohomology.

Equations

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

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohShiftIso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (n : ℤ) (X : C) : ((originalHeartCohFunctor t 0).shift n).obj X ≅ originalHeartCoh t n X

The shifted degree-zero functor agrees with the explicit degree-n original-heart cohomology functor, evaluated at an object.

Equations

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

theorem CategoryTheory.Triangulated.Tilting.originalHeartCoh_isZero_of_isGE {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) {X : C} {n lower : ℤ} (hX : t.IsGE X lower) (hn : n + 1 ≤ lower) : Limits.IsZero (originalHeartCoh t n X)

Cohomology below a known lower bound vanishes.

theorem CategoryTheory.Triangulated.Tilting.originalHeartCoh_isZero_of_isLE {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) {X : C} {n upper : ℤ} (hX : t.IsLE X upper) (hn : upper + 1 ≤ n) : Limits.IsZero (originalHeartCoh t n X)

Cohomology above a known upper bound vanishes.

theorem CategoryTheory.Triangulated.Tilting.originalHeartCohFunctor_shift_isZero_of_isGE {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) {X : C} {n lower : ℤ} (hX : t.IsGE X lower) (hn : n + 1 ≤ lower) : Limits.IsZero (((originalHeartCohFunctor t 0).shift n).obj X)

Shift-normal-form cohomology below a lower bound is zero.

theorem CategoryTheory.Triangulated.Tilting.originalHeartCohFunctor_shift_isZero_of_isLE {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) {X : C} {n upper : ℤ} (hX : t.IsLE X upper) (hn : upper + 1 ≤ n) : Limits.IsZero (((originalHeartCohFunctor t 0).shift n).obj X)

Shift-normal-form cohomology above an upper bound is zero.

The six-term sequence

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (T : Pretriangulated.Triangle C) : ComposableArrows t.heart.FullSubcategory 5

The six-term original-heart cohomology sequence of a triangle, in the shift-sequence normal form used by Mathlib's homological-functor API. The six objectwise comparison isomorphisms below identify its terms with the explicit originalHeartCoh t (-1) and originalHeartCoh t 0 objects.

Equations

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

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_obj₀Iso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (T : Pretriangulated.Triangle C) : (originalHeartCohomologySixTermSequence t T).obj' 0 ⋯ ≅ originalHeartCoh t (-1) T.obj₁

The first term is explicit degree-minus-one cohomology of the first triangle vertex.

Equations

• CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_obj₀Iso t T = CategoryTheory.Triangulated.Tilting.originalHeartCohShiftIso t (-1) T.obj₁

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_obj₁Iso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (T : Pretriangulated.Triangle C) : (originalHeartCohomologySixTermSequence t T).obj' 1 ⋯ ≅ originalHeartCoh t (-1) T.obj₂

The second term is explicit degree-minus-one cohomology of the second triangle vertex.

Equations

• CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_obj₁Iso t T = CategoryTheory.Triangulated.Tilting.originalHeartCohShiftIso t (-1) T.obj₂

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_obj₂Iso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (T : Pretriangulated.Triangle C) : (originalHeartCohomologySixTermSequence t T).obj' 2 ⋯ ≅ originalHeartCoh t (-1) T.obj₃

The third term is explicit degree-minus-one cohomology of the third triangle vertex.

Equations

• CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_obj₂Iso t T = CategoryTheory.Triangulated.Tilting.originalHeartCohShiftIso t (-1) T.obj₃

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_obj₃Iso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (T : Pretriangulated.Triangle C) : (originalHeartCohomologySixTermSequence t T).obj' 3 ⋯ ≅ originalHeartCoh t 0 T.obj₁

The fourth term is explicit degree-zero cohomology of the first triangle vertex.

Equations

• CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_obj₃Iso t T = CategoryTheory.Triangulated.Tilting.originalHeartCohShiftIso t 0 T.obj₁

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_obj₄Iso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (T : Pretriangulated.Triangle C) : (originalHeartCohomologySixTermSequence t T).obj' 4 ⋯ ≅ originalHeartCoh t 0 T.obj₂

The fifth term is explicit degree-zero cohomology of the second triangle vertex.

Equations

• CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_obj₄Iso t T = CategoryTheory.Triangulated.Tilting.originalHeartCohShiftIso t 0 T.obj₂

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_obj₅Iso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (T : Pretriangulated.Triangle C) : (originalHeartCohomologySixTermSequence t T).obj' 5 ⋯ ≅ originalHeartCoh t 0 T.obj₃

The sixth term is explicit degree-zero cohomology of the third triangle vertex.

Equations

• CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_obj₅Iso t T = CategoryTheory.Triangulated.Tilting.originalHeartCohShiftIso t 0 T.obj₃

theorem CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_exact {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) : (originalHeartCohomologySixTermSequence t T).Exact

The explicit six-term sequence is exact at all four interior junctions.

theorem CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_mono_first {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (hX₃ : t.IsGE T.obj₃ (-1)) : Mono ((originalHeartCohomologySixTermSequence t T).map' 0 1 ⋯ ⋯)

If the third vertex has no cohomology below degree -1, the first map of the six-term sequence is monic.

theorem CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence_epi_last {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (hX₁ : t.IsLE T.obj₁ 0) : Epi ((originalHeartCohomologySixTermSequence t T).map' 4 5 ⋯ ⋯)

If the first vertex has no cohomology above degree zero, the last map of the six-term sequence is epic.

Short exact sequences in the tilted heart

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.exists_distinguished_triangle_of_shortExact {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : ∃ (δ : S.X₃.obj ⟶ (shiftFunctor C 1).obj S.X₁.obj), Pretriangulated.Triangle.mk S.f.hom S.g.hom δ ∈ Pretriangulated.distinguishedTriangles

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

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.triangleOfShortExact {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : Pretriangulated.Triangle C

The ambient distinguished triangle canonically chosen from a tilted-heart short exact sequence.

Equations

• P.triangleOfShortExact S hS = CategoryTheory.Pretriangulated.Triangle.mk S.f.hom S.g.hom ⋯.choose

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.triangleOfShortExact_distinguished {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : P.triangleOfShortExact S hS ∈ Pretriangulated.distinguishedTriangles

The chosen triangle of a tilted-heart short exact sequence is distinguished.

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologySixTermSequenceOfShortExact {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : ComposableArrows t.heart.FullSubcategory 5

The six original-heart cohomology terms attached to a short exact sequence in the HRS-tilted heart.

Equations

• P.originalCohomologySixTermSequenceOfShortExact S hS = CategoryTheory.Triangulated.Tilting.originalHeartCohomologySixTermSequence t (P.triangleOfShortExact S hS)

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologySixTermSequenceOfShortExact_obj₀Iso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : (P.originalCohomologySixTermSequenceOfShortExact S hS).obj' 0 ⋯ ≅ P.originalHMinusOne ⋯

The first term is the canonical original H⁻¹ of the subobject.

Equations

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

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologySixTermSequenceOfShortExact_obj₁Iso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : (P.originalCohomologySixTermSequenceOfShortExact S hS).obj' 1 ⋯ ≅ P.originalHMinusOne ⋯

The second term is the canonical original H⁻¹ of the middle object.

Equations

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

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologySixTermSequenceOfShortExact_obj₂Iso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : (P.originalCohomologySixTermSequenceOfShortExact S hS).obj' 2 ⋯ ≅ P.originalHMinusOne ⋯

The third term is the canonical original H⁻¹ of the quotient.

Equations

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

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologySixTermSequenceOfShortExact_obj₃Iso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : (P.originalCohomologySixTermSequenceOfShortExact S hS).obj' 3 ⋯ ≅ P.originalHZero ⋯

The fourth term is the canonical original H⁰ of the subobject.

Equations

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

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologySixTermSequenceOfShortExact_obj₄Iso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : (P.originalCohomologySixTermSequenceOfShortExact S hS).obj' 4 ⋯ ≅ P.originalHZero ⋯

The fifth term is the canonical original H⁰ of the middle object.

Equations

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

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologySixTermSequenceOfShortExact_obj₅Iso {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : (P.originalCohomologySixTermSequenceOfShortExact S hS).obj' 5 ⋯ ≅ P.originalHZero ⋯

The sixth term is the canonical original H⁰ of the quotient.

Equations

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

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologySixTermSequenceOfShortExact_exact {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : (P.originalCohomologySixTermSequenceOfShortExact S hS).Exact

A tilted-heart short exact sequence induces an exact six-term sequence in the original heart.

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologySixTermSequenceOfShortExact_mono_first {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : Mono ((P.originalCohomologySixTermSequenceOfShortExact S hS).map' 0 1 ⋯ ⋯)

The first map in the six-term sequence induced by a tilted-heart short exact sequence is monic.

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologySixTermSequenceOfShortExact_epi_last {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : Epi ((P.originalCohomologySixTermSequenceOfShortExact S hS).map' 4 5 ⋯ ⋯)

The last map in the six-term sequence induced by a tilted-heart short exact sequence is epic.

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologySixTermSequenceOfShortExact_exact_with_endpoints {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) (S : ShortComplex P.tilt.heart.FullSubcategory) (hS : S.ShortExact) : (P.originalCohomologySixTermSequenceOfShortExact S hS).Exact ∧ Mono ((P.originalCohomologySixTermSequenceOfShortExact S hS).map' 0 1 ⋯ ⋯) ∧ Epi ((P.originalCohomologySixTermSequenceOfShortExact S hS).map' 4 5 ⋯ ⋯)

Paper-shaped form: the six-term sequence is exact, begins with a mono, and ends with an epi. Equivalently it may be displayed with zero objects at both ends.

Quotients of pure shifted objects

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.exists_original_triangle_of_torsion_subobject_free_shift {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (P : HeartTorsionPair t) {F T I : C} (hF : P.free F) (hT : P.tors T) (hI : P.tilt.heart I) {a : T ⟶ (shiftFunctor C 1).obj F} {q : (shiftFunctor C 1).obj F ⟶ I} {d : I ⟶ (shiftFunctor C 1).obj T} (hd : Pretriangulated.Triangle.mk a q d ∈ Pretriangulated.distinguishedTriangles) : ∃ (Ftilde : C) (_ : P.free Ftilde) (i : F ⟶ Ftilde) (p : Ftilde ⟶ T) (delta : T ⟶ (shiftFunctor C 1).obj F), Pretriangulated.Triangle.mk i p delta ∈ Pretriangulated.distinguishedTriangles ∧ Nonempty ((shiftFunctor C 1).obj Ftilde ≅ I)

A quotient of F[1] in the tilted heart by an original torsion subobject is again a pure shifted object. The middle four terms of the six-term sequence simultaneously produce the original-heart short exact sequence F ⟶ Ftilde ⟶ T.

This is the cohomological bridge used by boundary-phase saturation: the intersection with a maximal zero-charge subobject is an original torsion object T, so its quotient inside F[1] is Ftilde[1].