Serre's theorem: cd_p ≤ 1 implies free pro-p

Let G be a topologically finitely generated pro-p group. 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 of rank d(G); in particular this holds when cd_p G ≤ 1.

A minimal generating set of G gives a continuous surjection φ : F ↠ G from the free pro-p group F on d(G) generators. Since φ preserves the generator rank, its kernel lies in the Frattini subgroup Φ(F), so φ is a Frattini cover. Projectivity of G lifts the identity of G through φ 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 generating type X of the free group ranges over the finite types in the universe of G with Nat.card X = d(G), as in TauCeti.IsProP.exists_surjective_freeProP; the type ULift (Fin (d G)) is one such choice. Only this direction of Serre's characterization of free pro-p groups is proved here.

Main results

• TauCeti.IsProP.nonempty_continuousMulEquiv_freeProP_of_isProjective: a projective topologically finitely generated pro-p group is free pro-p of rank d(G).
• TauCeti.IsProP.nonempty_continuousMulEquiv_freeProP_of_cohomologicalDimensionAt_le_one: Serre's theorem, a topologically finitely generated pro-p group with cd_p ≤ 1 is free pro-p of rank d(G).

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, Section 7.7.

theorem TauCeti.IsProP.nonempty_continuousMulEquiv_freeProP_of_isProjective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (hproj : IsProjective p G) (X : Type u) [Finite X] (hX : Nat.card X = topologicalGeneratorRankNat G hfg) : Nonempty (G ≃ₜ* freeProP p X)

Projective topologically finitely generated pro-p groups are free. A topologically finitely generated pro-p group G that is projective is topologically isomorphic to the free pro-p group on any finite type of cardinality d(G).

theorem TauCeti.IsProP.nonempty_continuousMulEquiv_freeProP_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) (hfg : IsTopologicallyFinitelyGenerated G) (hcd : cohomologicalDimensionAt p G ≤ 1) (X : Type u) [Finite X] (hX : Nat.card X = topologicalGeneratorRankNat G hfg) : Nonempty (G ≃ₜ* freeProP p X)

Serre's theorem. A topologically finitely generated pro-p group G with cd_p G ≤ 1 is free pro-p: it is topologically isomorphic to the free pro-p group on any finite type of cardinality d(G).