The outer action of an extension

Let E be a topological group and N a normal subgroup of E, with the subspace topology. Conjugation gives ContinuousAut.conjNormal : E →* ContinuousAut N, where conjNormal e sends n to e * n * e⁻¹. Conjugation by an element of N is an inner automorphism of N (ContinuousAut.conjNormal_coe), so composing with the quotient map to ContinuousOut N kills N, and the result descends to the outer action TauCeti.outerAction : E ⧸ N →* ContinuousOut N, sending e N to the class of conjugation by e (TauCeti.outerAction_mk). Its kernel is the image of N ⊔ C_E(N): the classes of the elements of E that act on N as an element of N does.

When N is compact, ContinuousAut.conjNormal is continuous for the congruence topology on ContinuousAut N: on each characteristic open quotient N ⧸ U, which is finite, the induced automorphism is determined by the classes e * n * e⁻¹ U of finitely many representatives n, each locally constant in e. Hence the outer action is continuous for the quotient topologies. Neither finite generation nor total disconnectedness of N is needed for continuity; they are what make ContinuousAut N and ContinuousOut N profinite.

The case of interest is a closed normal subgroup of a profinite group, such as the geometric fundamental group inside an arithmetic fundamental group, where the outer action is the outer Galois action. The construction does not use closedness, so no closedness hypothesis is imposed.

Main definitions

• TauCeti.outerAction: the outer action E ⧸ N →* ContinuousOut N.

Main results

• TauCeti.outerAction_mk: the outer action of e N is the class of conjugation by e.
• TauCeti.ker_outerAction: the kernel of the outer action is the image of N ⊔ C_E(N).
• TauCeti.outerAction_smul_conjClasses_mk: the outer action on conjugacy classes of N is induced by conjugation.
• TauCeti.ContinuousAut.continuous_conjNormal, TauCeti.continuous_outerAction: for compact N, both maps are continuous for the congruence topology and its quotient.

References

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

def TauCeti.outerAction {E : Type u_1} [Group E] [TopologicalSpace E] (N : Subgroup E) [N.Normal] [SeparatelyContinuousMul E] : E ⧸ N →* ContinuousOut ↥N

The outer action of E ⧸ N on a normal subgroup N: the class of e acts by the outer class of conjugation by e (outerAction_mk). It is well defined because conjugation by an element of N is inner.

@[simp]

theorem TauCeti.outerAction_mk {E : Type u_1} [Group E] [TopologicalSpace E] {N : Subgroup E} [N.Normal] [SeparatelyContinuousMul E] (e : E) : (outerAction N) ↑e = ↑(ContinuousAut.conjNormal e)

The outer action of the class of e is the outer class of conjugation by e.

theorem TauCeti.ker_outerAction {E : Type u_1} [Group E] [TopologicalSpace E] {N : Subgroup E} [N.Normal] [SeparatelyContinuousMul E] : (outerAction N).ker = Subgroup.map (QuotientGroup.mk' N) (N ⊔ Subgroup.centralizer ↑N)

The kernel of the outer action is the image of N ⊔ C_E(N): the class of e acts trivially exactly when conjugation by e agrees on N with conjugation by an element of N.

theorem TauCeti.outerAction_smul_conjClasses_mk {E : Type u_1} [Group E] [TopologicalSpace E] {N : Subgroup E} [N.Normal] [SeparatelyContinuousMul E] (e : E) (n : ↥N) : (outerAction N) ↑e • ConjClasses.mk n = ConjClasses.mk ((ContinuousAut.conjNormal e) n)

The outer action on conjugacy classes of N is induced by conjugation: the class of e sends the conjugacy class of n to that of e * n * e⁻¹.

theorem TauCeti.ContinuousAut.continuous_conjNormal {E : Type u_1} [Group E] [TopologicalSpace E] {N : Subgroup E} [N.Normal] [IsTopologicalGroup E] [CompactSpace ↥N] : Continuous ⇑conjNormal

For compact N, conjugation E → ContinuousAut N is continuous for the congruence topology: on each characteristic open quotient N ⧸ U, which is finite, the induced automorphism is determined by the locally constant classes of e * n * e⁻¹ for finitely many n.

theorem TauCeti.continuous_outerAction {E : Type u_1} [Group E] [TopologicalSpace E] {N : Subgroup E} [N.Normal] [IsTopologicalGroup E] [CompactSpace ↥N] : Continuous ⇑(outerAction N)

For compact N, the outer action E ⧸ N → ContinuousOut N is continuous for the quotient topologies.