Original-heart cohomology of objects in an HRS-tilted heart

This file supplies the two-term cohomology bridge used by weak tilting arguments. It has two independent parts:

• originalHeartCohFunctor t n is the historical tilting-facing name for t.heartCohFunctor n, the degree-n cohomology of an arbitrary t-structure. Unlike HeartStabilityData.heartCohFunctor, it requires no stability or HN data.

• for a torsion pair P and an object X of the tilted heart, the canonical truncation triangle is exposed as

  H⁻¹_t(X)⟦1⟧ ⟶ X ⟶ H⁰_t(X).

The first term is torsion-free, the last is torsion, and the triangle induces a short exact sequence in the tilted heart. The final two theorems expose the inclusion as a kernel and the projection as a cokernel, so downstream semistability proofs can use abelian kernel/image language without reopening the ambient triangulated-category argument.

Cohomology attached only to a t-structure

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.Tilting.originalHeartCohFunctor {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 : ℤ) : Functor C t.heart.FullSubcategory

Historical tilting-facing name for t-structure-owned heart cohomology.

Equations

• CategoryTheory.Triangulated.Tilting.originalHeartCohFunctor t n = t.heartCohFunctor n

theorem CategoryTheory.Triangulated.Tilting.originalHeartCohFunctor_additive {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 : ℤ) : (originalHeartCohFunctor t n).Additive

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohFunctorZeroIso {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 ≅ t.heartH0Functor

The existing degree-zero tilted-cohomology notation agrees naturally with the t-structure-owned degree-zero heart functor.

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.Tilting.originalHeartCoh {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 : ℤ) (E : C) : t.heart.FullSubcategory

The object-level notation for originalHeartCohFunctor.

Equations

• CategoryTheory.Triangulated.Tilting.originalHeartCoh t n E = (CategoryTheory.Triangulated.Tilting.originalHeartCohFunctor t n).obj E

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohIsoOfHeart {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) (E : t.heart.FullSubcategory) : originalHeartCoh t 0 E.obj ≅ E

Degree-zero cohomology recovers an object already in the heart. This applies equally to the original t-structure and to an HRS tilt.

Equations

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

Canonical factors of a tilted-heart object

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.Tilting.HeartTorsionPair.tiltedHeartCohFunctor {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} (P : HeartTorsionPair t) [IsTriangulated C] (n : ℤ) : Functor C P.tilt.heart.FullSubcategory

Cohomology for the tilted t-structure. This abbreviation makes explicit that the same t-structure-only construction is available in both hearts.

Equations

• P.tiltedHeartCohFunctor n = CategoryTheory.Triangulated.Tilting.originalHeartCohFunctor P.tilt n

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.tors_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} (P : HeartTorsionPair t) : P.tors 0

The zero object belongs to the torsion class.

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.free_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} (P : HeartTorsionPair t) : P.free 0

