Topological generation of profinite groups

A subset of a topological group generates it topologically when the subgroup it generates is dense, that is when (Subgroup.closure s).topologicalClosure = ⊤. For a profinite group this is a condition on the finite quotients alone: a subgroup is dense exactly when it surjects onto every quotient by an open normal subgroup (Subgroup.topologicalClosure_eq_top_iff_forall_map_mk'). That criterion is the whole content of the notion, and everything else here is read off from it.

Topological finite generation — TauCeti.IsTopologicallyFinitelyGenerated, whose general API is in TauCeti/Topology/Algebra/Group/Generation.lean — is likewise detected by the finite quotients, but only in a uniform form: G is topologically finitely generated if and only if the minimal number of generators of its finite quotients is bounded (isTopologicallyFinitelyGenerated_iff_exists_rank_le). A bound on Group.rank (G ⧸ U) for each open normal U separately says nothing, since each such quotient is finite.

A possibly infinite subset converges to one when only finitely many of its elements lie outside each neighborhood of 1; in a profinite group it suffices to test open normal subgroups. This condition is inherited by subsets and carried to images by continuous maps preserving 1. It is the finiteness condition on generating sets used to define the cardinal-valued generator rank of a profinite group.

Main results

• Subgroup.topologicalClosure_eq_top_iff_forall_map_mk': a subgroup of a profinite group is dense if and only if its image in every quotient by an open normal subgroup is everything.
• TauCeti.topologicalClosure_closure_eq_top_iff: the same, for the subgroup generated by a subset.
• TauCeti.forall_mem_zpowers_mk_of_topologicalClosure_closure_eq_top: a topological generator generates every finite quotient.
• TauCeti.surjective_of_forall_surjective_mk'_comp: a continuous homomorphism from a compact group that is surjective onto every finite quotient is surjective.
• TauCeti.exists_topologicalClosure_closure_range_eq_top_of_rank_le: a profinite group whose finite quotients are generated by n elements is topologically generated by an n-tuple.
• TauCeti.rank_quotient_le_card_of_topologicalClosure_closure_eq_top: conversely, a topological generating set bounds the rank of every quotient by an open normal subgroup.
• TauCeti.isTopologicallyFinitelyGenerated_iff_exists_rank_le: topological finite generation is exactly a uniform bound on the ranks of the finite quotients.
• TauCeti.ConvergesToOne: a set has only finitely many elements outside every neighborhood of 1; TauCeti.ConvergesToOne.tendsto_coe is the defining limit of the inclusion.
• TauCeti.convergesToOne_iff_openNormalSubgroup: in a profinite group, the same holds for every open normal subgroup.
• TauCeti.ConvergesToOne.image: a continuous map preserving 1 carries a set converging to one to another such set.
• Filter.Tendsto.convergesToOne_range: the range of a map tending to 1 along the cofinite filter converges to one.
• TauCeti.ConvergesToOne.isCompact_insert_one, TauCeti.ConvergesToOne.isClosed_insert_one: a set converging to one is compact, and in a Hausdorff space closed, once 1 is added to it.
• Subgroup.exists_convergesToOne_lift_quotient: a converging set in a quotient by a closed normal subgroup has a converging set of representatives upstairs.
• Subgroup.exists_convergesToOne_lift_quotient_topologicallyGenerates: if the set generates the quotient, its representatives together with the kernel generate upstairs.
• Subgroup.exists_convergesToOne_lift_union_topologicallyGenerates: converging generators of a closed normal subgroup and its quotient combine to generate the ambient profinite group.
• TauCeti.exists_convergesToOne_topologicallyGenerates: every profinite group has a topological generating set converging to one.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Sections 2.5 and 2.6.

def TauCeti.ConvergesToOne {G : Type u_1} [TopologicalSpace G] [One G] (s : Set G) : Prop

A subset of a topological space with a distinguished point 1 converges to one when its inclusion tends to 1 along the cofinite filter, that is when every neighborhood of 1 omits only finitely many of its elements (TauCeti.convergesToOne_iff). For a profinite group this says that every open normal subgroup omits only finitely many elements (TauCeti.convergesToOne_iff_openNormalSubgroup); it is the finiteness condition imposed on generating sets in the cardinal-valued topological generator rank of a profinite group.

Equations

• TauCeti.ConvergesToOne s = Filter.Tendsto Subtype.val Filter.cofinite (nhds 1)

theorem TauCeti.ConvergesToOne.tendsto_coe {G : Type u_1} [TopologicalSpace G] [One G] {s : Set G} (hs : ConvergesToOne s) : Filter.Tendsto Subtype.val Filter.cofinite (nhds 1)

The inclusion of a set converging to one tends to 1 along the cofinite filter. This is the definition of TauCeti.ConvergesToOne, which is not unfolded outside this module.

theorem TauCeti.convergesToOne_iff {G : Type u_1} [TopologicalSpace G] [One G] {s : Set G} : ConvergesToOne s ↔ ∀ U ∈ nhds 1, {x : G | x ∈ s ∧ x ∉ U}.Finite

A set converges to one exactly when only finitely many of its elements lie outside each neighborhood of 1.

theorem Set.Finite.convergesToOne {G : Type u_1} [TopologicalSpace G] [One G] {s : Set G} (hs : s.Finite) : TauCeti.ConvergesToOne s

Every finite subset converges to one.

theorem TauCeti.ConvergesToOne.mono {G : Type u_1} [TopologicalSpace G] [One G] {s t : Set G} (hs : ConvergesToOne s) (hts : t ⊆ s) : ConvergesToOne t

Every subset of a set converging to one also converges to one.

theorem TauCeti.ConvergesToOne.union {G : Type u_1} [TopologicalSpace G] [One G] {s t : Set G} (hs : ConvergesToOne s) (ht : ConvergesToOne t) : ConvergesToOne (s ∪ t)

The union of two sets converging to one again converges to one.

theorem Filter.Tendsto.convergesToOne_range {G : Type u_1} [TopologicalSpace G] [One G] {ι : Type u_2} {f : ι → G} (hf : Tendsto f cofinite (nhds 1)) : TauCeti.ConvergesToOne (Set.range f)

The range of a map tending to 1 along the cofinite filter converges to one.

theorem TauCeti.ConvergesToOne.isCompact_insert_one {G : Type u_1} [TopologicalSpace G] [One G] {s : Set G} (hs : ConvergesToOne s) : IsCompact (insert 1 s)

A set converging to one is compact once 1 is added to it.

theorem TauCeti.ConvergesToOne.isClosed_insert_one {G : Type u_1} [TopologicalSpace G] [One G] [T2Space G] {s : Set G} (hs : ConvergesToOne s) : IsClosed (insert 1 s)

In a Hausdorff space, a set converging to one is closed once 1 is added to it; so for a profinite group G the subspace insert 1 s is a profinite space.

theorem TauCeti.convergesToOne_iff_openNormalSubgroup {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {s : Set G} : ConvergesToOne s ↔ ∀ (U : OpenNormalSubgroup G), {x : G | x ∈ s ∧ x ∉ ↑U.toOpenSubgroup}.Finite

In a profinite group, a set converges to one exactly when only finitely many of its elements lie outside each open normal subgroup.

theorem TauCeti.ConvergesToOne.image {G : Type u_1} [TopologicalSpace G] {H : Type u_2} [TopologicalSpace H] [One G] [One H] {F : Type u_3} [FunLike F G H] [OneHomClass F G H] {s : Set G} (hs : ConvergesToOne s) (f : F) (hf : Continuous ⇑f) : ConvergesToOne (⇑f '' s)

The image of a set converging to one under a continuous map preserving 1 also converges to one. The map may be any OneHomClass morphism; OneHomClass only asks f 1 = 1, so no compatibility with multiplication is needed.

@[simp]

theorem ContinuousMulEquiv.convergesToOne_image_iff {G : Type u_1} [TopologicalSpace G] {H : Type u_2} [TopologicalSpace H] [MulOneClass G] [MulOneClass H] (e : G ≃ₜ* H) {s : Set G} : TauCeti.ConvergesToOne (⇑e '' s) ↔ TauCeti.ConvergesToOne s

A continuous multiplicative equivalence carries a set converging to one exactly to a set converging to one.

theorem Subgroup.topologicalClosure_eq_top_iff_forall_map_mk' {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) : H.topologicalClosure = ⊤ ↔ ∀ (U : OpenNormalSubgroup G), map (QuotientGroup.mk' ↑U.toOpenSubgroup) H = ⊤

A subgroup of a profinite group is dense exactly when it surjects onto every quotient by an open normal subgroup. Density is topologicalClosure = ⊤; the open normal subgroups are cofinal among the open subgroups, so nothing finer than the finite quotients can be seen.

theorem TauCeti.topologicalClosure_closure_eq_top_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {s : Set G} : (Subgroup.closure s).topologicalClosure = ⊤ ↔ ∀ (U : OpenNormalSubgroup G), Subgroup.closure (⇑(QuotientGroup.mk' ↑U.toOpenSubgroup) '' s) = ⊤

A subset of a profinite group generates a dense subgroup exactly when its image generates every quotient by an open normal subgroup.

theorem TauCeti.forall_mem_zpowers_mk_of_topologicalClosure_closure_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {γ : G} (hγ : (Subgroup.closure {γ}).topologicalClosure = ⊤) (U : OpenNormalSubgroup G) (x : G ⧸ ↑U.toOpenSubgroup) : x ∈ Subgroup.zpowers ↑γ

If γ topologically generates the topological group G, then its class generates every quotient G ⧸ U by an open normal subgroup: every element of G ⧸ U is a power of γ.

theorem TauCeti.surjective_of_forall_surjective_mk'_comp {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] [CompactSpace H] {φ : H →* G} (hφ : Continuous ⇑φ) (h : ∀ (U : OpenNormalSubgroup G), Function.Surjective ⇑((QuotientGroup.mk' ↑U.toOpenSubgroup).comp φ)) : Function.Surjective ⇑φ

