The three-coordinate stability distance

This file adds the mass coordinate to the two-coordinate slicingDist of WeakStabilityCondition/StabilityCondition/Foundation/Deformation/SlicingDistance.lean. For every nonzero object it takes the maximum of

• the φ⁺ discrepancy;
• the φ⁻ discrepancy;
• the logarithmic discrepancy of the HN masses.

The supremum of those objectwise terms is an ℝ≥0∞-valued symmetric extended pseudodistance and satisfies the triangle inequality.

WeakStabilityCondition/StabilityCondition/Metric/Mass/Uniqueness.lean proves that the choice-free definition of stabilityMass is equal to the finite mass sum of every HN filtration. logMassDist is nevertheless defined on all of ℝ≥0∞: it places ⊤ at infinite distance from finite values and at distance zero from itself. On the positive finite masses occurring here it is exactly |log m₁ - log m₂|, equivalently the absolute log-ratio used by Bridgeland.

noncomputable def CategoryTheory.Triangulated.logMassDist (m n : ENNReal) : ENNReal

Extended absolute logarithmic distance on ℝ≥0∞.

Finite inputs use the ordinary real logarithm. ⊤ is infinitely far from every finite input and zero distance from itself.

The 0 input is not a distance. ENNReal.toReal 0 = 0 and Real.log 0 = 0, so this function reads mass 0 as mass 1: logMassDist 0 1 is 0, and logMassDist 0 n is finite where the true value is +∞. That is unreachable in this development and deliberately not guarded against — every application is to stabilityMass, which stabilityMass_pos and stabilityMass_ne_top pin inside (0, ⊤), and stabilityDist takes its supremum only over ¬IsZero E. Do not reuse this function on a mass that has not been shown nonzero.

Equations

• CategoryTheory.Triangulated.logMassDist m n = if m = ⊤ then if n = ⊤ then 0 else ⊤ else if n = ⊤ then ⊤ else ENNReal.ofReal |Real.log m.toReal - Real.log n.toReal|

@[simp]

theorem CategoryTheory.Triangulated.logMassDist_self (m : ENNReal) : logMassDist m m = 0

theorem CategoryTheory.Triangulated.logMassDist_comm (m n : ENNReal) : logMassDist m n = logMassDist n m

theorem CategoryTheory.Triangulated.logMassDist_triangle (m n k : ENNReal) : logMassDist m k ≤ logMassDist m n + logMassDist n k

The extended logarithmic discrepancy satisfies the triangle inequality.

theorem CategoryTheory.Triangulated.logMassDist_eq_of_ne_top {m n : ENNReal} (hm : m ≠ ⊤) (hn : n ≠ ⊤) : logMassDist m n = ENNReal.ofReal |Real.log m.toReal - Real.log n.toReal|

On finite inputs, logMassDist is the ordinary absolute logarithmic difference.

