Open subgroups of a topologically finitely generated compact group

A topologically finitely generated compact group has, for each n, only finitely many open subgroups of index n. The reason is the permutation representation: an open subgroup U of index n makes G act on the n-element coset space G ⧸ U, and U is recovered from that action as the stabilizer of the trivial coset. Transporting the coset space to Fin n turns the action into a homomorphism G →* Equiv.Perm (Fin n) whose kernel, the normal core of U, is open; and a topologically finitely generated group admits only finitely many homomorphisms with open kernel into a fixed finite group (TauCeti.IsTopologicallyFinitelyGenerated.finite_monoidHom_isOpen_ker).

Counting over all indices, the open subgroups then form a countable family, as do the open normal subgroups, and the latter can be arranged in a single descending sequence cofinal among them. That sequence is what lets an inverse-limit argument over the finite quotients be run along ℕ, using Mathlib's IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed in place of the directed form.

The same count has a rigidity consequence. A continuous surjective endomorphism f of G pulls open subgroups back to open subgroups of the same index, injectively; on each of the finite fibers of the index an injective self-map is a bijection, so every open subgroup of G is a preimage f ⁻¹' V. This is the combinatorial half of the Hopf property of a topologically finitely generated profinite group.

Only compactness of G is used, never total disconnectedness: for a connected compact group the statements below are trivial, since ⊤ is then the one open subgroup. The intended case is of course a profinite group, where the open subgroups carry all the information.

Main results

• TauCeti.IsTopologicallyFinitelyGenerated.finite_openSubgroup_index_eq: finitely many open subgroups of each index.
• TauCeti.IsTopologicallyFinitelyGenerated.openSubgroup_comap_surjective: every open subgroup is the preimage of an open subgroup along a continuous surjective endomorphism.
• TauCeti.IsTopologicallyFinitelyGenerated.countable_openSubgroup, TauCeti.IsTopologicallyFinitelyGenerated.countable_openNormalSubgroup: countably many open subgroups, and countably many open normal subgroups.
• TauCeti.IsTopologicallyFinitelyGenerated.exists_antitone_openNormalSubgroup_cofinal: a descending sequence of open normal subgroups cofinal among them.

References

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

theorem TauCeti.IsTopologicallyFinitelyGenerated.finite_openSubgroup_index_eq_of_ne_zero {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsTopologicallyFinitelyGenerated G) (n : ℕ) (hn : n ≠ 0) : Finite { U : OpenSubgroup G // (↑U).index = n }

A topologically finitely generated group has finitely many open subgroups of each nonzero index. An open subgroup of index n is the stabilizer of the trivial coset for the action of G on its n cosets, so it is determined by that action together with the trivial coset; both range over finite sets once the coset space is transported to Fin n.

theorem TauCeti.IsTopologicallyFinitelyGenerated.finite_openSubgroup_index_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) (n : ℕ) : Finite { U : OpenSubgroup G // (↑U).index = n }

A topologically finitely generated compact group has finitely many open subgroups of each index. This includes index zero, whose fiber is empty because open subgroups of a compact group have finite index.

theorem TauCeti.IsTopologicallyFinitelyGenerated.openSubgroup_comap_surjective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) {f : G →* G} (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Function.Surjective fun (V : OpenSubgroup G) => OpenSubgroup.comap f hf V

Pulling back open subgroups along a continuous surjective endomorphism is surjective. If f : G →* G is continuous and surjective, every open subgroup of a topologically finitely generated compact group G is of the form f ⁻¹' V for an open subgroup V.

theorem TauCeti.IsTopologicallyFinitelyGenerated.countable_openSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) : Countable (OpenSubgroup G)

A topologically finitely generated compact group has only countably many open subgroups: they are sorted into finitely many of each index.

theorem TauCeti.IsTopologicallyFinitelyGenerated.countable_openNormalSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) : Countable (OpenNormalSubgroup G)

A topologically finitely generated compact group has only countably many open normal subgroups.

theorem TauCeti.IsTopologicallyFinitelyGenerated.exists_antitone_openNormalSubgroup_cofinal {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) : ∃ (N : ℕ → OpenNormalSubgroup G), Antitone N ∧ ∀ (U : OpenNormalSubgroup G), ∃ (k : ℕ), N k ≤ U

A cofinal descending sequence of open normal subgroups. In a topologically finitely generated compact group the open normal subgroups, being countable and closed under binary infima, are refined by a single antitone sequence. This is what turns an inverse-limit argument over the finite quotients into a statement about a sequence.