The maximal pro-p quotient of a profinite group

The pro-p kernel proPKernel p G of a topological group G is the intersection of the open normal subgroups whose quotient is a p-group, and the maximal pro-p quotient is maximalProPQuotient p G = G ⧸ proPKernel p G. For a profinite G this quotient is the universal pro-p group receiving a continuous homomorphism from G.

The one substantial step is that G(p) really is pro-p. This is a compactness argument rather than a formal one: an open normal subgroup M of G containing proPKernel p G already contains one member U of the defining family, because the sets U \ M form a downward directed family of closed subsets of the compact space G with empty intersection, so one of them is empty. Directedness of the family is where IsPGroup.quotient_inf enters. Once that is known, G ⧸ M is a quotient of G ⧸ U and hence a p-group, and the open normal subgroups of G(p) are exactly the images of such M.

The universal property goes the other way and needs no compactness: if P is profinite and pro-p and f : G →* P is continuous, then for each open normal V ≤ P the preimage V.comap f is an open normal subgroup of G with p-group quotient, so f maps proPKernel p G into every V, and the open normal subgroups of a profinite group intersect in 1.

The pro-p kernel N of a profinite group G has trivial maximal pro-p quotient itself. This is not the definition, since the open normal subgroups of N need not come from those of G. The pro-p kernel K of N is topologically characteristic in N, hence normal and closed in G; then G ⧸ K is an extension of the pro-p group G ⧸ N by a quotient of the pro-p group N ⧸ K, so it is pro-p, and the universal property gives N ≤ K.

Everything before the compactness lemma is stated for an arbitrary topological group: the kernel, its normality, its closedness and its behaviour under continuous homomorphisms all hold there. Compactness of G is assumed exactly where it is used.

Main definitions

• TauCeti.proPKernel: the intersection of the open normal subgroups with p-group quotient.
• TauCeti.maximalProPQuotient: the quotient G ⧸ proPKernel p G, written G(p) in prose.
• TauCeti.maximalProPQuotient.mk: the canonical quotient homomorphism.
• TauCeti.maximalProPQuotient.map: the functorial action on continuous homomorphisms.
• TauCeti.maximalProPQuotient.lift: the canonical factorisation of a continuous homomorphism to a profinite pro-p group.

Main results

• TauCeti.isClosed_proPKernel: the pro-p kernel is closed, so G(p) is profinite again.
• TauCeti.proPKernel_eq_top_iff: the pro-p kernel is the whole group exactly when every relevant p-group quotient is trivial.
• TauCeti.exists_openNormalSubgroup_isPGroup_le: an open subgroup containing the pro-p kernel contains a member of the defining family.
• TauCeti.isProP_maximalProPQuotient: G(p) is pro-p.
• TauCeti.existsUnique_continuousMonoidHom_maximalProPQuotient: a continuous homomorphism from G to a profinite pro-p group factors uniquely and continuously through G(p).
• TauCeti.maximalProPQuotient.lift_comp_map and TauCeti.maximalProPQuotient.comp_lift: that factorisation is natural in the source and in the target.
• TauCeti.proPKernel_eq_bot_iff: G is pro-p if and only if its pro-p kernel is trivial; with TauCeti.proPKernel_maximalProPQuotient_eq_bot this is idempotence of G ↦ G(p).
• TauCeti.map_proPKernel_eq: continuous multiplicative equivalences preserve the pro-p kernel.
• TauCeti.isTopCharacteristic_proPKernel: the pro-p kernel is topologically characteristic.
• TauCeti.proPKernel_proPKernel_eq_top: the pro-p kernel of a profinite group has no nontrivial continuous p-group quotient, so every continuous homomorphism from it to a profinite pro-p group is trivial (TauCeti.eq_one_of_proPKernel_eq_top).

References

• L. Ribes and P. Zalesskii, Profinite Groups.

def TauCeti.proPKernel (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] : Subgroup G

The pro-p kernel of a topological group G: the intersection of the open normal subgroups of G whose quotient is a p-group. For profinite G it is the kernel of the universal continuous homomorphism from G to a pro-p group.

Equations

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

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

The pro-p kernel is a normal subgroup.

@[reducible, inline]

abbrev TauCeti.maximalProPQuotient (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] : Type u

The maximal pro-p quotient G(p) = G ⧸ proPKernel p G.

Equations

