Serre's theorem at arbitrary rank: projective pro-p groups are free

Let G be a pro-p group, not necessarily topologically finitely generated. If G is projective, meaning that every continuous homomorphism from G into a quotient of a profinite pro-p group lifts continuously, then G is free pro-p on a pointed profinite space: some subset s ⊆ G converging to 1 has a presentation F_p(insert 1 s, 1) → G (TauCeti.IsProP.presentation) that is a topological isomorphism. In particular this holds when cd_p G ≤ 1, which is Serre's theorem with no finite generation hypothesis. Conversely the free pro-p group on a pointed space is projective and has cd_p ≤ 1, so for pro-p groups projectivity, cd_p ≤ 1 and freeness on a pointed profinite space are the same condition.

The proof runs the finite-rank argument of TauCeti.Topology.Algebra.Group.Profinite.Free.Serre on a minimal presentation on a pointed space: G has a presentation on a subset s converging to 1 whose kernel lies in the Frattini subgroup of F_p(insert 1 s, 1). Projectivity lifts the identity of G through it to a continuous homomorphic section, and a Frattini cover of a pro-p group with such a section is an isomorphism (TauCeti.IsProP.continuousMulEquivOfLeftInverse). The converse, that a pro-p group free on a pointed profinite space has cd_p ≤ 1, is its projectivity read through the vanishing of H² of a projective pro-p group (TauCeti.IsProP.isProjective_iff_cohomologicalDimensionAt_le_one).

Main results

• TauCeti.IsProP.exists_convergesToOne_continuousMulEquiv_presentation_of_isProjective: a projective pro-p group is free pro-p on a pointed profinite space, its presentation on some subset converging to 1 being a topological isomorphism.
• TauCeti.IsProP.isProjective_iff_exists_convergesToOne_continuousMulEquiv_presentation: a pro-p group is projective if and only if it is free pro-p on a pointed profinite space.
• IsProP.exists_convergesToOne_continuousMulEquiv_presentation_of_cohomologicalDimensionAt_le_one (in the TauCeti namespace): Serre's theorem at arbitrary rank, a pro-p group with cd_p ≤ 1 is free pro-p on a pointed profinite space.
• IsProP.cohomologicalDimensionAt_le_one_iff_exists_convergesToOne_continuousMulEquiv_presentation (in the TauCeti namespace): a pro-p group has cd_p ≤ 1 if and only if it is free pro-p on a pointed profinite space.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §4.2 and §5.9.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. III, §5.
• L. Ribes and P. Zalesskii, Profinite Groups, 2nd ed., Section 7.7.

theorem TauCeti.IsProP.exists_convergesToOne_continuousMulEquiv_presentation_of_isProjective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hproj : IsProjective p G) : ∃ (s : Set G), ConvergesToOne s ∧ ∃ (e : freeProPInsertOne p s ≃ₜ* G), ⇑e = ⇑(hG.presentation s)

Projective pro-p groups are free pro-p on a pointed profinite space. A projective pro-p group G has a subset s converging to 1 whose presentation F_p(insert 1 s, 1) → G is a topological isomorphism.

theorem TauCeti.IsProP.isProjective_iff_exists_convergesToOne_continuousMulEquiv_presentation {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) : IsProjective p G ↔ ∃ (s : Set G), ConvergesToOne s ∧ ∃ (e : freeProPInsertOne p s ≃ₜ* G), ⇑e = ⇑(hG.presentation s)

A pro-p group is projective if and only if it is free pro-p on a pointed profinite space, its presentation on some subset converging to 1 being a topological isomorphism.

theorem TauCeti.IsProP.exists_convergesToOne_continuousMulEquiv_presentation_of_cohomologicalDimensionAt_le_one {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hcd : cohomologicalDimensionAt p G ≤ 1) : ∃ (s : Set G), ConvergesToOne s ∧ ∃ (e : freeProPInsertOne p s ≃ₜ* G), ⇑e = ⇑(hG.presentation s)

Serre's theorem at arbitrary rank. A pro-p group G with cd_p G ≤ 1 is free pro-p on a pointed profinite space: some subset s of G converging to 1 has a presentation F_p(insert 1 s, 1) → G that is a topological isomorphism. No finite generation is assumed.

theorem TauCeti.IsProP.cohomologicalDimensionAt_le_one_iff_exists_convergesToOne_continuousMulEquiv_presentation {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) : cohomologicalDimensionAt p G ≤ 1 ↔ ∃ (s : Set G), ConvergesToOne s ∧ ∃ (e : freeProPInsertOne p s ≃ₜ* G), ⇑e = ⇑(hG.presentation s)

Serre's theorem at arbitrary rank, as an equivalence. A pro-p group G has cd_p G ≤ 1 if and only if it is free pro-p on a pointed profinite space: some subset s of G converging to 1 has a presentation F_p(insert 1 s, 1) → G that is a topological isomorphism.