The maximal pro-p quotient

For a profinite group G and a prime p, the paper repeatedly uses the maximal pro-p quotient G(p) (e.g. G_{ℚ₂}(2) in B4, and Δ = maxPro2(FreeProfinite (Fin 2)) in B8). This file constructs it and proves the two facts that pin it down:

• it is a pro-p group (isProP_maxProPQuotient), and
• it enjoys the universal property: continuous homomorphisms from G into a pro-p group factor uniquely through G(p) (maxProPHomEquiv, an explicit bijection of hom-sets).

Design

G(p) := G ⧸ K, where the pro-p kernel K = proPKernel p G is the intersection of all open normal subgroups U ≤ G whose (finite) quotient G ⧸ U is a p-group:

proPKernel p G = ⨅ U : {U : OpenNormalSubgroup G // IsPGroup p (G ⧸ U.toSubgroup)}, U.toSubgroup.

K is a closed normal subgroup (an intersection of clopen normal subgroups), so GQ2.profiniteQuotient packages G ⧸ K as a ProfiniteGrp. A profinite group P is pro-p (IsProP p P) exactly when every finite continuous quotient P ⧸ V is a p-group.

The universal property rests on the kernel-containment lemma proPKernel_le_ker: for pro-p P and continuous f : G → P, K ≤ ker f (each f⁻¹ V is an open normal subgroup with G ⧸ f⁻¹V ↪ P ⧸ V a p-group, so it lies in the defining family; and the open normal subgroups of the profinite group P intersect in 1). Pro-p-ness of G(p) is the harder direction: an open normal Ŵ ≥ K contains some member U of the defining family (a directed family of clopen sets whose intersection lies in the open set Ŵ, so — by compactness — one member already does), whence G ⧸ Ŵ is a quotient of the p-group G ⧸ U.

Stress tests: a p-group is its own maximal pro-p quotient (proPKernel_eq_bot_of_isProP, maxProPMk_bijective_of_isProP; idempotence), instantiated on the finite 2-group ZMod 4.

The IsProP predicate

def GQ2.IsProP (p : ℕ) (P : Type u_1) [Group P] [TopologicalSpace P] : Prop

A topological group P is pro-p if every finite continuous quotient P ⧸ U (U an open normal subgroup) is a p-group. For profinite P this is the usual notion of a pro-p group (an inverse limit of finite p-groups).

Equations

• GQ2.IsProP p P = ∀ (U : OpenNormalSubgroup P), IsPGroup p (P ⧸ ↑U.toOpenSubgroup)

theorem GQ2.isProP_of_isPGroup {p : ℕ} {P : Type u_1} [Group P] [TopologicalSpace P] (hP : IsPGroup p P) : IsProP p P

A p-group is pro-p: every quotient of a p-group is a p-group.

Small group-theoretic helpers

theorem GQ2.isPGroup_prod {p : ℕ} {M : Type u_1} {N : Type u_2} [Group M] [Group N] (hM : IsPGroup p M) (hN : IsPGroup p N) : IsPGroup p (M × N)

A product of two p-groups is a p-group.

theorem GQ2.isPGroup_quotient_inf {p : ℕ} {G : Type u_1} [Group G] {A B : Subgroup G} [A.Normal] [B.Normal] (hA : IsPGroup p (G ⧸ A)) (hB : IsPGroup p (G ⧸ B)) : IsPGroup p (G ⧸ A ⊓ B)

If the quotients of G by two normal subgroups A, B are p-groups, then so is the quotient by A ⊓ B (it embeds in (G ⧸ A) × (G ⧸ B)).

def GQ2.topOpenNormalSubgroup (G : Type u_1) [Group G] [TopologicalSpace G] : OpenNormalSubgroup G

The whole group as an open normal subgroup (for non-vacuity of the defining family).

Equations

• GQ2.topOpenNormalSubgroup G = { toSubgroup := ⊤, isOpen' := ⋯, isNormal' := ⋯ }

theorem GQ2.isPGroup_quotient_top {p : ℕ} {G : Type u_1} [Group G] : IsPGroup p (G ⧸ ⊤)

The trivial quotient G ⧸ ⊤ is a p-group.

Intersection of open normal subgroups of a profinite group

theorem GQ2.eq_one_of_forall_mem_openNormalSubgroup {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] {x : P} (h : ∀ (V : OpenNormalSubgroup P), x ∈ V) : x = 1

In a profinite group, an element lying in every open normal subgroup is trivial.

The pro-p kernel and the maximal pro-p quotient

def GQ2.proPKernel (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] : Subgroup G

The pro-p kernel of G: the intersection of all open normal subgroups U ≤ G with G ⧸ U a p-group. G(p) := G ⧸ proPKernel p G.

Equations

• GQ2.proPKernel p G = ⨅ (U : { U : OpenNormalSubgroup G // IsPGroup p (G ⧸ ↑U.toOpenSubgroup) }), ↑(↑U).toOpenSubgroup

instance GQ2.proPKernel_normal (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] : (proPKernel p G).Normal

theorem GQ2.proPKernel_isClosed (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsClosed ↑(proPKernel p G)

theorem GQ2.proPKernel_le {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] (U : OpenNormalSubgroup G) (hU : IsPGroup p (G ⧸ ↑U.toOpenSubgroup)) : proPKernel p G ≤ ↑U.toOpenSubgroup

proPKernel p G ≤ U for every open normal U with G ⧸ U a p-group.

noncomputable def GQ2.maxProPQuotient (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : ProfiniteGrp.{u_1}

The maximal pro-p quotient G(p) of a profinite group G, as an object of ProfiniteGrp.

Equations

• GQ2.maxProPQuotient p G = GQ2.profiniteQuotient (GQ2.proPKernel p G)

noncomputable def GQ2.maxProPMk (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : G →ₜ* ↑(maxProPQuotient p G).toProfinite.toTop

The canonical projection G → G(p), a continuous homomorphism.

Equations

• GQ2.maxProPMk p G = GQ2.quotientMk (GQ2.proPKernel p G)

Universal property (kernel containment + hom-set bijection)

theorem GQ2.proPKernel_le_ker {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] {P : Type u_2} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : G →ₜ* P) : proPKernel p G ≤ f.ker

Kernel-containment lemma. A continuous homomorphism from G to a pro-p profinite group P kills the pro-p kernel: proPKernel p G ≤ ker f. Hence it factors through G(p).

noncomputable def GQ2.maxProPHomEquiv {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Type u_2} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP p P) : (↑(maxProPQuotient p G).toProfinite.toTop →ₜ* P) ≃ (G →ₜ* P)

Universal property of G(p). For a pro-p profinite group P, restriction along the projection G → G(p) is a bijection Hom_cont(G(p), P) ≃ Hom_cont(G, P): every continuous f : G → P factors uniquely through G(p).

Equations

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

Pro-p-ness of G(p)

theorem GQ2.isPGroup_quotient_of_proPKernel_le {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (W : OpenNormalSubgroup G) (hle : proPKernel p G ≤ ↑W.toOpenSubgroup) : IsPGroup p (G ⧸ ↑W.toOpenSubgroup)

If Ŵ is an open normal subgroup containing the pro-p kernel, then G ⧸ Ŵ is a p-group. (By compactness some member U of the defining family already sits inside Ŵ, and G ⧸ Ŵ is then a quotient of the p-group G ⧸ U.)

theorem GQ2.isProP_quotient_proPKernel {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] : IsProP p (G ⧸ proPKernel p G)

G(p) is pro-p (stated on the underlying quotient group). Every finite continuous quotient of G ⧸ proPKernel p G is a p-group.

theorem GQ2.isProP_maxProPQuotient {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] : IsProP p ↑(maxProPQuotient p G).toProfinite.toTop

G(p) is pro-p. This is the defining property of the maximal pro-p quotient (same statement, phrased on the bundled ProfiniteGrp object).

Idempotence: a pro-p group is its own maximal pro-p quotient

theorem GQ2.proPKernel_eq_bot_of_isProP {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (hG : IsProP p G) : proPKernel p G = ⊥

If G is already pro-p, its pro-p kernel is trivial.

Finite stress test: the finite 2-group Multiplicative (ZMod 4) is its own maximal

pro-2 quotient.