Functoriality of the topological abelianization, and the conjugation action on N^{ab}

The topological abelianization G^{ab} = G ⧸ closure [G, G] of a topological group G is Mathlib's TopologicalAbelianization G. This file adds two pieces of API to it.

Functoriality. A continuous homomorphism f : G →* H carries the topological closure of the commutator subgroup of G into that of H, so it induces a continuous homomorphism TopologicalAbelianization.map f hf : G^{ab} →* H^{ab}, compatible with identities and composition.

The conjugation action. Let N be a normal subgroup of G. Conjugation by G preserves N, hence its commutator subgroup, hence the topological closure of the latter, so it descends to an action of G on N^{ab} by continuous group automorphisms; and an element of N acts on N^{ab} trivially, because conjugation by it is an inner automorphism of N, so the action factors through G ⧸ N. Both actions are recorded as MulDistribMulAction instances, the first for Mathlib's conjugation type synonym ConjAct G, the second for the quotient G ⧸ N, and the action of G ⧸ N is jointly continuous. On classes it is (g : G ⧸ N) • (n : N^{ab}) = g n g⁻¹, the convention of MulAut.conjNormal.

This is the structure of Labute's relation module in the classification of Demushkin groups: for a continuous character χ of a free pro-p group F, its kernel X is normal, and Labute's E = X ⧸ (X, X) is TopologicalAbelianization X with Γ = F ⧸ X acting by conjugation (Labute, §4, p. 121). Labute writes the action as [y] · [x] = y⁻¹ x y, which is the inverse of the convention above: his [y] · [x] is [y]⁻¹ • [x] here (mk_inv_smul_mk). His formula defines a left action when Γ is abelian, as it is in his setting (Γ ≅ Im χ ≤ ℤ_pˣ); for a general normal subgroup it is a right action, which is why the instance uses Mathlib's convention and Labute's action is recovered by precomposing with the inversion of the acting group.

Main definitions

• TopologicalAbelianization.map: the homomorphism G^{ab} →* H^{ab} induced by a continuous homomorphism G →* H.
• ContinuousMulEquiv.topologicalAbelianizationCongr: the topological isomorphism G^{ab} ≃ₜ* H^{ab} induced by a topological group isomorphism G ≃ₜ* H.
• The instances MulDistribMulAction (ConjAct G) (TopologicalAbelianization N) and MulDistribMulAction (G ⧸ N) (TopologicalAbelianization N): conjugation on the topological abelianization of a normal subgroup, and its factorization through G ⧸ N.

Main results

• TopologicalAbelianization.map_mk, TopologicalAbelianization.continuous_map, TopologicalAbelianization.map_id, TopologicalAbelianization.map_comp: the characteristic properties of map.
• ContinuousMulEquiv.map_topologicalClosure_commutator: a topological group isomorphism carries the closed commutator subgroup onto the closed commutator subgroup.
• TopologicalAbelianization.map_surjective, TopologicalAbelianization.ker_map_of_surjective: a continuous surjection f : G →* H of a compact group onto a Hausdorff group induces a surjection G^{ab} →* H^{ab} whose kernel is the image of ker f, so that H^{ab} is the quotient of G^{ab} by the image of ker f.
• TopologicalAbelianization.mk_smul_mk: the class of g : G acts on the class of n : N by the class of g * n * g⁻¹; TopologicalAbelianization.mk_inv_smul_mk is Labute's form of the same action, the inverse of the class of g acting by the class of g⁻¹ * n * g.
• TopologicalAbelianization.toConjAct_smul_eq_self_of_mem: elements of N act trivially on N^{ab}.
• The instances ContinuousConstSMul (ConjAct G) (TopologicalAbelianization N) and ContinuousSMul (G ⧸ N) (TopologicalAbelianization N).
• TopologicalAbelianization.map_inclusion_smul, TopologicalAbelianization.map_inclusion_quotient_smul, TopologicalAbelianization.map_inclusion_mk_smul: for normal R ≤ N, the map R^{ab} →* N^{ab} induced by the inclusion is equivariant for conjugation by G, and intertwines the actions of G ⧸ R and G ⧸ N along the canonical map G ⧸ R →* G ⧸ N.
• TopologicalAbelianization.topologicalClosure_closure_univ_smul_image_mk_eq_top: if N is the closed normal closure of a set S, the (G ⧸ N)-orbit of the classes of the elements of S topologically generates N^{ab}.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), §4.

