Pro-p groups

A topological group is pro-p when each of its continuous finite quotients is a p-group. For the unbundled profinite groups used in Tau Ceti, these quotients are represented by the quotients by open normal subgroups. This file introduces that quotient-form predicate and its basic covariant API: abstract p-groups are pro-p, continuous surjective images of pro-p groups are pro-p, and hence so are topological quotients. It also records invariance under topological group isomorphism and agreement with IsPGroup for a discrete topology.

Closedness of a normal subgroup is not needed for the predicate to descend to its quotient. It is needed only when one wants the quotient of a profinite group to be profinite again; that separate topological fact is supplied by QuotientGroup.instTotallyDisconnectedSpace.

Main results

• IsProP: every quotient by an open normal subgroup is a p-group.
• isProP_iff: the defining property, as a lemma usable outside this module.
• IsPGroup.isProP: an abstract p-group with any topology is pro-p.
• isProP_of_module_zmod: a commutative group whose additive copy is a ZMod p-module, for instance an elementary abelian group, is pro-p.
• isProP_iff_isPGroup: for a discrete topology, pro-p agrees with IsPGroup.
• isProP_multiplicative_zmod_pow: the discrete cyclic group ℤ/pⁿ is pro-p.
• IsProP.exists_forall_pow_pow_eq_one: each finite quotient of a pro-p group is killed by a power of p.
• IsProP.subsingleton_of_coprime, IsProP.subsingleton_of_ne: a profinite group that is pro-p and pro-q for coprime p, q, in particular for distinct primes, is trivial.
• IsProP.of_surjective: a continuous surjective image of a pro-p group is pro-p.
• IsProP.quotient: a quotient of a pro-p group by a normal subgroup is pro-p.
• IsProP.top: the top subgroup of a pro-p group is pro-p.
• IsProP.isPGroup_range: a homomorphism from a pro-p group with open kernel has a p-group as its range.
• IsProP.isPGroup_map_mk': the image of a pro-p subgroup in the quotient by an open normal subgroup is a p-group.
• IsProP.exists_openNormalSubgroup_le_pow_dvd_relIndex: in an infinite pro-p group every open normal subgroup contains open normal subgroups of arbitrarily large p-power relative index.
• isProP_congr: the predicate is invariant under topological group isomorphism.
• Subgroup.isProP_subgroupOf_iff: for H ≤ K, the predicate for H does not depend on whether H is viewed inside G or inside K.

References

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

def TauCeti.IsProP (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] : Prop

A topological group is pro-p when every quotient by an open normal subgroup is a p-group. For a profinite group these are exactly its continuous finite quotients.

Equations

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

theorem TauCeti.isProP_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] : IsProP p G ↔ ∀ (U : OpenNormalSubgroup G), IsPGroup p (G ⧸ ↑U.toOpenSubgroup)

The defining property of IsProP, available to modules that only see the declaration and not its body.

theorem IsPGroup.isProP {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] (hG : IsPGroup p G) : TauCeti.IsProP p G

An abstract p-group is pro-p for any topology: all of its group quotients are p-groups.

theorem TauCeti.isProP_of_module_zmod {p : ℕ} {W : Type u} [CommGroup W] [TopologicalSpace W] [Module (ZMod p) (Additive W)] : IsProP p W

A commutative topological group whose additive copy is a ZMod p-module is pro-p: it is an abstract p-group by ZModModule.isPGroup_multiplicative.

@[simp]

