Products of pro-p groups

The class of pro-p groups is stable under products: if each factor is pro-p, then so is their product with the product topology. Together with stability under continuous surjective images from ProP.Basic, this is part of the basic closure API for IsProP, and lets new pro-p groups be assembled from known factors without re-examining their open normal subgroups. The result is stated both for binary products G × H and for indexed products ∀ i, G i, the two product forms used in practice.

The index type of IsProP.pi is arbitrary, so the closure covers infinite products as well as finite ones. That generality is what makes it applicable to inverse limits, which are carved out of a product over an index category that need not be finite.

Main results

• IsProP.prod: a product of two pro-p groups is pro-p.
• IsProP.pi: a product of pro-p groups is pro-p.

References

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

theorem TauCeti.IsProP.prod {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (hG : IsProP p G) (hH : IsProP p H) : IsProP p (G × H)

A product of two pro-p groups, with the product topology, is pro-p.

theorem TauCeti.IsProP.pi {p : ℕ} {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (hG : ∀ (i : ι), IsProP p (G i)) : IsProP p ((i : ι) → G i)

A product of pro-p groups, with the product topology, is pro-p. Specialising to a finite index type gives stability under finite products.