Surjectivity onto a profinite group is detected on the finite quotients. A continuous homomorphism from a compact group into a profinite group G whose composite with every quotient map onto a finite quotient G ⧸ U is surjective is itself surjective.

theorem TauCeti.exists_topologicalClosure_closure_range_eq_top_of_rank_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {n : ℕ} (hrank : ∀ (U : OpenNormalSubgroup G), Group.rank (G ⧸ ↑U.toOpenSubgroup) ≤ n) : ∃ (g : Fin n → G), (Subgroup.closure (Set.range g)).topologicalClosure = ⊤

Topological generation from the finite quotients. If every finite quotient of a profinite group G is generated by n elements, then G is topologically generated by an n-tuple.

The bound has to be uniform in the quotient: each G ⧸ U is finite, so a bound for a single U carries no information.

theorem TauCeti.exists_finset_card_le_topologicalClosure_closure_eq_top_of_rank_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {n : ℕ} (hrank : ∀ (U : OpenNormalSubgroup G), Group.rank (G ⧸ ↑U.toOpenSubgroup) ≤ n) : ∃ (s : Finset G), s.card ≤ n ∧ (Subgroup.closure ↑s).topologicalClosure = ⊤

A profinite group whose finite quotients are generated by n elements has a topological generating set of at most n elements.