theorem TauCeti.isProP_iff_isPGroup {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [DiscreteTopology G] : IsProP p G ↔ IsPGroup p G

On a group with the discrete topology, being pro-p is equivalent to being a p-group.

theorem TauCeti.isProP_multiplicative_zmod_pow (p n : ℕ) : IsProP p (Multiplicative (ZMod (p ^ n)))

The cyclic group ℤ/pⁿ, written multiplicatively and with its discrete topology, is pro-p. This holds for every natural number p, including composite numbers.

theorem TauCeti.IsProP.exists_forall_pow_pow_eq_one {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] (hG : IsProP p G) (U : OpenNormalSubgroup G) [Finite (G ⧸ ↑U.toOpenSubgroup)] : ∃ (n : ℕ), ∀ (g : G ⧸ ↑U.toOpenSubgroup), g ^ p ^ n = 1

Each finite quotient of a pro-p group is killed by a single power of p: the exponent in IsPGroup can be chosen uniformly in the element.

theorem TauCeti.IsProP.subsingleton_of_coprime {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {q : ℕ} (hG : IsProP p G) (hG' : IsProP q G) (hpq : p.Coprime q) : Subsingleton G

A profinite group that is pro-p and pro-q for coprime p and q is trivial: its finite quotients are simultaneously p-groups and q-groups.

theorem TauCeti.IsProP.subsingleton_of_ne {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hG : IsProP p G) (hG' : IsProP q G) (hpq : p ≠ q) : Subsingleton G

A profinite group that is pro-p and pro-q for two distinct primes is trivial.

theorem TauCeti.IsProP.of_surjective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (hG : IsProP p G) (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : IsProP p H

A continuous surjective image of a pro-p group is pro-p.

theorem TauCeti.IsProP.quotient {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] (hG : IsProP p G) (N : Subgroup G) [N.Normal] : IsProP p (G ⧸ N)

A quotient of a pro-p group by a normal subgroup is pro-p.

No closedness hypothesis is needed here: closedness controls whether the quotient topology is Hausdorff and profinite, not whether its open-normal quotients are p-groups.

theorem TauCeti.IsProP.topologicalAbelianization_self {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsProP p G) : IsProP p (TopologicalAbelianization G)

The topological abelianization of a pro-p group is pro-p.

theorem TauCeti.IsProP.top {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] (hG : IsProP p G) : IsProP p ↥⊤

The top subgroup of a pro-p group, with its subspace topology, is pro-p.

theorem TauCeti.IsProP.of_equiv {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (hG : IsProP p G) (e : G ≃ₜ* H) : IsProP p H

A topological group isomorphism carries the pro-p property to its target.

theorem TauCeti.IsProP.isPGroup_range {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] (hG : IsProP p G) (f : G →* H) (hf : IsOpen ↑f.ker) : IsPGroup p ↥f.range

The range of a homomorphism from a pro-p group with open kernel is a p-group. In particular, this applies to continuous homomorphisms to discrete groups.

theorem TauCeti.IsProP.isPGroup_map_mk' {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {P : Subgroup G} (hP : IsProP p ↥P) (U : OpenNormalSubgroup G) : IsPGroup p ↥(Subgroup.map (QuotientGroup.mk' ↑U.toOpenSubgroup) P)

The image of a pro-p subgroup in the quotient by an open normal subgroup is a p-group.

theorem TauCeti.IsProP.exists_openNormalSubgroup_le_pow_dvd_relIndex {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [Fact (Nat.Prime p)] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Infinite G] (hG : IsProP p G) (U : OpenNormalSubgroup G) (n : ℕ) : ∃ (V : OpenNormalSubgroup G), ↑V.toOpenSubgroup ≤ ↑U.toOpenSubgroup ∧ p ^ n ∣ (↑V.toOpenSubgroup).relIndex ↑U.toOpenSubgroup

Open normal subgroups of large p-power relative index. In an infinite pro-p group every open normal subgroup U contains, for every n, an open normal subgroup V with p ^ n ∣ [U : V]. Taking p ^ n to be the exponent of a finite p-primary G-module M on which U acts trivially produces a V ≤ U whose relative index [U : V] kills M; this is the choice of subgroup behind the co-effaceability of H⁰ on such modules.

theorem TauCeti.isProP_congr {p : ℕ} {G : Type u} {H : Type v} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] (e : G ≃ₜ* H) : IsProP p G ↔ IsProP p H

Being pro-p is invariant under topological group isomorphism.

theorem Subgroup.isProP_subgroupOf_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H K : Subgroup G} (hHK : H ≤ K) : TauCeti.IsProP p ↥(H.subgroupOf K) ↔ TauCeti.IsProP p ↥H

For subgroups H ≤ K of a topological group, H is pro-p exactly when it is pro-p as a subgroup of K: Subgroup.subgroupOfEquivOfLe is a homeomorphism for the subspace topologies.