Module

Procyclic.lean

Nyll.ProCGroups.Generation.Procyclic

1 declaration indexed from sourceView source ↗

Module documentation

A topological generator from cyclic finite quotients

For each open normal quotient, the lifts of its generators form a closed subset of the original compact group. A generator of a common finite quotient solves any finite family of these conditions. Compactness supplies one element satisfying all of them, and the finite-quotient criterion proves that this element topologically generates the original group.

Imports4

Nyll.ProCGroups.Generation.QuotientCriteria
Nyll.ProCGroups.ProC.OpenNormalSubgroups.Basic
Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Mathlib.Topology.Compactness.Compact

Imported by2

theorem

exists_topologicallyGenerates_singleton_of_cyclic_quotients

L32 ↗

ProCGroups.Generation.exists_topologicallyGenerates_singleton_of_cyclic_quotients

Documentation

A profinite group all of whose open normal quotients are cyclic has an actual topological generator. The compatible generator is obtained by compactness, not given as extra data.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
open scoped Topology
namespace ProCGroups.Generation
open ProCGroups.ProC
universe u

Lean source · statement

theorem exists_topologicallyGenerates_singleton_of_cyclic_quotients
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hcyclic : ∀ U : OpenNormalSubgroup G, IsCyclic (G ⧸ (U : Subgroup G))) :
    ∃ g : G, TopologicallyGenerates ({g} : Set G)

Module documentation

A topological generator from cyclic finite quotients

Declarations

exists_topologicallyGenerates_singleton_of_cyclic_quotients