Continuous outer automorphisms acting on closed subgroups up to conjugacy

A continuous automorphism φ of a topological group G is a homeomorphism, so it carries a closed subgroup H to the closed subgroup φ • H, its image. This is an action of ContinuousAut G on Mathlib's ClosedSubgroup G. Through the inner automorphisms ContinuousAut.conj, the group G itself acts on its closed subgroups by conjugation; this is recorded as an action of Mathlib's ConjAct G, whose orbits are the conjugacy classes of closed subgroups, ClosedSubgroupConjClasses G.

A continuous automorphism carries conjugate closed subgroups to conjugate closed subgroups, because φ * conj g = conj (φ g) * φ, so the action descends to ClosedSubgroupConjClasses G. Inner automorphisms fix every class, so the action on classes factors through the continuous outer automorphism group ContinuousOut G. This is the action in which outer actions on profinite groups, such as an outer Galois action on a profinite fundamental group, are stated on closed subgroups (for instance decomposition and inertia groups), which are only defined up to conjugacy. The companion action on conjugacy classes of elements is in TauCeti.Topology.Algebra.Group.ContinuousAut.ConjClasses.

All actions here are algebraic: they need a topology on G to speak of continuous automorphisms and closed subgroups, but no topology on ContinuousAut G.

Main definitions

• The action of ContinuousAut G on ClosedSubgroup G by images, with ContinuousAut.smul_closedSubgroup_toSubgroup computing the underlying subgroup.
• The conjugation action of ConjAct G on ClosedSubgroup G, through ContinuousAut.conj (ConjAct.smul_closedSubgroup_eq_conj_smul), compatible with Mathlib's pointwise conjugation of subgroups (ConjAct.smul_closedSubgroup_toSubgroup).
• TauCeti.ClosedSubgroupConjClasses G: closed subgroups of G up to conjugacy, the orbit quotient of that action, with the class map TauCeti.ClosedSubgroupConjClasses.mk.
• The actions of ContinuousAut G and of ContinuousOut G on ClosedSubgroupConjClasses G.

Main results

• TauCeti.ClosedSubgroupConjClasses.mk_eq_mk_iff: two closed subgroups have the same class exactly when one is a conjugate of the other.
• TauCeti.ContinuousAut.smul_closedSubgroupConjClass: a continuous automorphism sends the class of H to the class of φ • H.
• TauCeti.ContinuousAut.conj_smul_closedSubgroupConjClasses: inner automorphisms fix every class.
• TauCeti.ContinuousOut.mk_smul_closedSubgroupConjClass: the class of φ in ContinuousOut G sends the class of H to the class of φ • H.

References

• L. Ribes, P. Zalesskii, Profinite Groups, 2nd ed., §4.4.

@[instance_reducible]

instance TauCeti.ContinuousAut.instMulActionClosedSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] : MulAction (ContinuousAut G) (ClosedSubgroup G)

A continuous automorphism acts on closed subgroups by taking images; the image is closed because a continuous automorphism is a homeomorphism.

theorem TauCeti.ContinuousAut.smul_closedSubgroup_def {G : Type u_1} [Group G] [TopologicalSpace G] (φ : ContinuousAut G) (H : ClosedSubgroup G) : φ • H = (ContinuousMulEquiv.closedSubgroupOrderIso φ) H

The action of a continuous automorphism on closed subgroups is transport along it by ContinuousMulEquiv.closedSubgroupOrderIso, so that API applies to it.

@[simp]

theorem TauCeti.ContinuousAut.smul_closedSubgroup_toSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] (φ : ContinuousAut G) (H : ClosedSubgroup G) : ↑(φ • H) = Subgroup.map φ.toMonoidHom ↑H

The underlying subgroup of φ • H is the image of H under φ.

@[simp]

theorem TauCeti.ContinuousAut.mem_smul_closedSubgroup_iff {G : Type u_1} [Group G] [TopologicalSpace G] {φ : ContinuousAut G} {H : ClosedSubgroup G} {x : G} : x ∈ φ • H ↔ (ContinuousMulEquiv.symm φ) x ∈ H

An element lies in φ • H exactly when its preimage under φ lies in H.

@[instance_reducible]

instance TauCeti.instMulActionConjActClosedSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : MulAction (ConjAct G) (ClosedSubgroup G)