• TauCeti.maximalProPQuotient p G = (G ⧸ TauCeti.proPKernel p G)

@[reducible, inline]

abbrev TauCeti.maximalProPQuotient.mk (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] : G →* maximalProPQuotient p G

The canonical homomorphism from G to its maximal pro-p quotient.

Equations

• TauCeti.maximalProPQuotient.mk p G = QuotientGroup.mk' (TauCeti.proPKernel p G)

@[simp]

theorem TauCeti.maximalProPQuotient.mk_apply (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] (x : G) : (mk p G) x = ↑x

The canonical quotient homomorphism sends an element to its quotient class.

theorem TauCeti.maximalProPQuotient.mk_surjective (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] : Function.Surjective ⇑(mk p G)

The canonical homomorphism to the maximal pro-p quotient is surjective.

theorem TauCeti.maximalProPQuotient.continuous_mk (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] : Continuous ⇑(mk p G)

The canonical homomorphism to the maximal pro-p quotient is continuous.

theorem TauCeti.mem_proPKernel_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {x : G} : x ∈ proPKernel p G ↔ ∀ (U : OpenNormalSubgroup G), IsPGroup p (G ⧸ ↑U.toOpenSubgroup) → x ∈ ↑U.toOpenSubgroup

Membership in the pro-p kernel, unfolded over the defining family.

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

The pro-p kernel is contained in every open normal subgroup with p-group quotient.

instance TauCeti.isClosed_proPKernel {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsClosed ↑(proPKernel p G)

The pro-p kernel is closed, so its quotient is profinite when G is profinite.

Trivial maximal quotients

theorem TauCeti.proPKernel_eq_top_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] : proPKernel p G = ⊤ ↔ ∀ (U : OpenNormalSubgroup G), IsPGroup p (G ⧸ ↑U.toOpenSubgroup) → ↑U.toOpenSubgroup = ⊤

The pro-p kernel is the whole group exactly when every open normal subgroup with p-group quotient is the whole group. Equivalently, G has no nontrivial continuous p-group quotient.

theorem TauCeti.maximalProPQuotient.subsingleton_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] : Subsingleton (maximalProPQuotient p G) ↔ proPKernel p G = ⊤

The maximal pro-p quotient is trivial exactly when the pro-p kernel is the whole group.