theorem TauCeti.rank_quotient_le_card_of_topologicalClosure_closure_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {s : Finset G} (hs : (Subgroup.closure ↑s).topologicalClosure = ⊤) (U : OpenNormalSubgroup G) [Group.FG (G ⧸ ↑U.toOpenSubgroup)] : Group.rank (G ⧸ ↑U.toOpenSubgroup) ≤ s.card

The rank of a finitely generated quotient of a topological group by an open normal subgroup is at most the cardinality of any finite topological generating set, because the image of that set generates the quotient. For a compact group — in particular a profinite one — every such quotient is finite, so the finite-generation hypothesis is automatic and the bound applies to all the finite quotients at once.

theorem TauCeti.isTopologicallyFinitelyGenerated_iff_exists_rank_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : IsTopologicallyFinitelyGenerated G ↔ ∃ (n : ℕ), ∀ (U : OpenNormalSubgroup G), Group.rank (G ⧸ ↑U.toOpenSubgroup) ≤ n

Topological finite generation is a uniform bound on the ranks of the finite quotients. A profinite group is topologically finitely generated if and only if there is an n bounding the minimal number of generators of every quotient by an open normal subgroup.

theorem Subgroup.exists_convergesToOne_lift_quotient {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (N : Subgroup G) [N.Normal] (hN : IsClosed ↑N) {s : Set (G ⧸ N)} (hs : TauCeti.ConvergesToOne s) : ∃ (t : Set G), TauCeti.ConvergesToOne t ∧ ⇑(QuotientGroup.mk' N) '' t = s

A set converging to one in the quotient by a closed normal subgroup has a set of representatives converging to one upstairs. The representatives come from the normalized continuous section of the quotient map.

theorem Subgroup.exists_convergesToOne_lift_quotient_topologicallyGenerates {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (N : Subgroup G) [N.Normal] (hN : IsClosed ↑N) {s : Set (G ⧸ N)} (hs : TauCeti.ConvergesToOne s) (hsg : (closure s).topologicalClosure = ⊤) : ∃ (t : Set G), TauCeti.ConvergesToOne t ∧ ⇑(QuotientGroup.mk' N) '' t = s ∧ (closure (t ∪ ↑N)).topologicalClosure = ⊤

If a converging set topologically generates a quotient by a closed normal subgroup, it has a converging set of representatives which, together with the kernel, topologically generates the ambient profinite group. This is the extension step needed when constructing converging generators through successively finer quotients.

theorem Subgroup.exists_convergesToOne_lift_union_topologicallyGenerates {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (N : Subgroup G) [N.Normal] (hN : IsClosed ↑N) {s : Set (G ⧸ N)} (hs : TauCeti.ConvergesToOne s) (hsg : (closure s).topologicalClosure = ⊤) {u : Set ↥N} (hu : TauCeti.ConvergesToOne u) (hug : (closure u).topologicalClosure = ⊤) : ∃ (t : Set G), ⇑(QuotientGroup.mk' N) '' t = s ∧ TauCeti.ConvergesToOne (t ∪ ⇑N.subtype '' u) ∧ (closure (t ∪ ⇑N.subtype '' u)).topologicalClosure = ⊤

Converging generators combine across a closed normal subgroup. If both a closed normal subgroup and the corresponding quotient have converging topological generating sets, then the ambient profinite group has one obtained by lifting the quotient generators and adjoining the subgroup generators. The lifted set still maps exactly to the prescribed quotient set.

This is the compositional form of Subgroup.exists_convergesToOne_lift_quotient_topologicallyGenerates: it replaces the whole kernel by a dense generating subset, so it can be iterated along a series of closed normal subgroups.

Every profinite group has a generating set converging to one

Every profinite group admits a set that converges to 1 and generates a dense subgroup (Ribes–Zalesskii, Proposition 2.6.2). This makes the family used to define the cardinal-valued topological generator rank nonempty.

Refining a partial solution

Fix a partial solution a and an open normal subgroup U. The refinement has subgroup K ⊓ U and keeps, inside S, the subgroup K, the points lying in U, and the set a.reps U: one K ⊓ U-coset in each of the finitely many K-cosets of S outside K ⊔ U.

theorem TauCeti.exists_convergesToOne_topologicallyGenerates {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : ∃ (s : Set G), ConvergesToOne s ∧ (Subgroup.closure s).topologicalClosure = ⊤

Every profinite group has a generating set converging to one (Ribes–Zalesskii, Proposition 2.6.2). Such a set has only finitely many elements outside each open normal subgroup and generates a dense subgroup, so the least cardinality of a topological generating set converging to one is an infimum over a nonempty family.