The topological generator rank of a profinite group

The topological generator rank topologicalGeneratorRank G of a topological group G is the least cardinality of a subset that converges to 1 and generates a dense subgroup. Convergence to 1 is not decoration: without it the invariant is the least cardinality of a dense subgroup, which is the wrong notion for a profinite group. A product of continuum many copies of ℤ/p has a countable dense subgroup, yet every generating set converging to 1 has cardinality 2 ^ ℵ₀, which is the number the Frattini quotient and every later rank formula see.

For a profinite G the family being minimized over is nonempty — that is TauCeti.exists_convergesToOne_topologicallyGenerates — so the infimum is attained, cardinals being well-ordered. Attainment is what all the theorems below run on: an isomorphism-invariant, surjection-monotone cardinal whose finiteness is exactly TauCeti.IsTopologicallyFinitelyGenerated.

Alongside it sits the natural-number accessor topologicalGeneratorRankNat G h, the least cardinality of a finite topological generating set, available exactly when G is topologically finitely generated. Every numerical rank statement — Schreier-type bounds, deficiencies, Euler formulas, anything that subtracts ranks — is about the accessor rather than about the cardinal, and TauCeti.topologicalGeneratorRankNat_eq_topologicalGeneratorRank is what ties the two together. A comparison of the cardinal ranks of two groups is stated in Cardinal.lift form, so that the groups need not share a universe, with the same-universe form derived from it. The accessor needs no compactness and no convergence condition, since a finite set converges to 1 in any topological group; compactness enters only through the comparison with the cardinal rank.

Main definitions

• TauCeti.topologicalGeneratorRank: the least cardinality of a topological generating set converging to 1.
• TauCeti.topologicalGeneratorRankNat: the least cardinality of a finite topological generating set, for a topologically finitely generated group.

Main results

• TauCeti.topologicalGeneratorRank_le: a topological generating set converging to 1 bounds the rank by its cardinality.
• TauCeti.lift_topologicalGeneratorRank_congr, TauCeti.topologicalGeneratorRank_congr: the rank is invariant under a topological group isomorphism, with no compactness needed.
• TauCeti.exists_convergesToOne_mk_eq_topologicalGeneratorRank: in a profinite group the infimum is attained.
• TauCeti.lift_topologicalGeneratorRank_le_of_surjective, TauCeti.topologicalGeneratorRank_le_of_surjective, TauCeti.topologicalGeneratorRank_quotient_le: a continuous surjection does not raise the rank.
• TauCeti.topologicalGeneratorRank_lt_aleph0_iff: the rank is finite exactly under topological finite generation.
• TauCeti.topologicalGeneratorRank_eq_zero_iff: the rank vanishes exactly on the trivial group.
• TauCeti.topologicalGeneratorRankNat_le_of_surjective, TauCeti.topologicalGeneratorRankNat_congr: the accessor does not increase along a continuous surjection and is invariant under a topological group isomorphism.
• TauCeti.topologicalGeneratorRankNat_le_of_openSubgroup_of_finiteIndex, TauCeti.topologicalGeneratorRankNat_le_of_openSubgroup: the Schreier bound d(U) ≤ 1 + [G : U] * (d(G) - 1) for an open subgroup U of finite index, in particular for every open subgroup of a compact group.
• TauCeti.topologicalGeneratorRankNat_eq_topologicalGeneratorRank: the accessor computes the cardinal rank whenever it is available.
• TauCeti.topologicalGeneratorRankNat_eq_rank: on a discrete group the accessor is Mathlib's Group.rank.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.6; Proposition 2.6.2 for the existence of a generating set converging to 1; Corollary 3.6.3 for the Schreier bound.

