Module

GeneratingSetsConvergingToOne.lean

Nyll.ProCGroups.LocalWeight.GeneratingSetsConvergingToOne

2 declarations indexed from sourceView source ↗

Module documentation

Generating sets converging to one

Countable descending open-normal bases are characterized by generating sets that converge to the identity along open subgroups. For nonempty profinite groups this yields a characterization of metrizability by a countable convergent generating set.

Imports1

Nyll.ProCGroups.LocalWeight.LocalWeightTheorems

Imported by1

Nyll.ProCGroups.LocalWeight.All

theorem

cardinal_le_aleph0_iff_hasCountableDescendingOpenNormalChainAtOne

L34 ↗

ProCGroups.LocalWeight.cardinal_le_aleph0_iff_hasCountableDescendingOpenNormalChainAtOne

Documentation

A generating set converging to \(1\) is countable exactly when the profinite group admits a countable descending open-normal chain at the identity.

Source context 8 commands

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

open Set
open TopologicalSpace
open Order
open scoped Cardinal
open scoped Topology Pointwise
namespace ProCGroups.LocalWeight
universe u
open ProCGroups.Generation ProCGroups.ProC ProCGroups.FiniteGeneration

Lean source · statement

theorem cardinal_le_aleph0_iff_hasCountableDescendingOpenNormalChainAtOne
    {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (X : Set G) (hX : GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X) :
    Cardinal.mk X ≤ ℵ₀ ↔
      ProCGroups.ProC.HasCountableOpenNormalBasisAtOne G

theorem

nonempty_metrizableSpace_iff_exists_countable_generatingSetConvergingToOne

L91 ↗

ProCGroups.LocalWeight.nonempty_metrizableSpace_iff_exists_countable_generatingSetConvergingToOne