noncomputable def CategoryTheory.Triangulated.phiPlusDist {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : ENNReal

The φ⁺ coordinate discrepancy for a fixed nonzero object.

Equations

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

noncomputable def CategoryTheory.Triangulated.phiMinusDist {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : ENNReal

The φ⁻ coordinate discrepancy for a fixed nonzero object.

Equations

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

noncomputable def CategoryTheory.Triangulated.massDist {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) : ENNReal

The logarithmic mass coordinate discrepancy for a fixed object.

Equations

• CategoryTheory.Triangulated.massDist σ τ E = CategoryTheory.Triangulated.logMassDist (CategoryTheory.Triangulated.stabilityMass σ E) (CategoryTheory.Triangulated.stabilityMass τ E)

noncomputable def CategoryTheory.Triangulated.stabilityDistTerm {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : ENNReal

The maximum of the two phase discrepancies and the mass discrepancy for one nonzero object.

Equations

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

noncomputable def CategoryTheory.Triangulated.stabilityDist {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) : ENNReal

The three-coordinate, ℝ≥0∞-valued stability distance.

Equations

• CategoryTheory.Triangulated.stabilityDist σ τ = ⨆ (E : C), ⨆ (hE : ¬CategoryTheory.Limits.IsZero E), CategoryTheory.Triangulated.stabilityDistTerm σ τ E hE

@[simp]

theorem CategoryTheory.Triangulated.phiPlusDist_self {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : phiPlusDist σ σ E hE = 0

@[simp]

theorem CategoryTheory.Triangulated.phiMinusDist_self {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : phiMinusDist σ σ E hE = 0

@[simp]

theorem CategoryTheory.Triangulated.massDist_self {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (E : C) : massDist σ σ E = 0

theorem CategoryTheory.Triangulated.phiPlusDist_comm {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : phiPlusDist σ τ E hE = phiPlusDist τ σ E hE

theorem CategoryTheory.Triangulated.phiMinusDist_comm {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : phiMinusDist σ τ E hE = phiMinusDist τ σ E hE

theorem CategoryTheory.Triangulated.massDist_comm {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) : massDist σ τ E = massDist τ σ E

theorem CategoryTheory.Triangulated.phiPlusDist_triangle {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ υ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : phiPlusDist σ υ E hE ≤ phiPlusDist σ τ E hE + phiPlusDist τ υ E hE

theorem CategoryTheory.Triangulated.phiMinusDist_triangle {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ υ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : phiMinusDist σ υ E hE ≤ phiMinusDist σ τ E hE + phiMinusDist τ υ E hE

theorem CategoryTheory.Triangulated.massDist_triangle {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ υ : StabilityCondition.WithClassMap C v) (E : C) : massDist σ υ E ≤ massDist σ τ E + massDist τ υ E

theorem CategoryTheory.Triangulated.massDist_eq_abs_log {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) : massDist σ τ E = ENNReal.ofReal |Real.log (stabilityMass σ E).toReal - Real.log (stabilityMass τ E).toReal|

The mass coordinate used by stabilityDist is always the ordinary finite absolute logarithmic difference.

theorem CategoryTheory.Triangulated.massDist_eq_abs_log_ratio {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : massDist σ τ E = ENNReal.ofReal |Real.log ((stabilityMass τ E).toReal / (stabilityMass σ E).toReal)|

Ratio form of the preceding theorem, matching the mass term in Bridgeland's formula.

@[simp]

theorem CategoryTheory.Triangulated.stabilityDist_self {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) : stabilityDist σ σ = 0

theorem CategoryTheory.Triangulated.stabilityDist_comm {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) : stabilityDist σ τ = stabilityDist τ σ

theorem CategoryTheory.Triangulated.stabilityDist_triangle {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ υ : StabilityCondition.WithClassMap C v) : stabilityDist σ υ ≤ stabilityDist σ τ + stabilityDist τ υ

The full stability distance satisfies the triangle inequality.

theorem CategoryTheory.Triangulated.stabilityDistTerm_le_stabilityDist {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : stabilityDistTerm σ τ E hE ≤ stabilityDist σ τ

Every objectwise three-coordinate term is bounded by the full stability distance. This is the basic elimination rule for the supremum defining stabilityDist.

theorem CategoryTheory.Triangulated.phiPlusDist_le_stabilityDist {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : phiPlusDist σ τ E hE ≤ stabilityDist σ τ

The positive-phase coordinate of an object is bounded by the full stability distance.

theorem CategoryTheory.Triangulated.phiMinusDist_le_stabilityDist {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : phiMinusDist σ τ E hE ≤ stabilityDist σ τ

The negative-phase coordinate of an object is bounded by the full stability distance.

theorem CategoryTheory.Triangulated.massDist_le_stabilityDist {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) (E : C) (hE : ¬Limits.IsZero E) : massDist σ τ E ≤ stabilityDist σ τ

The mass coordinate of an object is bounded by the full stability distance.

theorem CategoryTheory.Triangulated.slicingDist_le_stabilityDist {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ τ : StabilityCondition.WithClassMap C v) : slicingDist C σ.slicing τ.slicing ≤ stabilityDist σ τ

The phase-only slicingDist is bounded by the full three-coordinate distance.