Hausdorff separation for the stability space

For a surjective class map v : K₀ C →+ Λ, the space StabilityCondition.WithClassMap C v is T0 and T2 for the topology it already carries -- the Section 6 topology generated by basisNhd and installed as StabilityCondition.WithClassMap.topologicalSpace.

The whole content is one rfl

Metric/Distance/Topology.lean builds the extended-metric package stabilityEMetricSpaceOfMassTriangle hv htriangle and proves that the topology it induces is the installed one, definitionally (stabilityEMetricSpace_toTopologicalSpace). The mass-triangle premise is discharged unconditionally by stabilityMassTriangleInequality, with no hypothesis beyond the ambient [IsTriangulated C]. So every proof below opens with

letI := stabilityEMetricSpaceOfMassTriangle hv stabilityMassTriangleInequality

and then reads Mathlib's separation instances for the metric topology off as statements about the installed topology, because the two are the same term. EMetricSpace forgets to PseudoEMetricSpace, to UniformSpace, to the already-installed TopologicalSpace; that last step is rfl, and stabilityEMetricSpaceOfMassTriangle_toTopologicalSpace pins it once more so that a later refactor cannot silently retarget these statements at a fresh metric topology.

What is deliberately not here

• No global instance. No TopologicalSpace, UniformSpace, EMetricSpace or MetricSpace instance is installed on WithClassMap C v, and no new member joins the stabilityEMetricSpace definition family: stabilityEMetricSpaceOfMassTriangle already exists, and an OfSurjective alias would be a third @[reducible] definition equal to it.
• No separation without surjectivity. stabilityDist only sees charges on Set.range v, so two stability conditions differing on a class outside the range are at distance zero; this is why stabilityDist_eq_zero takes hv, and why every statement here does.
• No local compactness, no completeness. Nothing here needs either; the autoequivalence lane carries local compactness as a hypothesis.

theorem CategoryTheory.Triangulated.stabilityEMetricSpaceOfMassTriangle_toTopologicalSpace {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 →+ Λ} (hv : Function.Surjective ⇑v) : PseudoEMetricSpace.toUniformSpace.toTopologicalSpace = inferInstance

Regression pin. The topology of the unconditional extended-metric package is the installed Section 6 topology, definitionally. Every separation statement below is about the right-hand side.

theorem CategoryTheory.Triangulated.t0Space_withClassMap {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 →+ Λ} (hv : Function.Surjective ⇑v) : T0Space (StabilityCondition.WithClassMap C v)

The stability space is T0 for its installed topology, when the class map is surjective: EMetricSpace.instT0Space for the metric topology, which is the installed one.

theorem CategoryTheory.Triangulated.t2Space_withClassMap {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 →+ Λ} (hv : Function.Surjective ⇑v) : T2Space (StabilityCondition.WithClassMap C v)

The stability space is Hausdorff for its installed topology, when the class map is surjective: T0 together with the R1Space every pseudo-extended-metric topology has.

theorem CategoryTheory.Triangulated.isClosed_singleton_withClassMap {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 →+ Λ} (hv : Function.Surjective ⇑v) (σ : StabilityCondition.WithClassMap C v) : IsClosed {σ}

Points of the stability space are closed.

theorem CategoryTheory.Triangulated.isClosed_diagonal_withClassMap {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 →+ Λ} (hv : Function.Surjective ⇑v) : IsClosed (Set.diagonal (StabilityCondition.WithClassMap C v))

The diagonal of the stability space is closed.