Module

LocalWeightTheorems.lean

Nyll.ProCGroups.LocalWeight.LocalWeightTheorems

2 declarations indexed from sourceView source ↗

Module documentation

Local weight from convergent generating sets

This file identifies local weight with the clopen invariant rho in the presence of a closed generating set, and computes the cardinality of an infinite generating set that converges to the identity along open subgroups.

Imports1

Nyll.ProCGroups.LocalWeight.ClosedNormalDataAndTransfiniteSeries

Imported by2

theorem

localWeight_eq_rho_of_closedGeneratingSet

L32 ↗

ProCGroups.LocalWeight.localWeight_eq_rho_of_closedGeneratingSet

Documentation

6.2(a). Closed generating subsets compute the local weight.

Source context 9 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.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration

Lean source · statement

theorem localWeight_eq_rho_of_closedGeneratingSet
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (X : Set G) (hXclosed : IsClosed X)
    (hXgen : TopologicallyGenerates (G := G) X) (hXinfinite : Set.Infinite X) :
    localWeight G = rho ↥X

theorem

cardinalEqLocalWeight_of_generatesAndConvergesToOneAlongOpenSubgroups_infinite

L58 ↗

ProCGroups.LocalWeight.cardinalEqLocalWeight_of_generatesAndConvergesToOneAlongOpenSubgroups_infinite