Separation for the full stability distance

The three-coordinate distance determines the slicing and every charge visible through the class map. More precisely, distance zero implies equality of the two slicings and of the composites Z.comp v : K₀ C →+ ℂ.

For StabilityCondition.WithClassMap C v, literal equality of the stored central charges on Λ additionally requires v to be surjective. Some hypothesis is genuinely needed — the distance only ever evaluates the charge on classes in the image of v, so nothing constrains the two charges off that image. Surjectivity is sufficient, not necessary: since ℂ is torsion-free, Λ / range v being torsion already suffices. Surjectivity is used because it is the hypothesis the (Λ, v) literature carries by definition. In the ordinary specialization StabilityCondition C, the class map is the identity and separation is unconditional.

theorem CategoryTheory.Triangulated.stabilityDistTerm_eq_zero_of_eq_zero {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} (hd : stabilityDist σ τ = 0) (E : C) (hE : ¬Limits.IsZero E) : stabilityDistTerm σ τ E hE = 0

Every objectwise term vanishes when the full distance vanishes.

theorem CategoryTheory.Triangulated.phiPlus_eq_of_stabilityDist_eq_zero {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} (hd : stabilityDist σ τ = 0) (E : C) (hE : ¬Limits.IsZero E) : Slicing.phiPlus C σ.slicing E hE = Slicing.phiPlus C τ.slicing E hE

Distance zero identifies the intrinsic highest phase of every nonzero object.

theorem CategoryTheory.Triangulated.phiMinus_eq_of_stabilityDist_eq_zero {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} (hd : stabilityDist σ τ = 0) (E : C) (hE : ¬Limits.IsZero E) : Slicing.phiMinus C σ.slicing E hE = Slicing.phiMinus C τ.slicing E hE

Distance zero identifies the intrinsic lowest phase of every nonzero object.

theorem CategoryTheory.Triangulated.stabilityMass_toReal_eq_of_stabilityDist_eq_zero {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} (hd : stabilityDist σ τ = 0) (E : C) (hE : ¬Limits.IsZero E) : (stabilityMass σ E).toReal = (stabilityMass τ E).toReal

The mass coordinate of a nonzero object agrees at distance zero.

theorem CategoryTheory.Triangulated.stabilityMass_toReal_eq_norm_charge {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} {φ : ℝ} (hP : σ.slicing.P φ E) : (stabilityMass σ E).toReal = ‖σ.charge E‖

A semistable object's real mass is the norm of its charge.

theorem CategoryTheory.Triangulated.slicing_eq_of_stabilityDist_eq_zero {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} (hd : stabilityDist σ τ = 0) : σ.slicing = τ.slicing

Distance zero identifies the two slicings.

theorem CategoryTheory.Triangulated.charge_eq_of_stabilityDist_eq_zero {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} (hd : stabilityDist σ τ = 0) (E : C) : σ.charge E = τ.charge E

Distance zero identifies the charge of every object. This statement does not require surjectivity of the class map.

theorem CategoryTheory.Triangulated.charge_comp_eq_of_stabilityDist_eq_zero {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} (hd : stabilityDist σ τ = 0) : σ.Z.comp v = τ.Z.comp v

Unconditionally, distance zero identifies the observable central charge Z ∘ v on K₀ C.

theorem CategoryTheory.Triangulated.stabilityDist_eq_zero {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} (hv : Function.Surjective ⇑v) (hd : stabilityDist σ τ = 0) : σ = τ

For a surjective class map, the full stability distance separates points.

theorem CategoryTheory.Triangulated.stabilityDist_eq_zero_iff {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} (hv : Function.Surjective ⇑v) : stabilityDist σ τ = 0 ↔ σ = τ

Identity of indiscernibles for a surjective class map.

Deliberately NOT @[simp]: Function.Surjective v is not equation-theorem shaped, so simp's default discharger never consults the context, and Function.surjective_id is not itself @[simp] -- the rewrite would be inert even at v = id. The unconditional stabilityConditionDist_eq_zero_iff below carries the attribute instead.

theorem CategoryTheory.Triangulated.stabilityConditionDist_eq_zero {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {σ τ : StabilityCondition C} (hd : stabilityDist σ τ = 0) : σ = τ

The ordinary stability distance on charges over K₀ C separates points without an additional hypothesis.

@[simp]

theorem CategoryTheory.Triangulated.stabilityConditionDist_eq_zero_iff {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {σ τ : StabilityCondition C} : stabilityDist σ τ = 0 ↔ σ = τ

Identity of indiscernibles for ordinary stability conditions.