Two-heart embeddings of owner interval categories

Every phase interval of width at most one embeds fully faithfully into two adjacent abelian slicing hearts. The left heart controls kernels and images; the right half-open heart controls cokernels and coimages. This is the owner foundation for the quasi-abelian interval machinery used by target transport.

The file also owns the dual half-open t-structure of a slicing: the dictionary translating the degree-zero aisle and degree-one coaisle of the phase-shifted dual t-structure into the cuts P(≥ t) and P(< t), and its boundedness, which is the one clause about the slicing itself that any larger-ambient extension of it has to be given.

theorem CategoryTheory.Triangulated.Slicing.intervalProp_implies_leftHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {a b : ℝ} (hab : b - a ≤ 1) {E : C} (hE : intervalProp C s a b E) : (toTStructure C (phaseShift C s a)).heart E

Owner interval objects lie in the left adjacent slicing heart P((a,a+1]).

def CategoryTheory.Triangulated.Slicing.toDualTStructure (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) : TStructure C

The dual half-open t-structure associated to an owner slicing. Its heart is P([0,1)).

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.Slicing.toDualTStructure_heart_iff (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (E : C) : (toDualTStructure C s).heart E ↔ geProp C s 0 E ∧ ltProp C s 1 E

theorem CategoryTheory.Triangulated.Slicing.phaseShift_toDualTStructure_isLE_zero_iff (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (t : ℝ) (E : C) : (toDualTStructure C (phaseShift C s t)).IsLE E 0 ↔ geProp C s t E

The connective half of the dual t-structure at the phase t is the lower phase cut 𝒫(≥ t). This is the dictionary through which the phase-indexed family of dual t-structures τ'_t = (𝒫(≥ t), 𝒫(< t + 1)) is read. Not a simp lemma: the phase cut is not a normal form the simplifier should chase, and both consumers apply the dictionary by hand at a chosen degree.

theorem CategoryTheory.Triangulated.Slicing.phaseShift_toDualTStructure_isGE_one_iff (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (t : ℝ) (E : C) : (toDualTStructure C (phaseShift C s t)).IsGE E 1 ↔ ltProp C s t E

The degree-one coconnective half of the dual t-structure at the phase t is the strict upper phase cut 𝒫(< t).

theorem CategoryTheory.Triangulated.Slicing.toDualTStructure_isBounded (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) : (toDualTStructure C s).IsBounded

The dual t-structure of a slicing is bounded: an HN filtration of an object confines its phases to a finite interval, which the integer degrees enclose. Boundedness is the only obligation about the slicing itself that a larger-ambient extension of this t-structure cannot derive from its own aisle formula, so this is the lemma such a construction consumes (TStructure.IndExtensionData.small_isBounded).

theorem CategoryTheory.Triangulated.Slicing.intervalProp_implies_rightHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {a b : ℝ} (hab : b - a ≤ 1) {E : C} (hE : intervalProp C s a b E) : (toDualTStructure C (phaseShift C s (b - 1))).heart E

Owner interval objects lie in the right adjacent half-open slicing heart P([b-1,b)).

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (a b : ℝ) (hab : b - a ≤ 1) : Functor (IntervalCat C s a b) (toTStructure C (phaseShift C s a)).heart.FullSubcategory

Fully faithful inclusion of an owner interval category into its left adjacent heart.

Equations

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

instance CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_full (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (a b : ℝ) (hab : b - a ≤ 1) : (toLeftHeart C s a b hab).Full

instance CategoryTheory.Triangulated.Slicing.IntervalCat.toLeftHeart_faithful (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (a b : ℝ) (hab : b - a ≤ 1) : (toLeftHeart C s a b hab).Faithful

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (a b : ℝ) (hab : b - a ≤ 1) : Functor (IntervalCat C s a b) (toDualTStructure C (phaseShift C s (b - 1))).heart.FullSubcategory

Fully faithful inclusion of an owner interval category into its right adjacent half-open heart.

Equations

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

instance CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_full (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (a b : ℝ) (hab : b - a ≤ 1) : (toRightHeart C s a b hab).Full

instance CategoryTheory.Triangulated.Slicing.IntervalCat.toRightHeart_faithful (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (a b : ℝ) (hab : b - a ≤ 1) : (toRightHeart C s a b hab).Faithful

theorem CategoryTheory.Triangulated.Slicing.phiMinus_gt_of_triangle_with_geProp (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {K E Q : C} (hQ : ¬Limits.IsZero Q) {a : ℝ} (hE : ∀ (hE : ¬Limits.IsZero E), a < phiMinus C s E hE) {c : ℝ} (hK : geProp C s c K) (hca : a < c + 1) {f : K ⟶ E} {g : E ⟶ Q} {h : Q ⟶ (shiftFunctor C 1).obj K} (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) : a < phiMinus C s Q hQ

A non-strict lower phase bound propagates through the third vertex of a distinguished triangle.

theorem CategoryTheory.Triangulated.Slicing.third_intervalProp_of_triangle (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) {a b : ℝ} (hab : a < b) {K E Q : C} (hE : intervalProp C s a b E) (hK : geProp C s (b - 1) K) (hQ : ltProp C s b Q) {f : K ⟶ E} {g : E ⟶ Q} {h : Q ⟶ (shiftFunctor C 1).obj K} (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) : intervalProp C s a b Q

The third vertex stays in a thin owner interval when right-heart bounds are available on the first and third vertices.

theorem CategoryTheory.Triangulated.Slicing.intervalProp_of_mono_leftHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {a b : ℝ} (hab : a < b) {X Y : (toTStructure C (phaseShift C s a)).heart.FullSubcategory} (hY : intervalProp C s a b Y.obj) (f : X ⟶ Y) [Mono f] : intervalProp C s a b X.obj

A monomorphism in the left adjacent heart with interval target has an interval source.

theorem CategoryTheory.Triangulated.Slicing.intervalProp_of_epi_rightHeart (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {a b : ℝ} (hab : a < b) {X Y : (toDualTStructure C (phaseShift C s (b - 1))).heart.FullSubcategory} (hX : intervalProp C s a b X.obj) (f : X ⟶ Y) [Epi f] : intervalProp C s a b Y.obj

An epimorphism in the right adjacent heart with interval source has an interval target.