Proper discontinuity of the autoequivalence action

This file isolates the geometric and topological input needed to treat the compatible-autoequivalence action on a Bridgeland stability space as properly discontinuous. At the generality of StabilityCondition.WithClassMap C v, that input is not a theorem: it is packaged explicitly in ProperDiscontinuityData.

From the supplied data we derive finite point stabilizers, the standard local neighbourhood consequences, Hausdorff separation of the orbit space, and the covering-map statement over the image of the free locus. The last result is deliberately restricted. Proper discontinuity makes point stabilizers finite, but does not make the action free, so it does not imply an unrestricted covering map.

The finite-stabilizer theorem below takes only the first field's Mathlib class. The local and quotient consequences install the surjectivity-derived Hausdorff instance and local compactness, while consuming the canonical continuous constant-action instance from the combined-topology layer; keeping that split visible prevents an accidental strengthening of the supplied geometric interface.

Missing geometric input

No inhabitant of ProperDiscontinuityData is constructed here. A geometric construction would require arithmetic control of the image of compatible autoequivalences in lattice isometries, local finiteness for the corresponding walls on the stability space, and finite-dimensionality sufficient to deduce local compactness. Those inputs are absent from the generic stability API.

Proper discontinuity here gives finite stabilizers of individual stability conditions, but does not by itself give finiteness of a chamber's setwise stabilizer. A chamber-level statement needs a specified chamber action and additional control of that action; none is asserted here.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.ProperDiscontinuityData {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 →+ Λ) : Prop

External input asserting proper discontinuity and the two hypotheses needed for its Hausdorff-local consequences on the stability space.

• properlyDiscontinuous : ProperlyDiscontinuousSMul (AutPairQuot v) (StabilityCondition.WithClassMap C v)

  The compatible-autoequivalence action is properly discontinuous.

• surjective : Function.Surjective ⇑v

  The class map is surjective, so the installed stability topology is Hausdorff.

• locallyCompact : LocallyCompactSpace (StabilityCondition.WithClassMap C v)

  The stability space is locally compact. This does not follow from the current local-homeomorphism API without a finite-dimensionality input.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.finite_stabilizer_of_properlyDiscontinuousSMul {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 →+ Λ} (h : ProperlyDiscontinuousSMul (AutPairQuot v) (StabilityCondition.WithClassMap C v)) (σ : StabilityCondition.WithClassMap C v) : (↑(MulAction.stabilizer (AutPairQuot v) σ)).Finite

Proper discontinuity alone makes every point stabilizer finite.

This helper intentionally takes the Mathlib class directly: surjectivity and local compactness are not needed for the point-stabilizer consequence.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.ProperDiscontinuityData.finite_stabilizer {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 →+ Λ} (d : ProperDiscontinuityData v) (σ : StabilityCondition.WithClassMap C v) : (↑(MulAction.stabilizer (AutPairQuot v) σ)).Finite

Compatibility wrapper for clients that already hold the complete external data bundle. Use finite_stabilizer_of_properlyDiscontinuousSMul when only proper discontinuity is available.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.ProperDiscontinuityData.exists_nhds_image_smul_eq_self {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 →+ Λ} (d : ProperDiscontinuityData v) (σ : StabilityCondition.WithClassMap C v) : ∃ U ∈ nhds σ, ∀ (q : AutPairQuot v), ((fun (x : StabilityCondition.WithClassMap C v) => q • x) '' U ∩ U).Nonempty → q • σ = σ

Every stability condition has a neighbourhood whose translates can meet it only under elements fixing the original point.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.ProperDiscontinuityData.exists_nhds_disjoint_image {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 →+ Λ} (d : ProperDiscontinuityData v) (σ : StabilityCondition.WithClassMap C v) : ∃ U ∈ nhds σ, ∀ (q : AutPairQuot v), q • σ ≠ σ → Disjoint ((fun (x : StabilityCondition.WithClassMap C v) => q • x) '' U) U

Every stability condition has a neighbourhood disjoint from each translate whose group element does not fix the original point.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.ProperDiscontinuityData.t2Space_autPairOrbitSpace {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 →+ Λ} (d : ProperDiscontinuityData v) : T2Space (AutPairOrbitSpace v)

A properly discontinuous compatible-autoequivalence quotient is Hausdorff under the supplied local-compactness and surjectivity inputs.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.ProperDiscontinuityData.isCoveringMapOn_autPairOrbitMap {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 →+ Λ} (d : ProperDiscontinuityData v) : IsCoveringMapOn autPairOrbitMap (autPairOrbitMap '' {σ : StabilityCondition.WithClassMap C v | MulAction.stabilizer (AutPairQuot v) σ = ⊥})

The compatible-autoequivalence orbit projection is a covering map over the image of the free locus. No covering claim is made at points with nontrivial stabilizer.