The continuous ZMod p-dual is bounded by the topological generator rank

A topological generating set converging to 1 bounds the continuous 𝔽_p-dual TauCeti.continuousZModDual p G of a topological group from above: a continuous character has open kernel, hence is trivial on all but finitely many members of such a set, and it is determined by its values there, so restriction is a linear injection of the dual into the finitely supported 𝔽_p-valued functions on the set. Minimising over the generating sets of a profinite group turns this into a bound by the topological generator rank, and a finite generating set turns it into finite-dimensionality.

Nothing here is pro-p, and nothing here needs the group to be commutative. The reverse inequality does need the group to be pro-p, but not to be commutative: its dual basis argument runs on the elementary abelian Frattini quotient, and the equality it yields, TauCeti.IsProP.topologicalGeneratorRank_eq_rank_continuousZModDual, holds for an arbitrary profinite pro-p group.

Main results

• TauCeti.rank_continuousZModDual_le_of_convergesToOne: a topological generating set converging to 1 bounds the dimension of the continuous 𝔽_p-dual by its cardinality.
• TauCeti.rank_continuousZModDual_le_topologicalGeneratorRank: the dimension of the continuous 𝔽_p-dual of a profinite group is at most its topological generator rank.
• TauCeti.finite_continuousZModDual: the continuous 𝔽_p-dual of a topologically finitely generated topological group is finite-dimensional.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.8.

theorem TauCeti.rank_continuousZModDual_le_of_convergesToOne {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {s : Set G} (hs : ConvergesToOne s) (hgen : (Subgroup.closure s).topologicalClosure = ⊤) : Module.rank (ZMod p) (continuousZModDual p G) ≤ Cardinal.mk ↑s

A generating set converging to 1 bounds the dimension of the continuous 𝔽_p-dual. Restriction to the set is injective because a character with open kernel is determined by its values on a topological generating set, and it lands in the finitely supported functions because the kernel of a continuous character is an open neighbourhood of 1.

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

The dimension of the continuous 𝔽_p-dual of a profinite group is at most its topological generator rank. No pro-p hypothesis is needed for this half.

theorem TauCeti.finite_continuousZModDual {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hfg : IsTopologicallyFinitelyGenerated G) : Module.Finite (ZMod p) (continuousZModDual p G)

The continuous 𝔽_p-dual of a topologically finitely generated topological group is finite-dimensional, its dimension being bounded by the cardinality of a finite topological generating set. Neither a pro-p hypothesis nor compactness is needed: a finite set converges to 1 in any topological group.