noncomputable def TauCeti.topologicalGeneratorRank (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Cardinal.{u}

The topological generator rank of a topological group: the least cardinality of a subset that converges to 1 and generates a dense subgroup. For a profinite group the family is nonempty (TauCeti.exists_convergesToOne_topologicallyGenerates), so the infimum is attained; for a group with no such generating set the empty infimum makes the rank 0, and every theorem below assumes what it needs.

Equations

• TauCeti.topologicalGeneratorRank G = ⨅ (s : { s : Set G // TauCeti.ConvergesToOne s ∧ (Subgroup.closure s).topologicalClosure = ⊤ }), Cardinal.mk ↑↑s

theorem TauCeti.topologicalGeneratorRank_def (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : topologicalGeneratorRank G = ⨅ (s : { s : Set G // ConvergesToOne s ∧ (Subgroup.closure s).topologicalClosure = ⊤ }), Cardinal.mk ↑↑s

The defining equation of the topological generator rank: the body of TauCeti.topologicalGeneratorRank is not exposed, so unfolding it goes through this lemma.

noncomputable def TauCeti.topologicalGeneratorRankNat (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (_h : IsTopologicallyFinitelyGenerated G) : ℕ

The natural-number topological generator rank of a topologically finitely generated topological group: the least cardinality of a finite topological generating set. This is the accessor every numerical rank statement uses; it agrees with the cardinal-valued TauCeti.topologicalGeneratorRank on a profinite group by TauCeti.topologicalGeneratorRankNat_eq_topologicalGeneratorRank.

Equations

• TauCeti.topologicalGeneratorRankNat G _h = sInf {n : ℕ | ∃ (s : Finset G), s.card = n ∧ (Subgroup.closure ↑s).topologicalClosure = ⊤}

theorem TauCeti.topologicalGeneratorRankNat_def (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h : IsTopologicallyFinitelyGenerated G) : topologicalGeneratorRankNat G h = sInf {n : ℕ | ∃ (s : Finset G), s.card = n ∧ (Subgroup.closure ↑s).topologicalClosure = ⊤}

The defining equation of the natural-number topological generator rank: the body of TauCeti.topologicalGeneratorRankNat is not exposed, so unfolding it goes through this lemma.

theorem TauCeti.topologicalGeneratorRank_le {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {s : Set G} (hs : ConvergesToOne s) (hgen : (Subgroup.closure s).topologicalClosure = ⊤) : topologicalGeneratorRank G ≤ Cardinal.mk ↑s

A topological generating set converging to 1 bounds the topological generator rank by its cardinality.

theorem TauCeti.lift_topologicalGeneratorRank_congr {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) : Cardinal.lift.{v, u} (topologicalGeneratorRank G) = Cardinal.lift.{u, v} (topologicalGeneratorRank H)

Topologically isomorphic groups have the same topological generator rank: an isomorphism carries the generating sets converging to 1 of one group bijectively onto those of the other, so the two infima are taken over the same cardinals. No compactness is needed, the empty case included: if neither group has such a generating set both ranks are the empty infimum 0. The two groups need not share a universe, so the comparison is between Cardinal.lifts; TauCeti.topologicalGeneratorRank_congr is the same-universe form.

theorem TauCeti.topologicalGeneratorRank_congr {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) : topologicalGeneratorRank G = topologicalGeneratorRank H

Topologically isomorphic groups in the same universe have the same topological generator rank.

theorem TauCeti.exists_convergesToOne_mk_eq_topologicalGeneratorRank (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : ∃ (s : Set G), ConvergesToOne s ∧ (Subgroup.closure s).topologicalClosure = ⊤ ∧ Cardinal.mk ↑s = topologicalGeneratorRank G

In a profinite group the infimum defining the topological generator rank is attained: some topological generating set converging to 1 has exactly that cardinality. The family is nonempty by TauCeti.exists_convergesToOne_topologicallyGenerates and the cardinals are well-ordered.

theorem TauCeti.lift_topologicalGeneratorRank_le_of_surjective {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace G] [TotallyDisconnectedSpace G] (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Cardinal.lift.{u, v} (topologicalGeneratorRank H) ≤ Cardinal.lift.{v, u} (topologicalGeneratorRank G)

A continuous surjective homomorphism cannot raise the topological generator rank: the image of a topological generating set converging to 1 is one again. The source and the target need not share a universe, so the comparison is between Cardinal.lifts; TauCeti.topologicalGeneratorRank_le_of_surjective is the same-universe form. Compactness of the source is what supplies the generating set that is pushed forward: a group admitting no set converging to 1 at all has rank 0 by the empty infimum, while its quotients can have positive rank, so the hypothesis is not decoration.

theorem TauCeti.topologicalGeneratorRank_le_of_surjective {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace G] [TotallyDisconnectedSpace G] (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : topologicalGeneratorRank H ≤ topologicalGeneratorRank G

A continuous surjective homomorphism onto a group in the same universe cannot raise the topological generator rank.

theorem TauCeti.topologicalGeneratorRank_quotient_le {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (N : Subgroup G) [N.Normal] : topologicalGeneratorRank (G ⧸ N) ≤ topologicalGeneratorRank G

Passing to a quotient cannot raise the topological generator rank.

theorem TauCeti.topologicalGeneratorRank_lt_aleph0_iff {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : topologicalGeneratorRank G < Cardinal.aleph0 ↔ IsTopologicallyFinitelyGenerated G

The topological generator rank of a profinite group is finite exactly when the group is topologically finitely generated.

theorem TauCeti.topologicalGeneratorRank_eq_zero_iff {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : topologicalGeneratorRank G = 0 ↔ Subsingleton G

The topological generator rank of a profinite group vanishes exactly on the trivial group.

theorem TauCeti.topologicalGeneratorRankNat_le {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h : IsTopologicallyFinitelyGenerated G) {s : Finset G} (hs : (Subgroup.closure ↑s).topologicalClosure = ⊤) : topologicalGeneratorRankNat G h ≤ s.card

A finite topological generating set bounds the natural-number topological generator rank by its cardinality.

theorem TauCeti.exists_finset_card_eq_topologicalGeneratorRankNat {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h : IsTopologicallyFinitelyGenerated G) : ∃ (s : Finset G), s.card = topologicalGeneratorRankNat G h ∧ (Subgroup.closure ↑s).topologicalClosure = ⊤

The infimum defining the natural-number topological generator rank is attained: some finite topological generating set has exactly that cardinality.

theorem TauCeti.topologicalGeneratorRankNat_le_of_surjective {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) (hG : IsTopologicallyFinitelyGenerated G) : topologicalGeneratorRankNat H ⋯ ≤ topologicalGeneratorRankNat G hG

A continuous surjective homomorphism cannot raise the natural-number topological generator rank. Unlike its cardinal counterpart this needs no compactness: a finite generating set of the source has a finite image.

theorem TauCeti.topologicalGeneratorRankNat_le_of_openSubgroup_of_finiteIndex {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsTopologicallyFinitelyGenerated G) (U : OpenSubgroup G) [(↑U).FiniteIndex] : topologicalGeneratorRankNat ↥↑U ⋯ ≤ 1 + (↑U).index * (topologicalGeneratorRankNat G hG - 1)

The Schreier bound. Let U be an open subgroup of finite index in a topologically finitely generated topological group G. Then U is topologically finitely generated (TauCeti.IsTopologicallyFinitelyGenerated.of_openSubgroup_of_finiteIndex), and d(U) ≤ 1 + [G : U] * (d(G) - 1), with subtraction in ℕ. This is the topological form of Schreier's index formula Subgroup.rank_le_one_add_index_mul_rank_sub_one. The bound is sharp: finite-index subgroups of nontrivial finitely generated discrete free groups attain it, by the Nielsen–Schreier theorem.

theorem TauCeti.topologicalGeneratorRankNat_le_of_openSubgroup {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) (U : OpenSubgroup G) : topologicalGeneratorRankNat ↥↑U ⋯ ≤ 1 + (↑U).index * (topologicalGeneratorRankNat G hG - 1)

The Schreier bound for open subgroups of a compact group. Every open subgroup U of a topologically finitely generated compact group G is topologically finitely generated (TauCeti.IsTopologicallyFinitelyGenerated.of_openSubgroup), with d(U) ≤ 1 + [G : U] * (d(G) - 1).

theorem TauCeti.topologicalGeneratorRankNat_congr {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) (hG : IsTopologicallyFinitelyGenerated G) : topologicalGeneratorRankNat G hG = topologicalGeneratorRankNat H ⋯

The natural-number topological generator rank is invariant under topological isomorphism.

@[simp]

theorem TauCeti.topologicalGeneratorRankNat_eq_topologicalGeneratorRank {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (h : IsTopologicallyFinitelyGenerated G) : ↑(topologicalGeneratorRankNat G h) = topologicalGeneratorRank G

The natural-number accessor computes the cardinal topological generator rank whenever it is available. Every theorem that subtracts ranks is stated with the accessor, and this is how it connects to the general cardinal theory.

theorem TauCeti.topologicalGeneratorRankNat_eq_rank {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [Group.FG G] (h : IsTopologicallyFinitelyGenerated G) : topologicalGeneratorRankNat G h = Group.rank G

On a discrete group the natural-number topological generator rank is Mathlib's Group.rank: in a discrete group every subgroup is its own topological closure, so a dense subgroup is the whole group and the two infima range over the same generating sets.