The source slope cutoff of display (14.1)

The phase-cut torsion pair is convenient for slicing arguments, while display (14.1) of arXiv:1902.08184v4 is parametrized by a finite weak slope b : ℝ. This module supplies the exact adapter.

The normalized phase of the cutoff is

slopeCutPhase b = arctan b / pi + 1 / 2.

For a nonzero heart object, muPlus and muMinus are the slopes of the nonzero endpoint factors of a slicing HN filtration. Their normalized phases are the intrinsic slicing endpoints phiPlus and phiMinus; consequently the paper's classes {muMinus > b} and {muPlus <= b} are exactly P((slopeCutPhase b, 1]) and P((0, slopeCutPhase b]).

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakStabilityFunctionOnHeart_phase_eq_of_mem_P_phi {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) {phi : ℝ} (hphi : phi ∈ Set.Ioc 0 1) (E : C) (hP : sigma.slicing.P phi E) (hE : ¬Limits.IsZero E) : sigma.weakStabilityFunctionOnHeart.phase E = phi

On a nonzero slicing-semistable heart object, the normalized weak slope recovers its slicing phase, including the phase-1 boundary.

structure CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.ExtremalHNData {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (E : C) : Type (max u_1 u_3)

A slicing HN filtration whose first and last factors are nonzero. It is used only to name the source extremal slopes; their phase normalizations are proved independent of this choice below.

• filtration : HNFiltration C sigma.slicing.P E

  The chosen slicing HN filtration.

• n_pos : 0 < self.filtration.n

  The filtration has at least one factor.

• first_nonzero : ¬Limits.IsZero (self.filtration.triangle ⟨0, ⋯⟩).obj₃

  Its largest-phase endpoint factor is nonzero.

• last_nonzero : ¬Limits.IsZero (self.filtration.triangle ⟨self.filtration.n - 1, ⋯⟩).obj₃

  Its smallest-phase endpoint factor is nonzero.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.extremalHNData {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (E : C) (hE : ¬Limits.IsZero E) : sigma.ExtremalHNData E

Choose an HN filtration with nonzero endpoint factors.

Equations

• sigma.extremalHNData E hE = { filtration := Classical.choose ⋯, n_pos := ⋯, first_nonzero := ⋯, last_nonzero := ⋯ }

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.muPlus {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (E : C) (hE : ¬Limits.IsZero E) : WithTop ℝ

The maximal HN slope muPlus of a nonzero heart object.

Equations

• sigma.muPlus E hE = sigma.weakStabilityFunctionOnHeart.slope ((sigma.extremalHNData E hE).filtration.triangle ⟨0, ⋯⟩).obj₃

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.muMinus {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (E : C) (hE : ¬Limits.IsZero E) : WithTop ℝ

The minimal HN slope muMinus of a nonzero heart object.

Equations

• sigma.muMinus E hE = sigma.weakStabilityFunctionOnHeart.slope ((sigma.extremalHNData E hE).filtration.triangle ⟨(sigma.extremalHNData E hE).filtration.n - 1, ⋯⟩).obj₃

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakPhaseOfSlope_muPlus {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (E : C) (hheart : (Slicing.toTStructure C sigma.slicing).heart E) (hE : ¬Limits.IsZero E) : weakPhaseOfSlope (sigma.muPlus E hE) = Slicing.phiPlus C sigma.slicing E hE

The normalized phase of muPlus is the intrinsic largest slicing phase.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakPhaseOfSlope_muMinus {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (E : C) (hheart : (Slicing.toTStructure C sigma.slicing).heart E) (hE : ¬Limits.IsZero E) : weakPhaseOfSlope (sigma.muMinus E hE) = Slicing.phiMinus C sigma.slicing E hE

The normalized phase of muMinus is the intrinsic smallest slicing phase.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slopeCutPhase (b : ℝ) : ℝ

Convert a finite weak-slope cutoff to the normalized phase interval.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slopeCutPhase b = CategoryTheory.Triangulated.WeakStabilityCondition.weakPhaseOfSlope ↑b

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slopeCutPhase_mem_Ioo (b : ℝ) : slopeCutPhase b ∈ Set.Ioo 0 1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.muMinus_gt_iff_phiMinus_gt {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (b : ℝ) (E : C) (hheart : (Slicing.toTStructure C sigma.slicing).heart E) (hE : ¬Limits.IsZero E) : ↑b < sigma.muMinus E hE ↔ slopeCutPhase b < Slicing.phiMinus C sigma.slicing E hE

The source inequality muMinus(E) > b is the strict lower phase bound at slopeCutPhase b.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.muPlus_le_iff_phiPlus_le {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (b : ℝ) (E : C) (hheart : (Slicing.toTStructure C sigma.slicing).heart E) (hE : ¬Limits.IsZero E) : sigma.muPlus E hE ≤ ↑b ↔ Slicing.phiPlus C sigma.slicing E hE ≤ slopeCutPhase b

The source inequality muPlus(E) <= b is the upper phase bound at slopeCutPhase b.

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slopeTors {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (b : ℝ) : ObjectProperty C

The source torsion class {E | muMinus(E) > b}.

Equations

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

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slopeFree {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (b : ℝ) : ObjectProperty C

The source torsion-free class {E | muPlus(E) <= b}.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slopeTors_iff_phaseTors {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (b : ℝ) (E : C) : sigma.slopeTors b E ↔ phaseTors sigma.slicing (slopeCutPhase b) E

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slopeFree_iff_phaseFree {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (b : ℝ) (E : C) : sigma.slopeFree b E ↔ phaseFree sigma.slicing (slopeCutPhase b) E

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slopeTorsionPair {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (b : ℝ) : Tilting.HeartTorsionPair (Slicing.toTStructure C sigma.slicing)

The torsion pair of display (14.1), parametrized by its real slope cutoff.

Equations

• sigma.slopeTorsionPair b = CategoryTheory.Triangulated.WeakStabilityCondition.slicingTorsionPair sigma.slicing ⋯ ⋯

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slopeTorsionPair_tors {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (b : ℝ) : (sigma.slopeTorsionPair b).tors = sigma.slopeTors b

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slopeTorsionPair_free {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (b : ℝ) : (sigma.slopeTorsionPair b).free = sigma.slopeFree b

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slopeTilt_heart_iff {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (sigma : WeakPreStabilityCondition v) (b : ℝ) (X : C) : (sigma.slopeTorsionPair b).tilt.heart X ↔ ∃ (F : C) (T : C) (_ : sigma.slopeFree b F) (_ : sigma.slopeTors b T) (f : (shiftFunctor C 1).obj F ⟶ X) (g : X ⟶ T) (d : T ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj F)), Pretriangulated.Triangle.mk f g d ∈ Pretriangulated.distinguishedTriangles

The exact source-slope version of the tilted-heart identification in display (14.1).