The group acts on its closed subgroups by conjugation, through the continuous inner automorphisms ContinuousAut.conj.

@[simp]

theorem ConjAct.smul_closedSubgroup_eq_conj_smul {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (g : ConjAct G) (H : ClosedSubgroup G) : g • H = TauCeti.ContinuousAut.conj (ofConjAct g) • H

Conjugating a closed subgroup by g is acting on it by the inner automorphism conj g. This is the normal form: simp reduces the conjugation action to the action of continuous automorphisms.

theorem ConjAct.smul_closedSubgroup_toSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (g : ConjAct G) (H : ClosedSubgroup G) : ↑(g • H) = g • ↑H

Conjugating a closed subgroup is Mathlib's pointwise conjugation of the underlying subgroup.

theorem TauCeti.ContinuousAut.smul_conj_smul_closedSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (φ : ContinuousAut G) (g : G) (H : ClosedSubgroup G) : φ • conj g • H = conj (φ g) • φ • H

Applying a continuous automorphism after conjugating by g is conjugating by φ g after applying the automorphism: φ * conj g = conj (φ g) * φ.

@[reducible, inline]

abbrev TauCeti.ClosedSubgroupConjClasses (G : Type u_1) [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : Type u_1

The closed subgroups of G up to conjugacy: the orbits of the conjugation action of G on ClosedSubgroup G.

def TauCeti.ClosedSubgroupConjClasses.mk {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (H : ClosedSubgroup G) : ClosedSubgroupConjClasses G

The conjugacy class of a closed subgroup.

@[simp]

theorem TauCeti.ClosedSubgroupConjClasses.quotient_mk_eq_mk {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (H : ClosedSubgroup G) : ⟦H⟧ = mk H

The class map is the quotient map of the orbit relation; simp rewrites the latter to the former.

theorem TauCeti.ClosedSubgroupConjClasses.mk_surjective {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : Function.Surjective mk

Every conjugacy class of closed subgroups is the class of a closed subgroup.

theorem TauCeti.ClosedSubgroupConjClasses.mk_eq_mk_iff {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {H K : ClosedSubgroup G} : mk H = mk K ↔ ∃ (g : G), ContinuousAut.conj g • H = K

Two closed subgroups have the same conjugacy class exactly when one is a conjugate of the other.

@[instance_reducible]

instance TauCeti.ContinuousAut.instMulActionClosedSubgroupConjClasses {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : MulAction (ContinuousAut G) (ClosedSubgroupConjClasses G)

A continuous automorphism acts on closed subgroups up to conjugacy: it carries conjugate closed subgroups to conjugate closed subgroups.

@[simp]

theorem TauCeti.ContinuousAut.smul_closedSubgroupConjClass {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (φ : ContinuousAut G) (H : ClosedSubgroup G) : φ • ClosedSubgroupConjClasses.mk H = ClosedSubgroupConjClasses.mk (φ • H)

A continuous automorphism sends the class of H to the class of φ • H.

@[simp]

theorem TauCeti.ContinuousAut.conj_smul_closedSubgroupConjClasses {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (g : G) (c : ClosedSubgroupConjClasses G) : conj g • c = c

Inner automorphisms fix every conjugacy class of closed subgroups.

@[instance_reducible]

instance TauCeti.ContinuousOut.instMulActionClosedSubgroupConjClasses {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : MulAction (ContinuousOut G) (ClosedSubgroupConjClasses G)

The action of continuous automorphisms on closed subgroups up to conjugacy factors through continuous outer automorphisms.

@[simp]

theorem TauCeti.ContinuousOut.mk_smul_closedSubgroupConjClasses {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (φ : ContinuousAut G) (c : ClosedSubgroupConjClasses G) : ↑φ • c = φ • c

The outer action on closed subgroups up to conjugacy is computed using any representative continuous automorphism.

theorem TauCeti.ContinuousOut.mk_smul_closedSubgroupConjClass {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (φ : ContinuousAut G) (H : ClosedSubgroup G) : ↑φ • ClosedSubgroupConjClasses.mk H = ClosedSubgroupConjClasses.mk (φ • H)

The class of φ in ContinuousOut G sends the class of H to the class of φ • H.