Open subgroups of a free pro-p group: the Nielsen–Schreier theorem

An open subgroup U of index m in a free pro-p group F of finite rank n ≥ 1 is free pro-p of rank d(U) = 1 + m * (n - 1). This is the pro-p Nielsen–Schreier theorem for open subgroups, with the Schreier index formula for the rank. The rank formula shows that the Schreier bound TauCeti.topologicalGeneratorRankNat_le_of_openSubgroup is an equality for free pro-p groups.

Closed subgroups that are not open are free pro-p of possibly infinite rank; that statement needs free pro-p groups on a profinite space and is not made here.

Main results

• TauCeti.freeProP.topologicalGeneratorRankNat_add_index: d(U) + [F : U] = 1 + [F : U] * n.
• TauCeti.freeProP.topologicalGeneratorRankNat_openSubgroup: d(U) = 1 + [F : U] * (n - 1) for n ≥ 1.
• TauCeti.freeProP.cohomologicalDimensionAt_le_one_openSubgroup: cd_p U ≤ 1 for an open subgroup U of a free pro-p group, on any type of generators.
• TauCeti.freeProP.nonempty_continuousMulEquiv_freeProP_openSubgroup: an open subgroup U of a free pro-p group of finite rank is free pro-p of rank d(U).
• TauCeti.freeProP.nonempty_continuousMulEquiv_freeProP_openSubgroup_index: the pro-p Nielsen–Schreier theorem for open subgroups, U ≅ freeProP p Y for every finite type Y with Nat.card Y = 1 + [F : U] * (n - 1).

References

• H. Koch, Galois Theory of p-Extensions, Example 6.3.
• J.-P. Serre, Galois Cohomology, Ch. I, §4.2.
• L. Ribes and P. Zalesskii, Profinite Groups, Thm. 3.6.2, for the transversal proof.

Cohomological dimension of an open subgroup

theorem TauCeti.freeProP.cohomologicalDimensionAt_le_one_openSubgroup {p : ℕ} {X : Type u} (hp : p ≠ 0) (U : OpenSubgroup (freeProP p X)) : cohomologicalDimensionAt p ↥↑U ≤ 1

cd_p U ≤ 1 for an open subgroup U of a free pro-p group, on any type X of generators and for p ≠ 0: cd_p (freeProP p X) ≤ 1 passes to open subgroups.

The rank of an open subgroup

theorem TauCeti.freeProP.topologicalGeneratorRankNat_add_index {p : ℕ} {X : Type u} [hp : Fact (Nat.Prime p)] [Finite X] (U : OpenSubgroup (freeProP p X)) : topologicalGeneratorRankNat ↥↑U ⋯ + (↑U).index = 1 + (↑U).index * Nat.card X

The Schreier index formula for open subgroups, additive form. For an open subgroup U of the free pro-p group on a finite type X, d(U) + [F : U] = 1 + [F : U] * #X.

theorem TauCeti.freeProP.topologicalGeneratorRankNat_openSubgroup {p : ℕ} {X : Type u} [hp : Fact (Nat.Prime p)] [Finite X] [Nonempty X] (U : OpenSubgroup (freeProP p X)) : topologicalGeneratorRankNat ↥↑U ⋯ = 1 + (↑U).index * (Nat.card X - 1)

The Schreier index formula for open subgroups. For an open subgroup U of index m in the free pro-p group on a nonempty finite type X of cardinality n, d(U) = 1 + m * (n - 1).

Freeness of an open subgroup

theorem TauCeti.freeProP.nonempty_continuousMulEquiv_freeProP_openSubgroup {p : ℕ} {X : Type u} [hp : Fact (Nat.Prime p)] [Finite X] (U : OpenSubgroup (freeProP p X)) (Y : Type u) [Finite Y] (hY : Nat.card Y = topologicalGeneratorRankNat ↥↑U ⋯) : Nonempty (↥↑U ≃ₜ* freeProP p Y)

An open subgroup of a free pro-p group of finite rank is free pro-p, of rank d(U). For an open subgroup U of the free pro-p group on a finite type X, U is topologically isomorphic to the free pro-p group on any finite type Y with Nat.card Y = d(U).

theorem TauCeti.freeProP.nonempty_continuousMulEquiv_freeProP_openSubgroup_index {p : ℕ} {X : Type u} [hp : Fact (Nat.Prime p)] [Finite X] [Nonempty X] (U : OpenSubgroup (freeProP p X)) (Y : Type u) [Finite Y] (hY : Nat.card Y = 1 + (↑U).index * (Nat.card X - 1)) : Nonempty (↥↑U ≃ₜ* freeProP p Y)

The pro-p Nielsen–Schreier theorem for open subgroups. An open subgroup U of index m in the free pro-p group on a nonempty finite type X of cardinality n is topologically isomorphic to the free pro-p group on any finite type Y with Nat.card Y = 1 + m * (n - 1).