theorem TopologicalAbelianization.topologicalClosure_commutator_le_comap {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) : (commutator G).topologicalClosure ≤ Subgroup.comap f (commutator H).topologicalClosure

A continuous homomorphism carries the topological closure of the commutator subgroup into the topological closure of the commutator subgroup of the target.

def TopologicalAbelianization.map {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) : TopologicalAbelianization G →* TopologicalAbelianization H

The homomorphism G^{ab} →* H^{ab} between topological abelianizations induced by a continuous homomorphism f : G →* H.

Equations

• TopologicalAbelianization.map f hf = QuotientGroup.map (commutator G).topologicalClosure (commutator H).topologicalClosure f ⋯

@[simp]

theorem TopologicalAbelianization.map_mk {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (x : G) : (map f hf) ↑x = ↑(f x)

map f hf sends the class of x : G to the class of f x.

theorem TopologicalAbelianization.continuous_map {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) : Continuous ⇑(map f hf)

The homomorphism G^{ab} →* H^{ab} induced by a continuous homomorphism is continuous.

@[simp]

theorem TopologicalAbelianization.map_id {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : map (MonoidHom.id G) ⋯ = MonoidHom.id (TopologicalAbelianization G)

The identity of G induces the identity of G^{ab}.

theorem TopologicalAbelianization.map_comp {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group K] [TopologicalSpace K] [IsTopologicalGroup K] (g : H →* K) (hg : Continuous ⇑g) (f : G →* H) (hf : Continuous ⇑f) : (map g hg).comp (map f hf) = map (g.comp f) ⋯

The topological abelianization is functorial: the map induced by a composite is the composite of the induced maps.

theorem TopologicalAbelianization.map_surjective {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Function.Surjective ⇑(map f hf)

The homomorphism between topological abelianizations induced by a continuous surjection is surjective.

theorem ContinuousMulEquiv.map_topologicalClosure_commutator {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) : Subgroup.map e.toMonoidHom (commutator G).topologicalClosure = (commutator H).topologicalClosure

A topological group isomorphism G ≃ₜ* H carries the closed commutator subgroup of G onto the closed commutator subgroup of H.

def ContinuousMulEquiv.topologicalAbelianizationCongr {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) : TopologicalAbelianization G ≃ₜ* TopologicalAbelianization H

A topological group isomorphism G ≃ₜ* H induces a topological isomorphism G^{ab} ≃ₜ* H^{ab} between the topological abelianizations. This is the topological analogue of MulEquiv.abelianizationCongr, and the specialisation of ContinuousMulEquiv.quotientCongr to the closed commutator subgroups.

Equations

• e.topologicalAbelianizationCongr = e.quotientCongr (commutator G).topologicalClosure (commutator H).topologicalClosure ⋯

@[simp]

theorem ContinuousMulEquiv.topologicalAbelianizationCongr_mk {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) (x : G) : e.topologicalAbelianizationCongr ↑x = ↑(e x)

e.topologicalAbelianizationCongr sends the class of x : G to the class of e x.

@[simp]

theorem ContinuousMulEquiv.topologicalAbelianizationCongr_symm {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) : e.topologicalAbelianizationCongr.symm = e.symm.topologicalAbelianizationCongr

The inverse of e.topologicalAbelianizationCongr is e.symm.topologicalAbelianizationCongr.

theorem TopologicalAbelianization.ker_map_of_surjective {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace G] [T2Space H] (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : (map f hf).ker = Subgroup.map (QuotientGroup.mk' (commutator G).topologicalClosure) f.ker

The kernel of the map induced on abelianizations by a surjection. For a continuous surjection f : G →* H from a compact group onto a Hausdorff group, the kernel of G^{ab} →* H^{ab} is the image of ker f in G^{ab}. Compactness is what makes the image of the closed commutator subgroup of G closed, so that it is the closed commutator subgroup of H.

instance TopologicalAbelianization.instContinuousConstSMulConjActSubtypeMemSubgroupOfSeparatelyContinuousMul_tauCeti {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (N : Subgroup G) [N.Normal] : ContinuousConstSMul (ConjAct G) ↥N

Conjugation by a fixed element of G is continuous on a normal subgroup.

theorem TopologicalAbelianization.conjAct_smul_mem_topologicalClosure_commutator {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (g : ConjAct G) {n : ↥N} (hn : n ∈ (commutator ↥N).topologicalClosure) : g • n ∈ (commutator ↥N).topologicalClosure

The topological closure of the commutator subgroup of a normal subgroup N is stable under conjugation by G.

instance TopologicalAbelianization.instQuotientActionSubtypeMemSubgroupConjActTopologicalClosureCommutator_tauCeti {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : MulAction.QuotientAction (ConjAct G) (commutator ↥N).topologicalClosure

Conjugation by G on a normal subgroup N descends to the topological abelianization of N.

@[instance_reducible]

instance TopologicalAbelianization.instMulDistribMulActionConjAct {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : MulDistribMulAction (ConjAct G) (TopologicalAbelianization ↥N)

Conjugation on the topological abelianization of a normal subgroup. The group G, as ConjAct G, acts on N^{ab} by group automorphisms, with g • (n : N^{ab}) = (g • n : N) (MulAction.Quotient.smul_mk).

Equations

• TopologicalAbelianization.instMulDistribMulActionConjAct N = { toMulAction := inferInstance, smul_one := ⋯, smul_mul := ⋯ }

theorem TopologicalAbelianization.toConjAct_smul_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (g : G) (n : ↥N) : ConjAct.toConjAct g • ↑n = ↑((MulAut.conjNormal g) n)

Conjugation by g : G on N^{ab}, on the class of n : N: it is the class of the conjugate MulAut.conjNormal g n = g * n * g⁻¹.

instance TopologicalAbelianization.instContinuousConstSMulConjActSubtypeMemSubgroup_tauCeti {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : ContinuousConstSMul (ConjAct G) (TopologicalAbelianization ↥N)

Each conjugation is continuous on the topological abelianization of N.

theorem TopologicalAbelianization.toConjAct_smul_eq_self_of_mem {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] {g : G} (hg : g ∈ N) (x : TopologicalAbelianization ↥N) : ConjAct.toConjAct g • x = x

Elements of N act trivially on N^{ab}: conjugation by an element of N is an inner automorphism of N, which is invisible in a commutative quotient.

def TopologicalAbelianization.conjAut {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : G ⧸ N →* MulAut (TopologicalAbelianization ↥N)

Conjugation by G ⧸ N on N^{ab}, as a homomorphism to the automorphism group: the conjugation action of G factored through G ⧸ N. It is the homomorphism underlying the MulDistribMulAction (G ⧸ N) (TopologicalAbelianization N) instance below (conjAut_apply), whose defining equation is mk_smul.

Equations

• TopologicalAbelianization.conjAut N = QuotientGroup.lift N ((MulDistribMulAction.toMulAut (ConjAct G) (TopologicalAbelianization ↥N)).comp ConjAct.toConjAct.toMonoidHom) ⋯

theorem TopologicalAbelianization.conjAut_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (g : G) : (conjAut N) ↑g = (MulDistribMulAction.toMulAut (ConjAct G) (TopologicalAbelianization ↥N)) (ConjAct.toConjAct g)

conjAut N sends the class of g : G to conjugation by g on N^{ab}, as an element of MulAut (TopologicalAbelianization N).

@[instance_reducible]

instance TopologicalAbelianization.instMulDistribMulActionQuotient {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : MulDistribMulAction (G ⧸ N) (TopologicalAbelianization ↥N)

The conjugation action of G ⧸ N on the topological abelianization of N. It is the action of G by conjugation, which factors through G ⧸ N because N acts trivially (toConjAct_smul_eq_self_of_mem); on classes, (g : G ⧸ N) • (n : N^{ab}) = g * n * g⁻¹ (mk_smul_mk).

Equations

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

@[simp]

theorem TopologicalAbelianization.conjAut_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (γ : G ⧸ N) (x : TopologicalAbelianization ↥N) : ((conjAut N) γ) x = γ • x

Applying the automorphism conjAut N γ is the action of γ : G ⧸ N on N^{ab}.

theorem TopologicalAbelianization.mk_smul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (g : G) (x : TopologicalAbelianization ↥N) : ↑g • x = ConjAct.toConjAct g • x

The class of g : G in G ⧸ N acts on N^{ab} as conjugation by g.

@[simp]

theorem TopologicalAbelianization.mk_smul_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (g : G) (n : ↥N) : ↑g • ↑n = ↑((MulAut.conjNormal g) n)

The defining equation of the action of G ⧸ N on N^{ab}: the class of g sends the class of n to the class of g * n * g⁻¹.

@[simp]

theorem TopologicalAbelianization.mk_inv_smul_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (g : G) (n : ↥N) : (↑g)⁻¹ • ↑n = ↑⟨g⁻¹ * ↑n * g, ⋯⟩

Labute's form of the action (§4 Definition, p. 121): the inverse of the class of y sends the class of x to the class of y⁻¹ * x * y. Labute's [y] · [x] = y⁻¹ x y is thus (y : G ⧸ N)⁻¹ • [x] in the convention of mk_smul_mk; the two agree up to the inversion of the acting group, and Labute's formula is itself a left action when G ⧸ N is abelian.

instance TopologicalAbelianization.instContinuousSMulQuotientSubgroupSubtypeMem_tauCeti {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : ContinuousSMul (G ⧸ N) (TopologicalAbelianization ↥N)

The conjugation action of G ⧸ N on N^{ab} is jointly continuous.

@[simp]

theorem TopologicalAbelianization.mk_eq_one_of_mem_commutator {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} {r : G} (hrN : r ∈ N) (hr : r ∈ ⁅N, N⁆) : ↑⟨r, hrN⟩ = 1

An element of ⁅N, N⁆ has trivial class in N^{ab}: ⁅N, N⁆ is the image of the commutator subgroup of N, which the topological abelianization kills.

theorem TopologicalAbelianization.ofMul_mk_eq_zero_of_mem_commutator {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} {r : G} (hrN : r ∈ N) (hr : r ∈ ⁅N, N⁆) : Additive.ofMul ↑⟨r, hrN⟩ = 0

An element of ⁅N, N⁆ has zero class in N^{ab}, written additively. Not a simp lemma: simp derives it from TopologicalAbelianization.mk_eq_one_of_mem_commutator and ofMul_one.

theorem TopologicalAbelianization.map_inclusion_smul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {R : Subgroup G} [R.Normal] (h : R ≤ N) (g : ConjAct G) (x : TopologicalAbelianization ↥R) : (map (Subgroup.inclusion h) ⋯) (g • x) = g • (map (Subgroup.inclusion h) ⋯) x

For normal subgroups R ≤ N, the map R^{ab} →* N^{ab} induced by the inclusion is equivariant for conjugation by G.

theorem TopologicalAbelianization.map_inclusion_quotient_smul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {R : Subgroup G} [R.Normal] (h : R ≤ N) (γ : G ⧸ R) (x : TopologicalAbelianization ↥R) : (map (Subgroup.inclusion h) ⋯) (γ • x) = (QuotientGroup.map R N (MonoidHom.id G) ⋯) γ • (map (Subgroup.inclusion h) ⋯) x

For normal subgroups R ≤ N, the map R^{ab} →* N^{ab} induced by the inclusion intertwines the actions of G ⧸ R and G ⧸ N along the canonical map G ⧸ R →* G ⧸ N.

theorem TopologicalAbelianization.map_inclusion_mk_smul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {R : Subgroup G} [R.Normal] (h : R ≤ N) (g : G) (x : TopologicalAbelianization ↥R) : (map (Subgroup.inclusion h) ⋯) (↑g • x) = ↑g • (map (Subgroup.inclusion h) ⋯) x

For normal subgroups R ≤ N, the map R^{ab} →* N^{ab} induced by the inclusion intertwines the actions of G ⧸ R and G ⧸ N, on the class of g : G.

theorem TopologicalAbelianization.topologicalClosure_closure_univ_smul_image_mk_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {S : Set G} (hS : (Subgroup.normalClosure S).topologicalClosure = N) : (Subgroup.closure (Set.univ • QuotientGroup.mk '' Subtype.val ⁻¹' S)).topologicalClosure = ⊤

Generators of a closed normal closure generate its abelianization as a module. If N is the closed normal closure of S, then the (G ⧸ N)-orbit of the classes of the elements of S topologically generates N^{ab}: the conjugates of S generate a dense subgroup of N, and conjugation by g on a class is the action of the class of g in G ⧸ N.