Support property for weak stability and transport across a phase tilt

This file binds the generic linear-algebraic support predicate from WeakStabilityCondition/Support/Predicate/Basic.lean to the numerical classes of nonzero weak semistable heart objects. It then proves the support-property transport used in Proposition 14.16.

The proof follows Remark 14.9 and Lemma 14.17. An original zero-charge object is weak semistable, so the original support property forces its numerical class to vanish. The tilted classification then says that a nonzero-charge tilted semistable class is either an original semistable class or the negative of one, up to such a zero class. Finally, multiplication of the charge by exp (-pi * beta * I) preserves its norm.

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.semistableClasses {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [NormedAddCommGroup V] {t : TStructure C} (W : WeakStabilityFunction t) (v : K₀ C →+ V) : Set V

Numerical classes of nonzero weak-semistable objects in the heart.

Equations

• W.semistableClasses v = {x : V | ∃ (E : C), W.IsSemistable E ∧ ¬CategoryTheory.Limits.IsZero E ∧ x = v (CategoryTheory.Triangulated.K₀.of C E)}

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.HasSupportProperty {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : TStructure C} (W : WeakStabilityFunction t) (v : K₀ C →+ V) (Zlin : V →ₗ[ℝ] ℂ) : Prop

The support property for a weak stability function, relative to a real linear realization of its charge.

Equations

• W.HasSupportProperty v Zlin = CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasSupportProperty Zlin (W.semistableClasses v)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.isSemistable_of_zeroCharge {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) {E : C} (hE : W.zeroCharge E) : W.IsSemistable E

A zero-charge object is weak semistable.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.class_eq_zero_of_zeroCharge {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} {t : TStructure C} (W : WeakStabilityFunction t) (Zlin : V →ₗ[ℝ] ℂ) (hcompat : ∀ (k : K₀ C), Zlin (v k) = W.Z k) (hsupport : W.HasSupportProperty v Zlin) {E : C} (hE : W.zeroCharge E) : v (K₀.of C E) = 0

Under the support property, every zero-charge heart object has zero numerical class. This is the weak-stability form of Remark 14.9.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.phaseTiltLinearCharge {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (beta : ℝ) (Zlin : V →ₗ[ℝ] ℂ) : V →ₗ[ℝ] ℂ

The real-linear rotation of a charge used by the phase tilt.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.phaseTiltLinearCharge beta Zlin = LinearMap.mulLeft ℝ (Complex.exp (↑(-(Real.pi * beta)) * Complex.I)) ∘ₗ Zlin

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.phaseTiltLinearCharge_apply {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (beta : ℝ) (Zlin : V →ₗ[ℝ] ℂ) (x : V) : (phaseTiltLinearCharge beta Zlin) x = Zlin x * Complex.exp (-(↑Real.pi * ↑beta) * Complex.I)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.norm_phaseTiltLinearCharge {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (beta : ℝ) (Zlin : V →ₗ[ℝ] ℂ) (x : V) : ‖(phaseTiltLinearCharge beta Zlin) x‖ = ‖Zlin x‖

Rotating a complex charge does not change its norm.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTilt_hasSupportProperty {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] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1) (Zlin : V →ₗ[ℝ] ℂ) (hcompat : ∀ (x : V), Zlin x = sigma.Z x) (hsupport : sigma.weakStabilityFunctionOnHeart.HasSupportProperty v Zlin) : (sigma.phaseTiltWeakStabilityFunction beta ⋯ hbeta1).HasSupportProperty v (phaseTiltLinearCharge beta Zlin)

Support-property transport across the phase tilt.

For a cutoff strictly inside (0, 1), the support property of the original heart weak function implies the support property of the rotated weak function on the tilted heart. The same comparison constant works.