The tilted heart and its weak stability function

This file owns the sign facts for the rotated charge of an object whose old slicing phases lie in the tilted window, the identification of the HRS-tilted heart by that phase interval, its agreement with the phase-shifted heart, and the construction of the weak stability function the tilted heart carries. Its charge is the original charge rotated clockwise through pi * beta.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.rotatedCharge_cross_ray_nonneg_of_bounds {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) {beta theta n : ℝ} {A : C} (hn : 0 ≤ n) (htheta : theta ≤ 1) (hgt : Slicing.gtProp C sigma.slicing beta A) (hle : Slicing.leProp C sigma.slicing (beta + theta) A) : 0 ≤ cross (sigma.Z (v (K₀.of C A)) * Complex.exp (-(↑Real.pi * ↑beta) * Complex.I)) (↑n * Complex.exp (↑(Real.pi * theta) * Complex.I))

For an object whose old slicing phases lie in the tilted window, the cross product of its rotated charge against a fixed ray is nonnegative.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltHeart_interval {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] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) {beta : ℝ} (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) {E : C} (hE : (slicingTorsionPair sigma.slicing hbeta0 ⋯).tilt.heart E) : Slicing.gtProp C sigma.slicing beta E ∧ Slicing.leProp C sigma.slicing (beta + 1) E

A tilted-heart object has all old slicing phases in (beta, beta + 1]. This is the sector form of the HRS heart description.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseFree_of_tiltHeart_triangle {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] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) {beta : ℝ} (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) {U V E : C} (hE : (slicingTorsionPair sigma.slicing hbeta0 ⋯).tilt.heart E) (hUheart : (Slicing.toTStructure C sigma.slicing).heart U) (hVheart : (Slicing.toTStructure C sigma.slicing).heart V) {f : (shiftFunctor C 1).obj U ⟶ E} {g : E ⟶ V} {d : V ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj U)} (hdist : Pretriangulated.Triangle.mk f g d ∈ Pretriangulated.distinguishedTriangles) : phaseFree sigma.slicing beta U

The free-class field of case (2) of Lemma 14.17 is automatic.

If E lies in the tilted heart and sits in a distinguished triangle U⟦1⟧ ⟶ E ⟶ V whose outer terms lie in the original heart, then U lies in the phase-cut free class P((0, beta]).

The printed case (2) of Lemma 14.17 (arXiv:1902.08184v4, page 74) asks only that U be an object of the original heart. This lemma supplies the free-class membership the constructive direction consumes, so that it need not be carried as an extra hypothesis of IsPhaseTiltTypeTwo.

The argument is the phase interval alone: E is bounded above by beta + 1 and V⟦-1⟧ is bounded above by 0, so inverse rotation bounds the middle term U⟦1⟧ of V⟦-1⟧ ⟶ U⟦1⟧ ⟶ E by beta + 1.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltHeart_iff_phaseShiftHeart {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] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) {beta : ℝ} (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) (E : C) : (slicingTorsionPair sigma.slicing hbeta0 ⋯).tilt.heart E ↔ (Slicing.toTStructure C (Slicing.phaseShift C sigma.slicing beta)).heart E

The HRS tilt at the phase cut is exactly the heart of the phase-shifted slicing. This identifies both descriptions with the interval P((beta, beta + 1]).

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltWeakStabilityFunction {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] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) : WeakStabilityFunction (slicingTorsionPair sigma.slicing hbeta0 ⋯).tilt

The phase-language tilted weak stability function. Its heart is the HRS tilt at the cutoff beta, and its charge is the original charge rotated clockwise through pi * beta.

Equations

• sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1 = { Z := sigma.phaseTiltCharge beta, nonzero_mem := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltWeakStabilityFunction_Z {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] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).Z = sigma.phaseTiltCharge beta

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltWeakStabilityFunction_charge {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] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 ≤ beta) (hbeta1 : beta < 1) (E : C) : (sigma.phaseTiltWeakStabilityFunction beta hbeta0 hbeta1).charge E = sigma.Z (v (K₀.of C E)) * Complex.exp (-(↑Real.pi * ↑beta) * Complex.I)