Transport of connected components by symmetries

A group acting continuously, element by element, on a topological space also acts on its connected-component set. This file packages that general fact and then applies it to the three symmetry groups already acting on the Bridgeland stability space:

• GLTilde;
• AutPairQuot v;
• GLTilde × AutPairQuot v.

The resulting action is not merely a permutation of component labels. Each group element restricts to a homeomorphism from one component subtype to the component subtype carrying the translated label. The stabilizer of a label therefore acts on the corresponding component itself.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentSmul {G : Type u} {X : Type v} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] (g : G) (cc : ConnectedComponents X) : ConnectedComponents X

The action induced on connected-component labels by a continuous group action.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentSmul g cc = ⋯.connectedComponentsMap cc

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentSmul_mk {G : Type u} {X : Type v} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] (g : G) (x : X) : componentSmul g (ConnectedComponents.mk x) = ConnectedComponents.mk (g • x)

@[implicit_reducible]

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentMulAction {G : Type u} {X : Type v} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] : MulAction G (ConnectedComponents X)

Functoriality of connected components turns the original group action into an action on component labels.

scoped. Stated at full generality, in a domain-specific namespace, for a class pairing (MulAction/ConnectedComponents) that Mathlib does not equip at this pin. If it is ever upstreamed, an unscoped copy here becomes a second instance for the same class and type.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.image_connectedComponent_smul {G : Type u} {X : Type v} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] (g : G) (x : X) : (fun (y : X) => g • y) '' connectedComponent x = connectedComponent (g • x)

A symmetry maps the connected component of x exactly onto the connected component of g • x. Continuity gives one inclusion; applying the inverse symmetry gives the other.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentHomeomorph {G : Type u} {X : Type v} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] (g : G) (cc : ConnectedComponents X) : { x : X // ConnectedComponents.mk x = cc } ≃ₜ { x : X // ConnectedComponents.mk x = componentSmul g cc }

Restriction of a symmetry to a homeomorphism between the corresponding connected-component subtypes.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentHomeomorph g cc = (Homeomorph.smul g).subtype ⋯

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentHomeomorph_apply_coe {G : Type u} {X : Type v} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] (g : G) (cc : ConnectedComponents X) (x : { x : X // ConnectedComponents.mk x = cc }) : ↑((componentHomeomorph g cc) x) = g • ↑x

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentStabilizer {G : Type u} {X : Type v} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] (cc : ConnectedComponents X) : Subgroup G

The subgroup preserving a chosen connected component.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentStabilizer cc = MulAction.stabilizer G cc

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.mem_componentStabilizer_iff {G : Type u} {X : Type v} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] {cc : ConnectedComponents X} {g : G} : g ∈ componentStabilizer cc ↔ g • cc = cc

@[implicit_reducible]

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.componentStabilizerMulAction {G : Type u} {X : Type v} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] (cc : ConnectedComponents X) : MulAction ↥(componentStabilizer cc) { x : X // ConnectedComponents.mk x = cc }

The component stabilizer acts on the corresponding component subtype.

scoped for the same reason as componentMulAction above.

Equations

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