theorem TauCeti.proPKernel_eq_top_of_not_dvd_card {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [Fact (Nat.Prime p)] (hcard : ¬p ∣ Nat.card G) : proPKernel p G = ⊤

If p does not divide the cardinality of G, then its pro-p kernel is the whole group. For prime p this hypothesis forces G to be finite.

theorem TauCeti.maximalProPQuotient.subsingleton_of_not_dvd_card {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [Fact (Nat.Prime p)] (hcard : ¬p ∣ Nat.card G) : Subsingleton (maximalProPQuotient p G)

If p does not divide the cardinality of G, then its maximal pro-p quotient is trivial. For prime p this hypothesis forces G to be finite.

Functoriality

theorem TauCeti.proPKernel_le_comap {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) : proPKernel p G ≤ Subgroup.comap f (proPKernel p H)

A continuous homomorphism carries the pro-p kernel into the pro-p kernel.

theorem TauCeti.map_proPKernel_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) : Subgroup.map f (proPKernel p G) ≤ proPKernel p H

The image of the pro-p kernel under a continuous homomorphism lies in the pro-p kernel of the target.

theorem TauCeti.map_proPKernel_eq {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (e : G ≃ₜ* H) : Subgroup.map e.toMonoidHom (proPKernel p G) = proPKernel p H

Continuous multiplicative equivalences identify the pro-p kernels of their source and target. In particular, the pro-p kernel is characteristic under continuous automorphisms.

theorem TauCeti.isTopCharacteristic_proPKernel {G : Type u} [Group G] [TopologicalSpace G] (p : ℕ) : IsTopCharacteristic G (proPKernel p G)

The pro-p kernel is topologically characteristic for every topological group and every natural number p.

def TauCeti.maximalProPQuotient.map {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) : maximalProPQuotient p G →* maximalProPQuotient p H

The map induced on maximal pro-p quotients by a continuous homomorphism.

Equations

• TauCeti.maximalProPQuotient.map f hf = QuotientGroup.map (TauCeti.proPKernel p G) (TauCeti.proPKernel p H) f ⋯

@[simp]

theorem TauCeti.maximalProPQuotient.map_mk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) (x : G) : (map f hf) ↑x = (mk p H) (f x)

The induced map on maximal pro-p quotients is computed on classes by f.

theorem TauCeti.maximalProPQuotient.continuous_map {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) : Continuous ⇑(map f hf)

The induced map on maximal pro-p quotients is continuous.

@[simp]

theorem TauCeti.maximalProPQuotient.map_id {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] : map (MonoidHom.id G) ⋯ = MonoidHom.id (maximalProPQuotient p G)

Functoriality: the identity induces the identity.

@[simp]

theorem TauCeti.maximalProPQuotient.map_comp {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] {K : Type w} [Group K] [TopologicalSpace K] (f : G →* H) (hf : Continuous ⇑f) (g : H →* K) (hg : Continuous ⇑g) : map (g.comp f) ⋯ = (map g hg).comp (map f hf)

Functoriality: the induced maps compose.

The compactness step

theorem TauCeti.exists_openNormalSubgroup_isPGroup_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {M : Subgroup G} (hM : IsOpen ↑M) (hKM : proPKernel p G ≤ M) : ∃ (U : OpenNormalSubgroup G), IsPGroup p (G ⧸ ↑U.toOpenSubgroup) ∧ ↑U.toOpenSubgroup ≤ M

An open subgroup containing the pro-p kernel contains an open normal subgroup with p-group quotient.

theorem TauCeti.isPGroup_quotient_of_proPKernel_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {U : OpenNormalSubgroup G} (hU : proPKernel p G ≤ ↑U.toOpenSubgroup) : IsPGroup p (G ⧸ ↑U.toOpenSubgroup)

An open normal subgroup containing the pro-p kernel has p-group quotient.

theorem TauCeti.proPKernel_le_iff_isPGroup_quotient {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {U : OpenNormalSubgroup G} : proPKernel p G ≤ ↑U.toOpenSubgroup ↔ IsPGroup p (G ⧸ ↑U.toOpenSubgroup)

For an open normal subgroup of a compact group, containing the pro-p kernel is the same as having a p-group quotient.

theorem TauCeti.isProP_maximalProPQuotient {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] : IsProP p (maximalProPQuotient p G)

The maximal pro-p quotient is pro-p.

The universal property

theorem TauCeti.proPKernel_le_ker {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Type v} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : G →* P) (hf : Continuous ⇑f) : proPKernel p G ≤ f.ker

A continuous homomorphism to a profinite pro-p group kills the pro-p kernel.

def TauCeti.maximalProPQuotient.lift {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Type v} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : G →* P) (hf : Continuous ⇑f) : maximalProPQuotient p G →* P

The canonical factorisation of a continuous homomorphism to a profinite pro-p group through the maximal pro-p quotient.

Equations

• TauCeti.maximalProPQuotient.lift hP f hf = QuotientGroup.lift (TauCeti.proPKernel p G) f ⋯

@[simp]

theorem TauCeti.maximalProPQuotient.lift_mk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Type v} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : G →* P) (hf : Continuous ⇑f) (x : G) : (lift hP f hf) ↑x = f x

The factorisation through the maximal pro-p quotient computes as f on classes.

@[simp]

theorem TauCeti.maximalProPQuotient.lift_comp_mk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Type v} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : G →* P) (hf : Continuous ⇑f) : (lift hP f hf).comp (mk p G) = f

The factorisation through the maximal pro-p quotient recovers f.

theorem TauCeti.maximalProPQuotient.continuous_lift {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Type v} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : G →* P) (hf : Continuous ⇑f) : Continuous ⇑(lift hP f hf)

The factorisation through the maximal pro-p quotient is continuous.

theorem TauCeti.maximalProPQuotient.lift_unique {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Type v} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : G →* P) (hf : Continuous ⇑f) {g : maximalProPQuotient p G →* P} (hg : ∀ (x : G), g ((mk p G) x) = f x) : g = lift hP f hf

The factorisation through the maximal pro-p quotient is the only homomorphism restricting to f along the quotient map.

theorem TauCeti.maximalProPQuotient.lift_comp_map {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Type v} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] {G' : Type w} [Group G'] [TopologicalSpace G'] (hP : IsProP p P) (f : G →* P) (hf : Continuous ⇑f) (u : G' →* G) (hu : Continuous ⇑u) : (lift hP f hf).comp (map u hu) = lift hP (f.comp u) ⋯

