Orbit spaces of stability conditions

This file packages the topological orbit spaces of the three symmetry groups acting on a Bridgeland stability space: compatible autoequivalences, the combined lifted-linear/autoequivalence group, and its effective quotient.

The topology on every orbit space is the ordinary coinduced topology on MulAction.orbitRel.Quotient. Mathlib's general theorem for continuous group actions therefore makes each orbit projection a continuous open quotient map. The connected-component labelling descends equivariantly to orbit spaces.

Finally, autoequivalence orbits map continuously and surjectively to combined orbits, while the combined and effective actions have exactly the same orbits and hence homeomorphic orbit spaces. No separation, proper-discontinuity, or covering-space property is asserted here.

Connected-component labels on orbit spaces

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.ComponentOrbitSpace (G : Type uG) (X : Type uX) [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] : Type uX

The orbit space of connected-component labels induced by a continuous group action on X.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.ComponentOrbitSpace G X = MulAction.orbitRel.Quotient G (ConnectedComponents X)

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentOrbitMap {G : Type uG} {X : Type uX} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] : MulAction.orbitRel.Quotient G X → ComponentOrbitSpace G X

Connected-component labelling descends from points to their group orbits.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentOrbitMap = Quotient.map ConnectedComponents.mk ⋯

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentOrbitMap_mk {G : Type uG} {X : Type uX} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] (x : X) : componentOrbitMap (Quotient.mk'' x) = Quotient.mk'' (ConnectedComponents.mk x)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.continuous_componentOrbitMap {G : Type uG} {X : Type uX} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] : Continuous componentOrbitMap

The descended connected-component labelling is continuous for the quotient topologies.

Stability-condition orbit spaces

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.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 →+ Λ) : Type (max u' u)

Stability conditions modulo compatible autoequivalences.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.CombinedOrbitSpace {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 →+ Λ) : Type (max u' u)

Stability conditions modulo the combined lifted-linear and autoequivalence action.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.EffectiveCombinedOrbitSpace {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 →+ Λ) : Type (max u' u)

Stability conditions modulo the effective combined symmetry group.

Equations

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.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 →+ Λ} : StabilityCondition.WithClassMap C v → AutPairOrbitSpace v

The projection to compatible-autoequivalence orbits.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.autPairOrbitMap σ = ⟦σ⟧

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedOrbitMap {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 → CombinedOrbitSpace v

The projection to combined-symmetry orbits.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedOrbitMap σ = ⟦σ⟧

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.effectiveCombinedContinuousConstSMul {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 →+ Λ} : ContinuousConstSMul (EffectiveCombinedSymmetry v) (StabilityCondition.WithClassMap C v)

The effective combined action is continuous in the stability-condition variable for each fixed symmetry class.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.effectiveCombinedOrbitMap {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 → EffectiveCombinedOrbitSpace v

The projection to effective-combined-symmetry orbits.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.effectiveCombinedOrbitMap σ = ⟦σ⟧

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.isOpenQuotientMap_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 →+ Λ} : IsOpenQuotientMap autPairOrbitMap

The compatible-autoequivalence orbit projection is a continuous open quotient map.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.isOpenQuotientMap_combinedOrbitMap {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 →+ Λ} : IsOpenQuotientMap combinedOrbitMap

The combined-symmetry orbit projection is a continuous open quotient map.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.isOpenQuotientMap_effectiveCombinedOrbitMap {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 →+ Λ} : IsOpenQuotientMap effectiveCombinedOrbitMap

The effective-combined-symmetry orbit projection is a continuous open quotient map.

Comparison of the three orbit spaces

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.autPairToCombinedOrbitMap {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 →+ Λ} : AutPairOrbitSpace v → CombinedOrbitSpace v

Forgetting that an orbit was generated only by compatible autoequivalences gives its combined-symmetry orbit.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.autPairToCombinedOrbitMap = Quotient.map id ⋯

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.autPairToCombinedOrbitMap_mk {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) : autPairToCombinedOrbitMap (Quotient.mk'' σ) = Quotient.mk'' σ

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.continuous_autPairToCombinedOrbitMap {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 →+ Λ} : Continuous autPairToCombinedOrbitMap

The comparison from autoequivalence orbits to combined orbits is continuous.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.surjective_autPairToCombinedOrbitMap {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 →+ Λ} : Function.Surjective autPairToCombinedOrbitMap

Every combined orbit is the image of an autoequivalence orbit.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedOrbitRel_iff_effectiveCombinedOrbitRel {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) : (MulAction.orbitRel (GLTilde × AutPairQuot v) (StabilityCondition.WithClassMap C v)) σ τ ↔ (MulAction.orbitRel (EffectiveCombinedSymmetry v) (StabilityCondition.WithClassMap C v)) σ τ

Passing from the combined group to its quotient by the action kernel does not change the orbit relation on the stability space.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedEffectiveOrbitHomeomorph {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 →+ Λ} : CombinedOrbitSpace v ≃ₜ EffectiveCombinedOrbitSpace v

Combined and effective symmetries have homeomorphic orbit spaces because quotienting the group by the full action kernel leaves every orbit unchanged.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedEffectiveOrbitHomeomorph = Homeomorph.Quotient.congrRight ⋯

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedEffectiveOrbitHomeomorph_mk {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) : combinedEffectiveOrbitHomeomorph (Quotient.mk'' σ) = Quotient.mk'' σ