Profinite groups: quotients by normal subgroups, and open subgroups

The foundational layer for profinite groups in the unbundled classes: G is a group with a topology making it a topological group, compact and totally disconnected. The separation chain itself needs no new work — Mathlib derives T1Space, T2Space and T3Space on such a G from TotallyDisconnectedSpace.t1Space and IsTopologicalGroup.regularSpace — so no statement of the profinite and pro-p development has to carry a [T2Space G] hypothesis.

What is genuinely missing is total disconnectedness of a quotient by a closed normal subgroup. We prove it through the clopen-image argument: the quotient map sends the open normal subgroups of G to clopen neighbourhoods of the identity in G ⧸ N, their intersection is the image of N, and in a compact Hausdorff group the connected component of the identity is the intersection of its clopen neighbourhoods. With the compactness, topological-group and separation instances, G ⧸ N is then a profinite group again.

Closedness of N is needed only for the total-disconnectedness results: a quotient by a non-closed subgroup is not even T1 (take ℤ̂ ⧸ ℤ with ℤ dense), so QuotientGroup.connectedComponent_one and QuotientGroup.instTotallyDisconnectedSpace carry the hypothesis, while the clopen-image statement is valid for an arbitrary normal subgroup.

Main results

• Subgroup.eq_iInf_sup_openNormalSubgroup: a closed subgroup is the infimum of the subgroups N ⊔ U with U open normal.
• Subgroup.exists_le_of_iInf_le_of_directed: in a compact group, a directed family of closed subgroups whose infimum lies in an open subgroup has a member lying in it.
• Subgroup.exists_openSubgroup_le_subset_of_isClosed: an open set containing a closed subgroup contains an open subgroup containing it.
• Subgroup.exists_openNormalSubgroup_comap_le: open normal subgroups of a subgroup are refined by pullbacks of ambient open normal subgroups.
• QuotientGroup.connectedComponent_one, QuotientGroup.instTotallyDisconnectedSpace: the quotient of a profinite group by a closed normal subgroup is totally disconnected.
• exists_openNormalSubgroup_lt_card_quotient: an infinite profinite group has finite quotients of arbitrarily large order.
• Subgroup.iInf_openNormalSubgroup_eq_bot: the infimum of the open normal subgroups of a profinite group is trivial.
• Subgroup.isOpen_of_index_sup_openNormalSubgroup_le: a closed subgroup whose joins with the open normal subgroups have uniformly bounded index is open.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Proposition 1.1.4 and Theorem 1.1.6.

@[simp]

theorem Subgroup.map_topologicalClosure_quotient_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) (N : OpenNormalSubgroup G) : map (QuotientGroup.mk' ↑N.toOpenSubgroup) H.topologicalClosure = map (QuotientGroup.mk' ↑N.toOpenSubgroup) H

Taking the topological closure of a subgroup does not change its image in the quotient by an open normal subgroup: that quotient is discrete, so the image is already closed.

theorem Subgroup.eq_iInf_sup_openNormalSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (N : Subgroup G) (hN : IsClosed ↑N) : N = ⨅ (U : OpenNormalSubgroup G), N ⊔ ↑U.toOpenSubgroup

A closed subgroup of a profinite group is the infimum of the subgroups N ⊔ U, over the open normal subgroups U of G: the open normal subgroups are cofinal among the open subgroups containing N. This is the saturation statement behind the clopen-image argument for quotients, and the form of ProfiniteGrp.closedSubgroup_eq_sInf_open that the pro-p development uses.

theorem Subgroup.exists_le_of_iInf_le_of_directed {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] {ι : Type u_2} [Nonempty ι] {U : ι → Subgroup G} (hU : ∀ (i : ι), IsClosed ↑(U i)) (hdir : Directed (fun (x1 x2 : Subgroup G) => x1 ≥ x2) U) {M : Subgroup G} (hM : IsOpen ↑M) (h : ⨅ (i : ι), U i ≤ M) : ∃ (i : ι), U i ≤ M

Compactness for directed families of closed subgroups. In a compact group, if the infimum of a downward directed family of closed subgroups lies in an open subgroup M, then already one member of the family does.

theorem Subgroup.exists_openSubgroup_le_subset_of_isClosed {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) (hH : IsClosed ↑H) {W : Set G} (hW : IsOpen W) (hHW : ↑H ⊆ W) : ∃ (V : OpenSubgroup G), H ≤ ↑V ∧ ↑V ⊆ W

An open neighbourhood of a closed subgroup contains an open subgroup containing it. In a profinite group, every open set containing a closed subgroup H contains an open subgroup V ≥ H.

theorem Subgroup.exists_openNormalSubgroup_comap_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) (V : OpenNormalSubgroup ↥H) : ∃ (N : OpenNormalSubgroup G), comap H.subtype ↑N.toOpenSubgroup ≤ ↑V.toOpenSubgroup

Every open normal subgroup of a subgroup of a profinite group contains the pullback of an ambient open normal subgroup.

theorem Subgroup.eq_one_of_mem_iInf_openNormalSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {x : G} (hx : ∀ (U : OpenNormalSubgroup G), x ∈ ↑U.toOpenSubgroup) : x = 1

In a profinite group, an element that lies in every open normal subgroup is 1.

@[simp]

theorem Subgroup.iInf_openNormalSubgroup_eq_bot {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : ⨅ (U : OpenNormalSubgroup G), ↑U.toOpenSubgroup = ⊥

In a profinite group, the infimum of the open normal subgroups is trivial.

theorem TauCeti.exists_openNormalSubgroup_lt_card_quotient {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Infinite G] (n : ℕ) : ∃ (U : OpenNormalSubgroup G), n < Nat.card (G ⧸ ↑U.toOpenSubgroup)

An infinite profinite group has arbitrarily large finite quotients. For every n there is an open normal subgroup U with n < |G ⧸ U|.

theorem Subgroup.isOpen_of_index_sup_openNormalSubgroup_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Subgroup G} {m : ℕ} (hH : IsClosed ↑H) (hbound : ∀ (N : OpenNormalSubgroup G), (H ⊔ ↑N.toOpenSubgroup).index ≤ m) : IsOpen ↑H

A closed subgroup H of a profinite group whose joins H ⊔ N with the open normal subgroups N have uniformly bounded index is open.

This is the criterion that turns a bound on the indices of the open subgroups above H into openness of H itself, as in the characterization of the open subgroups as the closed subgroups of natural index.

theorem TauCeti.QuotientGroup.connectedComponent_one {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {N : Subgroup G} [N.Normal] (hN : IsClosed ↑N) : connectedComponent 1 = {1}

In the quotient of a profinite group by a closed normal subgroup, the connected component of the identity is trivial: it is contained in every clopen image mk '' U, and the intersection of those images is the image of N, a single point.

instance TauCeti.QuotientGroup.instTotallyDisconnectedSpace {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {N : Subgroup G} [N.Normal] [hN : IsClosed ↑N] : TotallyDisconnectedSpace (G ⧸ N)

The quotient of a profinite group by a closed normal subgroup is totally disconnected. Together with the compactness, topological-group and separation instances, this says that G ⧸ N is a profinite group again.