The generator rank of a pro-p group and its continuous 𝔽_p-dual

For a profinite pro-p group G the topological generator rank is the dimension of the continuous 𝔽_p-dual TauCeti.continuousZModDual p G over 𝔽_p. This is Burnside's basis theorem as an identity of cardinals, with no finiteness hypothesis anywhere; the dual, and not the Frattini quotient itself, is the correct object, because at infinite rank the Frattini quotient is a vector space of much larger dimension than the rank — a countable product of copies of ℤ/p has rank ℵ₀ and Frattini quotient of dimension 2 ^ ℵ₀.

One inequality holds for every profinite group and is proved without any pro-p hypothesis, as TauCeti.rank_continuousZModDual_le_topologicalGeneratorRank.

The other inequality is the dual-basis construction, and it is where compactness and the elementary abelian hypothesis enter. Over the Frattini quotient W, the common kernel of a basis of the dual is trivial, so by compactness the finite intersections of those kernels are a neighbourhood basis of 1. In particular, for each basis vector the common kernel of the others is not contained in its own kernel — otherwise a finite subfamily would already be, making it a linear combination of finitely many of the others. Choosing a point separating it from the others gives a dual basis, which converges to 1 and generates W topologically. Finally a generating set of the Frattini quotient converging to 1 lifts to G, which is TauCeti.IsProP.topologicalGeneratorRank_quotient_proPFrattini.

Main results

• TauCeti.topologicalGeneratorRank_le_rank_continuousZModDual: for a profinite 𝔽_p-vector group the dimension of the continuous 𝔽_p-dual bounds the topological generator rank from above.
• TauCeti.IsProP.topologicalGeneratorRank_eq_rank_continuousZModDual: Burnside's basis theorem, cardinal form — the two agree for a profinite pro-p group.
• TauCeti.IsProP.exists_tendsto_cofinite_topologicallyGenerates_coord_eq: a basis of the continuous 𝔽_p-dual of a profinite pro-p group has a dual family in the group, which tends to 1 and generates topologically — a converging basis of the group.
• TauCeti.IsProP.finrank_continuousZModDual_eq_topologicalGeneratorRankNat: the natural-number form of the theorem, for a topologically finitely generated pro-p group.
• TauCeti.IsProP.finite_continuousZModDual_iff: the continuous 𝔽_p-dual is finite-dimensional exactly when the pro-p group is topologically finitely generated.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.8.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, (3.9.1).

Dual bases in a profinite elementary abelian group

theorem TauCeti.topologicalGeneratorRank_le_rank_continuousZModDual {p : ℕ} [hp : Fact (Nat.Prime p)] {W : Type u} [CommGroup W] [TopologicalSpace W] [IsTopologicalGroup W] [CompactSpace W] [TotallyDisconnectedSpace W] [hW : Module (ZMod p) (Additive W)] : topologicalGeneratorRank W ≤ Module.rank (ZMod p) (continuousZModDual p W)

Burnside's basis theorem, cardinal form: the lower bound. A profinite group whose additive copy is an 𝔽_p-vector space is topologically generated by a dual family of a basis of its continuous 𝔽_p-dual, and such a dual family converges to 1.

Burnside's basis theorem in cardinal form

theorem TauCeti.IsProP.topologicalGeneratorRank_eq_rank_continuousZModDual {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) : topologicalGeneratorRank G = Module.rank (ZMod p) (continuousZModDual p G)

Burnside's basis theorem, cardinal form. The topological generator rank of a profinite pro-p group is the dimension of its continuous 𝔽_p-dual over 𝔽_p. No finiteness hypothesis is needed, and the statement is an identity of cardinals.

theorem TauCeti.IsProP.exists_tendsto_cofinite_topologicallyGenerates_coord_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {ι : Type u} (b : Module.Basis ι (ZMod p) (continuousZModDual p G)) : ∃ (g : ι → G), Filter.Tendsto g Filter.cofinite (nhds 1) ∧ (Subgroup.closure (Set.range g)).topologicalClosure = ⊤ ∧ ∀ (i : ι) (x : continuousZModDual p G), (b.coord i) x = Multiplicative.toAdd ((Additive.toMul x) (g i))

Dual families of a basis of the continuous dual of a pro-p group. For a basis b of the continuous 𝔽_p-dual of a profinite pro-p group G there is a family g : ι → G whose evaluation functionals are the coordinate functionals of b: b j (g i) is 1 for j = i and 0 otherwise. It tends to 1 along the cofinite filter and generates G topologically: it is a topological generating set converging to 1 whose members are separated by continuous characters, the generating set of the minimal presentations of G.

theorem TauCeti.IsProP.finrank_continuousZModDual_eq_topologicalGeneratorRankNat {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) : Module.finrank (ZMod p) (continuousZModDual p G) = topologicalGeneratorRankNat G hfg

Burnside's basis theorem, numerical form against the dual. For a topologically finitely generated profinite pro-p group the dimension of the continuous 𝔽_p-dual over 𝔽_p is the natural-number topological generator rank.

theorem TauCeti.IsProP.finite_continuousZModDual_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) : Module.Finite (ZMod p) (continuousZModDual p G) ↔ IsTopologicallyFinitelyGenerated G

Finiteness of the continuous 𝔽_p-dual of a profinite pro-p group. The dual is finite-dimensional over 𝔽_p exactly when the group is topologically finitely generated.