The free pro-p group on a pointed space is projective

Let F = F_p(X, x₀) be the free pro-p group on a pointed topological space, that is the free pro-C group TauCeti.freeProCPointed C x₀ for C the class of finite p-groups. A finite embedding problem for F with p-group kernel is a continuous surjection π : F ↠ Q onto a finite group together with a surjection α : E ↠ Q of finite groups whose kernel is a p-group. Since Q is a continuous finite quotient of the pro-p group F, it is a p-group, and then so is E. A set-theoretic section of α normalised at 1, composed with π ∘ of, is a continuous map X → E killing x₀, because Q and E are discrete; the universal property of F extends it to a continuous homomorphism F → E, which solves the problem because both composites agree on the generators. So F solves every finite embedding problem with p-group kernel, and the inverse-limit assembly of compatible finite solutions makes it projective: every continuous homomorphism from F into a quotient of a profinite pro-p group lifts continuously.

Neither compactness of X nor any bound on its size is used: the universal property of freeProCPointed holds for every pointed topological space. For the free pro-p group on a discrete type the same statements are TauCeti.hasPGroupSolutions_freeProP and its corollary.

Main results

• TauCeti.hasPGroupSolutions_freeProCPointed: F_p(X, x₀) solves every finite embedding problem with p-group kernel.
• TauCeti.isProjective_freeProCPointed: F_p(X, x₀) is projective.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §5.9.
• L. Ribes and P. Zalesskii, Profinite Groups, 2nd ed., Chapter 7.

theorem TauCeti.hasPGroupSolutions_freeProCPointed (p : ℕ) {X : Type u} [TopologicalSpace X] (x₀ : X) : HasPGroupSolutions p (freeProCPointed (finiteGroupClassP p) x₀)

The free pro-p group on a pointed space solves the finite embedding problems with p-group kernel: for every continuous surjection π : F_p(X, x₀) ↠ Q onto a finite group and every surjection α : E ↠ Q of finite groups with ker α a p-group, some continuous homomorphism β : F_p(X, x₀) → E satisfies α ∘ β = π.

theorem TauCeti.isProjective_freeProCPointed (p : ℕ) {X : Type u} [TopologicalSpace X] (x₀ : X) : IsProjective p (freeProCPointed (finiteGroupClassP p) x₀)

The free pro-p group on a pointed space is projective: every continuous homomorphism from F_p(X, x₀) into a quotient of a profinite pro-p group lifts continuously, with the covering group and the quotient in arbitrary universes.