Topology of charge-zero loci

For a lattice class in Set.range v, evaluation of the central charge is continuous on StabilityCondition.WithClassMap C v. Consequently, when v is surjective, each chargeZeroLocus is closed and a regular locus indexed by a finite set of classes is open.

Why the range hypothesis is necessary

The owner topology is generated by Deformation.basisNhd. Its charge coordinate is measured by Deformation.stabilitySeminorm, which evaluates a perturbation only on classes classOf C v E and hence only on Set.range v. Charges that agree on that range but differ outside it are therefore topologically indistinguishable. Evaluation at an arbitrary δ : Λ cannot be continuous without a range hypothesis; surjectivity is used below only to put every δ in the range.

For an object class, continuity follows directly from an HN filtration: the seminorm bounds the charge change on every semistable factor, and the Postnikov-tower identity sums those bounds. A general element of K₀ C need not be represented by a single object under the hypotheses of this file, so the proof extends from object classes by GrothendieckPresentation.induction_on rather than assuming such a representative exists.

The estimates are pointwise in the center stability condition. No uniform continuity or Lipschitz bound is asserted. Openness is proved only for finite sets of charge-zero loci; the corresponding result for an infinite family would require a local-finiteness input not present here.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.ChargeZero.continuous_chargeAt_of_mem_range {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 →+ Λ} {δ : Λ} (hδ : δ ∈ Set.range ⇑v) : Continuous fun (σ : StabilityCondition.WithClassMap C v) => σ.Z δ

Evaluation of the central charge at a class in the range of the class map is continuous on the stability space.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.ChargeZero.continuous_chargeAt {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 →+ Λ} (hv : Function.Surjective ⇑v) (δ : Λ) : Continuous fun (σ : StabilityCondition.WithClassMap C v) => σ.Z δ

Surjectivity makes every lattice class visible to the owner stability seminorm, so the range-level continuity theorem applies to every δ : Λ.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.ChargeZero.isClosed_chargeZeroLocus {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 →+ Λ} (hv : Function.Surjective ⇑v) (δ : Λ) : IsClosed (chargeZeroLocus δ)

For a surjective class map, the charge-zero locus of each lattice class is closed.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.ChargeZero.isOpen_chargeRegularLocus {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 →+ Λ} (hv : Function.Surjective ⇑v) {Δ : Set Λ} (hΔ : Δ.Finite) : IsOpen (chargeRegularLocus Δ)

For a surjective class map, the regular locus associated to finitely many lattice classes is open.