The zero object belongs to the torsion-free class.

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.isLE_zero_of_tilt_heart {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : t.IsLE X 0

A tilted-heart object has original cohomological upper bound zero.

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.isGE_neg_one_of_tilt_heart {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : t.IsGE X (-1)

A tilted-heart object has original cohomological lower bound minus one.

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.tors_truncGE_zero_of_tilt_heart {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : P.tors ((t.truncGE 0).obj X)

The original degree-zero truncation of a tilted-heart object is torsion.

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.free_truncLT_zero_shift_of_tilt_heart {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : P.free ((shiftFunctor C (-1)).obj ((t.truncLT 0).obj X))

The original degree-minus-one truncation of a tilted-heart object, shifted into the original heart, is torsion-free.

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHMinusOne {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : t.heart.FullSubcategory

The original H⁻¹ factor of a tilted-heart object. Its underlying object is τ^{<0}X⟦-1⟧.

Equations

• P.originalHMinusOne hX = { obj := (CategoryTheory.shiftFunctor C (-1)).obj ((t.truncLT 0).obj X), property := ⋯ }

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHZero {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : t.heart.FullSubcategory

The original H⁰ factor of a tilted-heart object. Its underlying object is τ^{≥0}X.

Equations

• P.originalHZero hX = { obj := (t.truncGE 0).obj X, property := ⋯ }

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHMinusOne_free {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : P.free (P.originalHMinusOne hX).obj

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHZero_tors {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : P.tors (P.originalHZero hX).obj

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHeartCohIsoHMinusOne {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : originalHeartCoh t (-1) X ≅ P.originalHMinusOne hX

The truncation model of H⁻¹ agrees with the generic original-heart cohomology functor.

Equations

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

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHeartCohIsoHZero {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : originalHeartCoh t 0 X ≅ P.originalHZero hX

The truncation model of H⁰ agrees with the generic original-heart cohomology functor.

Equations

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

The canonical short exact sequence in the tilted heart

noncomputable def CategoryTheory.Triangulated.Tilting.originalCohomologyShiftIso {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 : C) : (shiftFunctor C 1).obj ((shiftFunctor C (-1)).obj ((t.truncLT 0).obj X)) ≅ (t.truncLT 0).obj X

The shift-cancellation isomorphism used to put the first term of the level-zero truncation triangle in H⁻¹(X)⟦1⟧ form.

Equations

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

noncomputable def CategoryTheory.Triangulated.Tilting.originalCohomologyTriangle {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 : C) : Pretriangulated.Triangle C

The canonical original-cohomology triangle of X, obtained from the level-zero truncation triangle by writing its first term as H⁻¹(X)⟦1⟧.

Equations

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

theorem CategoryTheory.Triangulated.Tilting.originalCohomologyTriangle_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] (t : TStructure C) (X : C) : originalCohomologyTriangle t X ∈ Pretriangulated.distinguishedTriangles

The canonical original-cohomology triangle is distinguished.

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.free_shift_mem_tilt_heart {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} (P : HeartTorsionPair t) [IsTriangulated C] {F : C} (hF : P.free F) : P.tilt.heart ((shiftFunctor C 1).obj F)

A shifted torsion-free object belongs to the tilted heart.

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.tors_mem_tilt_heart {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} (P : HeartTorsionPair t) [IsTriangulated C] {T : C} (hT : P.tors T) : P.tilt.heart T

A torsion object belongs to the tilted heart.

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHMinusOneShiftInTiltHeart {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : P.tilt.heart.FullSubcategory

The H⁻¹(X)⟦1⟧ term, regarded as an object of the tilted heart.

Equations

• P.originalHMinusOneShiftInTiltHeart hX = { obj := (CategoryTheory.shiftFunctor C 1).obj (P.originalHMinusOne hX).obj, property := ⋯ }

def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.objectInTiltHeart {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : P.tilt.heart.FullSubcategory

X, regarded as an object of the tilted heart.

Equations

• P.objectInTiltHeart hX = { obj := X, property := hX }

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHZeroInTiltHeart {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : P.tilt.heart.FullSubcategory

The H⁰(X) term, regarded as an object of the tilted heart.

Equations

• P.originalHZeroInTiltHeart hX = { obj := (P.originalHZero hX).obj, property := ⋯ }

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologyShortComplex {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : ShortComplex P.tilt.heart.FullSubcategory

The canonical two-term original-cohomology complex in the tilted heart.

Equations

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

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologyShortComplex_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] {t : TStructure C} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : (P.originalCohomologyShortComplex hX).ShortExact

The canonical sequence 0 ⟶ H⁻¹_t(X)⟦1⟧ ⟶ X ⟶ H⁰_t(X) ⟶ 0 is short exact in the tilted heart.

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologyShortComplex_f_isKernel {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : Nonempty (Limits.IsLimit (Limits.KernelFork.ofι (P.originalCohomologyShortComplex hX).f ⋯))

The left map of the canonical tilted-heart sequence is a kernel of the right map.

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalCohomologyShortComplex_g_isCokernel {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) : Nonempty (Limits.IsColimit (Limits.CokernelCofork.ofπ (P.originalCohomologyShortComplex hX).g ⋯))

The right map of the canonical tilted-heart sequence is a cokernel of the left map.

Pure shifted objects

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHMinusOne_isZero_of_tors {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} (P : HeartTorsionPair t) [IsTriangulated C] {T : C} (hT : P.tors T) : Limits.IsZero (P.originalHMinusOne ⋯)

The original degree-minus-one cohomology of a torsion object vanishes.

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHZeroIsoOfTors {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} (P : HeartTorsionPair t) [IsTriangulated C] {T : C} (hT : P.tors T) : P.originalHZero ⋯ ≅ { obj := T, property := ⋯ }

The original H⁰ of a torsion object is canonically the object itself.

Equations

• P.originalHZeroIsoOfTors hT = (P.originalHeartCohIsoHZero ⋯).symm ≪≫ CategoryTheory.Triangulated.Tilting.originalHeartCohIsoOfHeart t { obj := T, property := ⋯ }

theorem CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHZero_isZero_of_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] {t : TStructure C} (P : HeartTorsionPair t) [IsTriangulated C] {F : C} (hF : P.free F) : Limits.IsZero (P.originalHZero ⋯)

The original degree-zero cohomology of a shifted torsion-free object vanishes. This is the endpoint calculation used when a quotient in the tilted heart is shown to remain a pure shifted object.

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHMinusOneShiftIsoOfHZeroIsZero {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} (P : HeartTorsionPair t) [IsTriangulated C] {X : C} (hX : P.tilt.heart X) (hzero : Limits.IsZero (P.originalHZero hX)) : P.originalHMinusOneShiftInTiltHeart hX ≅ P.objectInTiltHeart hX

If the original H⁰ of a tilted-heart object vanishes, its canonical H⁻¹[1] subobject is an isomorphism.

Equations

• P.originalHMinusOneShiftIsoOfHZeroIsZero hX hzero = CategoryTheory.asIso (P.originalCohomologyShortComplex hX).f

noncomputable def CategoryTheory.Triangulated.Tilting.HeartTorsionPair.originalHMinusOneIsoOfFreeShift {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} (P : HeartTorsionPair t) [IsTriangulated C] {F : C} (hF : P.free F) : P.originalHMinusOne ⋯ ≅ { obj := F, property := ⋯ }

The original H⁻¹ of F[1] is canonically isomorphic to F when F is torsion-free.

Equations

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