Pro-p groups and supernatural order

A profinite group is pro-p exactly when its supernatural order is supported at p. This connects the finite-quotient definition of IsProP with the primewise invariant profiniteOrder: every quotient by an open normal subgroup has prime-power order precisely when every other prime has exponent zero in the supremum of the quotient orders.

The equivalent bound by the infinite supernatural prime power is the form used in divisibility arguments.

Main results

• isProP_iff_profiniteOrder_apply_eq_zero: pro-p groups are characterized by the vanishing of every exponent away from p.
• isProP_iff_profiniteOrder_le_primePower: the equivalent supernatural divisibility criterion.
• proPKernel_eq_top_of_profiniteOrder_apply_eq_zero: if p does not divide the supernatural order of a profinite group, then the group has no nontrivial pro-p quotient.
• maximalProPQuotient.subsingleton_of_profiniteOrder_apply_eq_zero: the corresponding maximal pro-p quotient is trivial.

References

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

theorem TauCeti.isProP_iff_profiniteOrder_apply_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [CompactSpace G] : IsProP p G ↔ ∀ (q : Nat.Primes), ↑q ≠ p → profiniteOrder G q = 0

A profinite group is pro-p exactly when every prime other than p has exponent zero in its supernatural order.

theorem TauCeti.isProP_iff_profiniteOrder_le_primePower {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [CompactSpace G] : IsProP p G ↔ profiniteOrder G ≤ Supernatural.primePower ⟨p, ⋯⟩ ⊤

A profinite group is pro-p exactly when its supernatural order divides the infinite p-power.

theorem TauCeti.proPKernel_eq_top_of_profiniteOrder_apply_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [CompactSpace G] (h : profiniteOrder G ⟨p, ⋯⟩ = 0) : proPKernel p G = ⊤

A prime absent from the supernatural order gives no nontrivial pro-p quotient. If the p-exponent of the supernatural order of a profinite group G is zero, then its pro-p kernel is all of G.

theorem TauCeti.maximalProPQuotient.subsingleton_of_profiniteOrder_apply_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [CompactSpace G] (h : profiniteOrder G ⟨p, ⋯⟩ = 0) : Subsingleton (maximalProPQuotient p G)

The maximal pro-p quotient is trivial when p is absent from the supernatural order.