Naturality in the source: the factorisation of f ∘ u is the factorisation of f precomposed with the map induced by u.

theorem TauCeti.maximalProPQuotient.comp_lift {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Type v} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] {Q : Type w} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [CompactSpace Q] [TotallyDisconnectedSpace Q] (hP : IsProP p P) (hQ : IsProP p Q) (f : G →* P) (hf : Continuous ⇑f) (v : P →* Q) (hv : Continuous ⇑v) : v.comp (lift hP f hf) = lift hQ (v.comp f) ⋯

Naturality in the target: postcomposing the factorisation of f with a continuous homomorphism of profinite pro-p groups gives the factorisation of the composite.

theorem TauCeti.existsUnique_continuousMonoidHom_maximalProPQuotient {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Type v} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : G →* P) (hf : Continuous ⇑f) : ∃! g : maximalProPQuotient p G →* P, Continuous ⇑g ∧ ∀ (x : G), g ((maximalProPQuotient.mk p G) x) = f x

The universal property of the maximal pro-p quotient. A continuous homomorphism to a profinite pro-p group factors uniquely and continuously through the canonical quotient map.

theorem TauCeti.eq_one_of_proPKernel_eq_top {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Type v} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (h : proPKernel p G = ⊤) (hP : IsProP p P) (f : G →* P) (hf : Continuous ⇑f) : f = 1

A topological group with no nontrivial continuous p-group quotient admits no nontrivial continuous homomorphism to a profinite pro-p group.

Pro-p groups and idempotence

theorem TauCeti.proPKernel_eq_bot_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : proPKernel p G = ⊥ ↔ IsProP p G

A profinite group is pro-p exactly when its pro-p kernel is trivial.

theorem TauCeti.IsProP.proPKernel_eq_bot {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) : proPKernel p G = ⊥

The pro-p kernel of a profinite pro-p group is trivial.

def TauCeti.maximalProPQuotient.equivOfIsProP {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) : maximalProPQuotient p G ≃ₜ* G

The canonical continuous multiplicative equivalence from the maximal pro-p quotient of a profinite pro-p group to the group itself.

Equations

• TauCeti.maximalProPQuotient.equivOfIsProP hG = { toMulEquiv := (QuotientGroup.quotientMulEquivOfEq ⋯).trans QuotientGroup.quotientBot, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.maximalProPQuotient.equivOfIsProP_mk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (x : G) : (equivOfIsProP hG) ↑x = x

The canonical equivalence from a pro-p group's maximal pro-p quotient sends each class to its representative.

theorem TauCeti.proPKernel_maximalProPQuotient_eq_bot {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : proPKernel p (maximalProPQuotient p G) = ⊥

Idempotence. The pro-p kernel of a maximal pro-p quotient is trivial.

def TauCeti.maximalProPQuotient.idempotentEquiv {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : maximalProPQuotient p (maximalProPQuotient p G) ≃ₜ* maximalProPQuotient p G

Idempotence. Applying the maximal pro-p quotient construction twice gives a group canonically continuously equivalent to applying it once.

Equations

• TauCeti.maximalProPQuotient.idempotentEquiv = TauCeti.maximalProPQuotient.equivOfIsProP ⋯

@[simp]

theorem TauCeti.maximalProPQuotient.idempotentEquiv_mk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : maximalProPQuotient p G) : idempotentEquiv ↑x = x

The idempotence equivalence sends each class to its representative.

The pro-p kernel has no p-quotient

@[simp]

theorem TauCeti.proPKernel_proPKernel_eq_top {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : proPKernel p ↥(proPKernel p G) = ⊤

The pro-p kernel has no p-quotient. The pro-p kernel of the pro-p kernel N of a profinite group is all of N. Equivalently, N has no nontrivial continuous p-group quotient (TauCeti.proPKernel_eq_top_iff), so every continuous homomorphism from N to a profinite pro-p group is trivial (TauCeti.eq_one_of_proPKernel_eq_top).

theorem TauCeti.maximalProPQuotient.subsingleton_proPKernel {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : Subsingleton (maximalProPQuotient p ↥(proPKernel p G))

The maximal pro-p quotient of the pro-p kernel of a profinite group is trivial.