Quotients of profinite groups by closed normal subgroups are profinite

The paper's presented group Γ_A is a quotient of a free profinite group by the closed normal closure of the relators. Mathlib already provides CompactSpace, T3Space (hence T2Space), and IsTopologicalGroup instances for G ⧸ N; the missing ingredient of profiniteness is total disconnectedness (see docs/foundations-audit.md, "profinite presentations" gap).

This file supplies it: for G profinite and N a closed normal subgroup, G ⧸ N is totally disconnected. The clopen subsets of G ⧸ N form a topological basis — for x ∈ u open, lift x to p ∈ G, take an open normal subgroup U ⊆ G with p · U inside the preimage of u (possible since G is profinite), and push forward: q '' (p · U) is clopen (the quotient map q is open, and closed because N is compact) and lies between x and u. A T0 space with a clopen basis is totally separated, hence totally disconnected.

theorem GQ2.isTopologicalBasis_clopen_quotient {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (N : Subgroup G) [N.Normal] [IsClosed ↑N] : TopologicalSpace.IsTopologicalBasis {s : Set (G ⧸ N) | IsClopen s}

For G profinite and N a closed normal subgroup, the clopen subsets of G ⧸ N form a topological basis.

instance GQ2.instTotallyDisconnectedSpace_quotient {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (N : Subgroup G) [N.Normal] [IsClosed ↑N] : TotallyDisconnectedSpace (G ⧸ N)

Total disconnectedness of G ⧸ N for G profinite and N closed normal. Together with the ambient CompactSpace, T2Space, and IsTopologicalGroup instances this is the last piece of profiniteness.

def GQ2.profiniteQuotient {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (N : Subgroup G) [N.Normal] [IsClosed ↑N] : ProfiniteGrp.{u_1}

The quotient of a profinite group G by a closed normal subgroup N, packaged as an object of ProfiniteGrp. This is the construction underlying profinite presentations (e.g. the paper's Γ_A): quotient the free profinite group by the closed normal closure of the relators.

Equations

• GQ2.profiniteQuotient N = ProfiniteGrp.of (G ⧸ N)

def GQ2.quotientMk {G : Type u_1} [Group G] [TopologicalSpace G] (N : Subgroup G) [N.Normal] : G →ₜ* G ⧸ N

The quotient projection G → G ⧸ N as a continuous homomorphism.

Equations

• GQ2.quotientMk N = { toMonoidHom := QuotientGroup.mk' N, continuous_toFun := ⋯ }

theorem GQ2.quotientMk_surjective {G : Type u_1} [Group G] [TopologicalSpace G] (N : Subgroup G) [N.Normal] : Function.Surjective ⇑(quotientMk N)

theorem GQ2.quotientMk_eq_one_iff {G : Type u_1} [Group G] [TopologicalSpace G] (N : Subgroup G) [N.Normal] {g : G} : (quotientMk N) g = 1 ↔ g ∈ N

An element lies in the kernel of the quotient projection iff it lies in N.

noncomputable def GQ2.quotientLift {G : Type u_1} [Group G] [TopologicalSpace G] (N : Subgroup G) [N.Normal] {P : Type u_2} [Group P] [TopologicalSpace P] (f : G →ₜ* P) (hf : N ≤ f.ker) : G ⧸ N →ₜ* P

Universal property of the profinite quotient. A continuous homomorphism f : G →ₜ* P whose kernel contains N factors through the quotient projection as a continuous homomorphism G ⧸ N →ₜ* P. (Continuity is automatic: G → G ⧸ N is a quotient map.)

Equations

• GQ2.quotientLift N f hf = { toMonoidHom := QuotientGroup.lift N f.toMonoidHom hf, continuous_toFun := ⋯ }

@[simp]

theorem GQ2.quotientLift_quotientMk {G : Type u_1} [Group G] [TopologicalSpace G] (N : Subgroup G) [N.Normal] {P : Type u_2} [Group P] [TopologicalSpace P] (f : G →ₜ* P) (hf : N ≤ f.ker) (g : G) : (quotientLift N f hf) ((quotientMk N) g) = f g