NYLL
Module

CardinalInvariantsAndLocalWeight.lean

Nyll.ProCGroups.LocalWeight.CardinalInvariantsAndLocalWeight
46 declarations indexed from sourceView source ↗

Module documentation

Cardinal invariants and local weight

This file defines the cardinality of a family, topological weight, the clopen invariant rho, and local weight. It compares these invariants using topological and neighborhood bases and proves that continuous homomorphisms are determined by a topological generating set.

Imports2
Imported by2

Declarations

def

familyCardinal

L36 ↗
ProCGroups.LocalWeight.familyCardinal
Documentation

The cardinality of a family of subsets is viewed as a subtype.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
def familyCardinal (B : Set (Set X)) : Cardinal
def

IsNeighborhoodBasisAt

L43 ↗
ProCGroups.LocalWeight.IsNeighborhoodBasisAt
Documentation

A family \(B\) is a neighborhood basis at \(x\) if each member of \(B\) is an open neighborhood of \(x\), and every open neighborhood of \(x\) contains an element of \(B\).

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
def IsNeighborhoodBasisAt (x : X) (B : Set (Set X)) : Prop
def

weight

L48 ↗
ProCGroups.LocalWeight.weight
Documentation

The weight \(w(X)\) is the least cardinality of a basis of open sets.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
def weight : Cardinal
def

rho

L53 ↗
ProCGroups.LocalWeight.rho
Documentation

\(\rho(X)\) is the cardinality of the set of all clopen subsets of \(X\).

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
def rho : Cardinal
def

localWeightAt

L57 ↗
ProCGroups.LocalWeight.localWeightAt
Documentation

The local weight at \(x\) is the least cardinality of a neighborhood basis at \(x\).

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
def localWeightAt (x : X) : Cardinal
theorem

weight_le_familyCardinal_of_basis

L63 ↗
ProCGroups.LocalWeight.weight_le_familyCardinal_of_basis
Documentation

Any explicit basis bounds the weight from above.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem weight_le_familyCardinal_of_basis {B : Set (Set X)} (hB : IsTopologicalBasis B) :
    weight X ≤ familyCardinal (X := X) B
theorem

localWeightAt_le_familyCardinal_of_basis

L73 ↗
ProCGroups.LocalWeight.localWeightAt_le_familyCardinal_of_basis
Documentation

Any explicit neighborhood basis at \(x\) bounds the local weight from above.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem localWeightAt_le_familyCardinal_of_basis {x : X} {B : Set (Set X)}
    (hB : IsNeighborhoodBasisAt (X := X) x B) :
    localWeightAt X x ≤ familyCardinal (X := X) B
theorem

localWeightAt_le_one_of_isOpen_singleton

L85 ↗
ProCGroups.LocalWeight.localWeightAt_le_one_of_isOpen_singleton
Documentation

If the singleton \(\{x\}\) is open, then the local weight at \(x\) is at most 1.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem localWeightAt_le_one_of_isOpen_singleton {x : X} (hx : IsOpen ({x} : Set X)) :
    localWeightAt X x ≤ 1
theorem

familyCardinal_mono

L108 ↗
ProCGroups.LocalWeight.familyCardinal_mono
Documentation

The family cardinal is monotone under inclusion of families.

Source context 12 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
omit [TopologicalSpace X] in
Lean source · statement
theorem familyCardinal_mono {B C : Set (Set X)} (hBC : B ⊆ C) :
    familyCardinal (X := X) B ≤ familyCardinal (X := X) C
theorem

familyCardinal_le_rho_of_clopenFamily

L121 ↗
ProCGroups.LocalWeight.familyCardinal_le_rho_of_clopenFamily
Documentation

Any family of clopen sets injects into the type of all clopen subsets, so its cardinality is bounded by \(\rho(X)\).

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem familyCardinal_le_rho_of_clopenFamily {B : Set (Set X)}
    (hB : ∀ U ∈ B, IsClopen U) :
    familyCardinal (X := X) B ≤ rho X
theorem

finite_of_finite_basisSubtype

L132 ↗
ProCGroups.LocalWeight.finite_of_finite_basisSubtype
Documentation

A finite basis on a \(T_1\) space forces the underlying space itself to be finite.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem finite_of_finite_basisSubtype [T1Space X] {B : Set (Set X)}
    (hB : IsTopologicalBasis B) [Finite { U : Set X // U ∈ B }] : Finite X
theorem

infinite_familySubtype_of_basis

L165 ↗
ProCGroups.LocalWeight.infinite_familySubtype_of_basis
Documentation

An infinite \(T_1\) space cannot have a finite topological basis.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem infinite_familySubtype_of_basis [T1Space X] [Infinite X] {B : Set (Set X)}
    (hB : IsTopologicalBasis B) : Infinite { U : Set X // U ∈ B }
theorem

exists_finset_basisSUnion_eq_of_isClopen

L177 ↗
ProCGroups.LocalWeight.exists_finset_basisSUnion_eq_of_isClopen
Documentation

In a compact space, every clopen set is the union of finitely many members of any chosen topological basis.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem exists_finset_basisSUnion_eq_of_isClopen [CompactSpace X] {B : Set (Set X)}
    (hB : IsTopologicalBasis B) {U : Set X} (hU : IsClopen U) :
    ∃ s : Finset { V : Set X // V ∈ B },
      U = ⋃₀ (Subtype.val '' (↑s : Set { V : Set X // V ∈ B }))
theorem

rho_le_familyCardinal_of_basis

L189 ↗
ProCGroups.LocalWeight.rho_le_familyCardinal_of_basis
Documentation

In an infinite compact Hausdorff space, every basis controls the number of clopen subsets.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem rho_le_familyCardinal_of_basis [CompactSpace X] [T2Space X] [Infinite X]
    {B : Set (Set X)} (hB : IsTopologicalBasis B) :
    rho X ≤ familyCardinal (X := X) B
theorem

rho_le_weight

L226 ↗
ProCGroups.LocalWeight.rho_le_weight
Documentation

For an infinite compact Hausdorff space, the cardinal invariant \(\rho(X)\) is bounded above by the topological weight of \(X\).

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem rho_le_weight [CompactSpace X] [T2Space X] [Infinite X] :
    rho X ≤ weight X
theorem

localWeightAt_le_weight

L240 ↗
ProCGroups.LocalWeight.localWeightAt_le_weight
Documentation

Every global basis yields a local basis at any chosen point, so the local weight is always bounded by the weight.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem localWeightAt_le_weight {x : X} :
    localWeightAt X x ≤ weight X
theorem

weight_le_rho_of_exists_clopenBasis

L266 ↗
ProCGroups.LocalWeight.weight_le_rho_of_exists_clopenBasis
Documentation

Any clopen basis bounds the weight by \(\rho(X)\).

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem weight_le_rho_of_exists_clopenBasis
    (hB : ∃ B : Set (Set X), IsTopologicalBasis B ∧ ∀ U ∈ B, IsClopen U) :
    weight X ≤ rho X
theorem

familyCardinal_eq_rho_of_clopenBasis

L277 ↗
ProCGroups.LocalWeight.familyCardinal_eq_rho_of_clopenBasis
Documentation

Any clopen basis of an infinite compact Hausdorff space has cardinality exactly \(\rho(X)\).

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem familyCardinal_eq_rho_of_clopenBasis [CompactSpace X] [T2Space X] [Infinite X]
    {B : Set (Set X)} (hB : IsTopologicalBasis B) (hClopen : ∀ U ∈ B, IsClopen U) :
    familyCardinal (X := X) B = rho X
theorem

weight_le_rho_of_clopenBasis

L288 ↗
ProCGroups.LocalWeight.weight_le_rho_of_clopenBasis
Documentation

If the clopen subsets already form a topological basis, the weight is bounded by the same cardinal invariant.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem weight_le_rho_of_clopenBasis
    (hBasis : IsTopologicalBasis { U : Set X | IsClopen U }) :
    weight X ≤ rho X
theorem

weight_eq_rho_of_clopenBasis

L297 ↗
ProCGroups.LocalWeight.weight_eq_rho_of_clopenBasis
Documentation

6.1(a) in the special case where all clopen subsets already form a basis.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem weight_eq_rho_of_clopenBasis [CompactSpace X] [T2Space X] [Infinite X]
    (hBasis : IsTopologicalBasis { U : Set X | IsClopen U }) :
    weight X = rho X
theorem

localWeightAt_le_rho_of_exists_clopenNeighborhoodBasis

L305 ↗
ProCGroups.LocalWeight.localWeightAt_le_rho_of_exists_clopenNeighborhoodBasis
Documentation

Any clopen neighborhood basis at \(x\) bounds the local weight at \(x\) by \(\rho(X)\).

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section CardinalInvariants
variable (X : Type u) [TopologicalSpace X]
Lean source · statement
theorem localWeightAt_le_rho_of_exists_clopenNeighborhoodBasis {x : X}
    (hB : ∃ B : Set (Set X),
      IsNeighborhoodBasisAt (X := X) x B ∧ ∀ U ∈ B, IsClopen U) :
    localWeightAt X x ≤ rho X
def

localWeight

L326 ↗
ProCGroups.LocalWeight.localWeight
Documentation

the local weight w₀(G) of a topological group is the local weight at 1.

The continuity assumptions needed for later results are imposed where they are used; the cardinal invariant itself only depends on the underlying topology and distinguished point.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section LocalWeightOfGroups
variable (G : Type u) [Group G] [TopologicalSpace G]
Lean source · statement
def localWeight : Cardinal
theorem

localWeight_le_weight

L330 ↗
ProCGroups.LocalWeight.localWeight_le_weight
Documentation

The local weight of a topological group is bounded by its weight.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section LocalWeightOfGroups
variable (G : Type u) [Group G] [TopologicalSpace G]
Lean source · statement
theorem localWeight_le_weight :
    localWeight G ≤ weight G
theorem

localWeight_le_rho_of_exists_clopenNeighborhoodBasis

L336 ↗
ProCGroups.LocalWeight.localWeight_le_rho_of_exists_clopenNeighborhoodBasis
Documentation

A clopen neighborhood basis of cardinal at most \(\rho\) bounds the local weight by \(\rho\).

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section LocalWeightOfGroups
variable (G : Type u) [Group G] [TopologicalSpace G]
Lean source · statement
theorem localWeight_le_rho_of_exists_clopenNeighborhoodBasis
    (hB : ∃ B : Set (Set G),
      IsNeighborhoodBasisAt (X := G) (1 : G) B ∧ ∀ U ∈ B, IsClopen U) :
    localWeight G ≤ rho G
def

leftTranslateFamily

L353 ↗
ProCGroups.LocalWeight.leftTranslateFamily
Documentation

The family of all left translates of members of \(B\). This is the global basis naturally associated to a neighborhood basis at \(1\).

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section GroupTranslateBases
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def leftTranslateFamily (B : Set (Set G)) : Set (Set G)
theorem

isTopologicalBasis_leftTranslateFamily

L357 ↗
ProCGroups.LocalWeight.isTopologicalBasis_leftTranslateFamily
Documentation

In a group, left translates of a neighborhood basis at \(1\) form a topological basis.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section GroupTranslateBases
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem isTopologicalBasis_leftTranslateFamily {B : Set (Set G)}
    (hB : IsNeighborhoodBasisAt (X := G) (1 : G) B) :
    IsTopologicalBasis (leftTranslateFamily (G := G) B)
theorem

weight_le_familyCardinal_leftTranslateFamily_of_neighborhoodBasis

L380 ↗
ProCGroups.LocalWeight.weight_le_familyCardinal_leftTranslateFamily_of_neighborhoodBasis
Documentation

Any neighborhood basis at \(1\) yields a global basis whose cardinality is the cardinality of its translate family.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section GroupTranslateBases
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem weight_le_familyCardinal_leftTranslateFamily_of_neighborhoodBasis {B : Set (Set G)}
    (hB : IsNeighborhoodBasisAt (X := G) (1 : G) B) :
    weight G ≤ familyCardinal (X := G) (leftTranslateFamily (G := G) B)
theorem

leftTranslate

L393 ↗
ProCGroups.LocalWeight.IsClopen.leftTranslate
Documentation

Left translation preserves clopen subsets in a topological group.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section GroupTranslateClopen
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem IsClopen.leftTranslate {U : Set G} (hU : IsClopen U) (g : G) :
    IsClopen (g • U)
theorem

weight_le_rho_of_exists_clopenNeighborhoodBasisAtOne

L404 ↗
ProCGroups.LocalWeight.weight_le_rho_of_exists_clopenNeighborhoodBasisAtOne
Documentation

If the identity has a clopen neighborhood basis, then w(G) \(\le\) \(\rho\)(G). The remaining work for the full proposition is the comparison with \(w_0(G)\) in the using cardinality-preserving form used in the book.

Source context 11 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section GroupTranslateClopen
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem weight_le_rho_of_exists_clopenNeighborhoodBasisAtOne
    (hB : ∃ B : Set (Set G),
      IsNeighborhoodBasisAt (X := G) (1 : G) B ∧ ∀ U ∈ B, IsClopen U) :
    weight G ≤ rho G
theorem

continuousMonoidHom_eq_of_eqOn_topologicalGeneratingSet

L423 ↗
ProCGroups.LocalWeight.continuousMonoidHom_eq_of_eqOn_topologicalGeneratingSet
Documentation

A continuous homomorphism out of a profinite group is determined by any topological generating set.

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem continuousMonoidHom_eq_of_eqOn_topologicalGeneratingSet
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {R : Type v} [Group R] [TopologicalSpace R] [T2Space R]
    {X : Set G} (hXgen : TopologicallyGenerates (G := G) X)
    {f g : ContinuousMonoidHom G R} (hfg : Set.EqOn f g X) :
    f = g
theorem

cardinal_continuousMap_to_finite_le_rho

L461 ↗
ProCGroups.LocalWeight.cardinal_continuousMap_to_finite_le_rho
Documentation

For a finite discrete codomain, the set of continuous maps from a profinite space has cardinality at most \(\rho(X)\).

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem cardinal_continuousMap_to_finite_le_rho
    (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X]
    [TotallyDisconnectedSpace X] [Infinite X]
    (H : Type v) [Finite H] [TopologicalSpace H] [DiscreteTopology H] :
    Cardinal.mk C(X, H) ≤ Cardinal.lift (rho X)
theorem

rho_subtype_le_rho_of_closed

L514 ↗
ProCGroups.LocalWeight.rho_subtype_le_rho_of_closed
Documentation

Passing to a closed subspace does not increase \(\rho\).

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem rho_subtype_le_rho_of_closed
    (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X]
    [TotallyDisconnectedSpace X] {A : Set X} (hAclosed : IsClosed A) :
    rho ↥A ≤ rho X
abbrev

openSubgroupIndexContinuousHom

L565 ↗
ProCGroups.LocalWeight.openSubgroupIndexContinuousHom
Documentation

The finite coset action is a continuous homomorphism into a discrete permutation group, with the finite-quotient certificate supplied by openness.

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
abbrev openSubgroupIndexContinuousHom
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    (H : Subgroup G) (hH : IsOpen (H : Set G)) {n : ℕ} (hn : Nat.card (G ⧸ H) = n) :
    ContinuousMonoidHom G (Equiv.Perm (Fin n))
theorem

rho_eq_of_homeomorph

L573 ↗
ProCGroups.LocalWeight.rho_eq_of_homeomorph
Documentation

The clopen-subset cardinal \(\rho\) is a topological invariant.

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem rho_eq_of_homeomorph
    (X Y : Type u) [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) :
    rho X = rho Y
theorem

rho_onePoint_eq_cardinal_of_infinite_discrete

L597 ↗
ProCGroups.LocalWeight.rho_onePoint_eq_cardinal_of_infinite_discrete
Documentation

For an infinite discrete space \(X\), the one-point compactification has exactly \(\#X\) clopen subsets: finite subsets coming from \(X\), and complements of finite subsets.

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem rho_onePoint_eq_cardinal_of_infinite_discrete
    (X : Type u) [TopologicalSpace X] [DiscreteTopology X] [Infinite X] :
    rho (OnePoint X) = Cardinal.mk X
theorem

rho_closure_eq_cardinal_of_generatesAndConvergesToOneAlongOpenSubgroups_infinite

L703 ↗
ProCGroups.LocalWeight.rho_closure_eq_cardinal_of_generatesAndConvergesToOneAlongOpenSubgroups_infinite
Documentation

The generating and convergence data imply the stated local-weight or cardinal-invariant relation.

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem rho_closure_eq_cardinal_of_generatesAndConvergesToOneAlongOpenSubgroups_infinite
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (X : Set G)
    (hX : GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X) (hXinfinite : Set.Infinite X)
    (hclosure : closure X = X ∪ ({1} : Set G)) :
    rho ↥(closure X) = Cardinal.mk X
theorem

exists_neighborhoodBasisAt_cardinal_le_of_localWeightAt_le

L800 ↗
ProCGroups.LocalWeight.exists_neighborhoodBasisAt_cardinal_le_of_localWeightAt_le
Documentation

The datum exists neighborhood Basis At cardinal le of local Weight At le fixes the component used in the corresponding finite-stage construction.

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem exists_neighborhoodBasisAt_cardinal_le_of_localWeightAt_le
    {X : Type u} [TopologicalSpace X] {x : X} {κ : Cardinal}
    (hcount : localWeightAt (X := X) x ≤ κ) :
    ∃ B : Set (Set X), IsNeighborhoodBasisAt (X := X) x B ∧ familyCardinal (X := X) B ≤ κ
theorem

localWeightAt_image_le_of_continuous_open

L825 ↗
ProCGroups.LocalWeight.localWeightAt_image_le_of_continuous_open
Documentation

Open maps do not increase local weight at the image point.

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem localWeightAt_image_le_of_continuous_open
    {X : Type u} {Y : Type u} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} {x : X} (hfcont : Continuous f) (hfopen : IsOpenMap f) :
    localWeightAt (X := Y) (f x) ≤ localWeightAt (X := X) x
theorem

exists_openNormalNeighborhoodBasisAtOne_cardinal_le_localWeight

L862 ↗
ProCGroups.LocalWeight.exists_openNormalNeighborhoodBasisAtOne_cardinal_le_localWeight
Documentation

In a profinite group, the identity admits a neighborhood basis of open normal subgroups whose indexing cardinality is bounded by \(w_0(G)\).

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · full declaration
theorem exists_openNormalNeighborhoodBasisAtOne_cardinal_le_localWeight
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
    ∃ ι : Type u, ∃ W : ι → OpenNormalSubgroup G,
      IsNeighborhoodBasisAt (X := G) (1 : G)
        (Set.range fun i : ι => (((W i : Subgroup G) : Set G))) ∧
      Cardinal.mk ι ≤ localWeight G := by
  rcases exists_neighborhoodBasisAt_cardinal_le_of_localWeightAt_le
      (X := G) (x := (1 : G)) (κ := localWeight G) le_rfl with
    ⟨B, hBbasis, hBcard⟩
  let ι : Type u := { U : Set G // U ∈ B }
  have hchoose :
      ∀ i : ι, ∃ N : OpenNormalSubgroup G, (N : Set G) ⊆ i.1 := by
    intro i
    have hi : IsOpen i.1 ∧ (1 : G) ∈ i.1 := hBbasis.1 i.1 i.2
    rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hi.1 hi.2 with
      ⟨N, hN⟩
    exact ⟨N, hN⟩
  choose W hW using hchoose
  refine ⟨ι, W, ?_, ?_⟩
  · constructor
    · intro U hU
      rcases hU with ⟨i, rfl⟩
      exact ⟨openNormalSubgroup_isOpen (G := G) (W i), (W i).one_mem'⟩
    · intro V hVopen h1V
      rcases hBbasis.2 V hVopen h1V with ⟨U, hUB, hUV⟩
      refine ⟨((W ⟨U, hUB⟩ : Subgroup G) : Set G), ?_, ?_⟩
      · exact ⟨⟨U, hUB⟩, rfl⟩
      · exact (hW ⟨U, hUB⟩).trans hUV
  · simpa [familyCardinal, ι] using hBcard
theorem

exists_openNormalNeighborhoodBasisAtOne_inClass_cardinal_le_localWeight

L897 ↗
ProCGroups.LocalWeight.exists_openNormalNeighborhoodBasisAtOne_inClass_cardinal_le_localWeight
Documentation

In a pro-\(C\) group, the identity admits a neighborhood basis of open normal subgroups whose quotients lie in \(C\), still indexed by at most \(w_0(G)\).

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · full declaration
theorem exists_openNormalNeighborhoodBasisAtOne_inClass_cardinal_le_localWeight
    (C : FiniteGroupClass.{u}) (G : Type u)
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hG : HasOpenNormalBasisInClass C G) :
    ∃ ι : Type u, ∃ W : ι → OpenNormalSubgroup G,
      (∀ i, C (G ⧸ (W i : Subgroup G))) ∧
      IsNeighborhoodBasisAt (X := G) (1 : G)
        (Set.range fun i : ι => (((W i : Subgroup G) : Set G))) ∧
      Cardinal.mk ι ≤ localWeight G := by
  rcases exists_openNormalNeighborhoodBasisAtOne_cardinal_le_localWeight (G := G) with
    ⟨ι, W, hWbasis, hWcard⟩
  have hchoose :
      ∀ i : ι, ∃ U : OpenNormalSubgroup G,
        C (G ⧸ (U : Subgroup G)) ∧ (((U : Subgroup G) : Set G)) ⊆ ((W i : Subgroup G) : Set G) := by
    intro i
    rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one
        (openNormalSubgroup_isOpen (G := G) (W i)) (W i).one_mem' with ⟨U, hUW⟩
    exact ⟨U.1, U.2, hUW⟩
  choose U hUC hUsub using hchoose
  refine ⟨ι, U, hUC, ?_, hWcard⟩
  constructor
  · intro V hV
    rcases hV with ⟨i, rfl⟩
    exact ⟨openNormalSubgroup_isOpen (G := G) (U i), (U i).one_mem'⟩
  · intro V hVopen hVone
    rcases hWbasis.2 V hVopen hVone with ⟨W', hW'range, hW'sub⟩
    rcases hW'range with ⟨i, rfl⟩
    refine ⟨((U i : Subgroup G) : Set G), ?_, (hUsub i).trans hW'sub⟩
    exact ⟨i, rfl⟩
theorem

iInf_eq_bot_of_openNormalNeighborhoodBasisAtOne

L929 ↗
ProCGroups.LocalWeight.iInf_eq_bot_of_openNormalNeighborhoodBasisAtOne
Documentation

A neighborhood basis at \(1\) consisting of open normal subgroups has trivial intersection.

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · full declaration
theorem iInf_eq_bot_of_openNormalNeighborhoodBasisAtOne
    (G : Type u) [Group G] [TopologicalSpace G] [T2Space G]
    {ι : Type v} (W : ι → OpenNormalSubgroup G)
    (hWbasis : IsNeighborhoodBasisAt (X := G) (1 : G)
      (Set.range fun i : ι => (((W i : Subgroup G) : Set G)))) :
    iInf (fun i => (W i : Subgroup G)) = (⊥ : Subgroup G) := by
  ext x
  constructor
  · intro hx
    by_cases hx1 : x = 1
    · simp only [hx1, one_mem]
    · have hxall : ∀ i : ι, x ∈ (W i : Subgroup G) := by
        rw [Subgroup.mem_iInf] at hx
        exact hx
      have hOpen : IsOpen ({x}ᶜ : Set G) := isClosed_singleton.isOpen_compl
      have hOne : (1 : G) ∈ ({x}ᶜ : Set G) := by
        simpa [Set.mem_compl_iff, eq_comm] using hx1
      rcases hWbasis.2 ({x}ᶜ : Set G) hOpen hOne with ⟨U, hUrange, hUsub⟩
      rcases hUrange with ⟨i, rfl⟩
      have : x ∈ ({x}ᶜ : Set G) := hUsub (hxall i)
      simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false] at this
  · intro hx
    have hx1 : x = 1 := by
      exact Subgroup.mem_bot.mp hx
    simp only [hx1, one_mem]
theorem

localWeight_le_rho_of_closedGeneratingSet

L959 ↗
ProCGroups.LocalWeight.localWeight_le_rho_of_closedGeneratingSet
Documentation

A closed topological generating subset of an infinite profinite group has clopen cardinal at least 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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem localWeight_le_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

aleph0_le_localWeight_of_infinite_profiniteGroup

L1142 ↗
ProCGroups.LocalWeight.aleph0_le_localWeight_of_infinite_profiniteGroup
Documentation

An infinite profinite group has local weight at least \(\aleph_0\).

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem aleph0_le_localWeight_of_infinite_profiniteGroup
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Infinite G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
    ℵ₀ ≤ localWeight G
theorem

localWeight_eq_weight_of_infinite_profiniteGroup

L1189 ↗
ProCGroups.LocalWeight.localWeight_eq_weight_of_infinite_profiniteGroup
Documentation

6.1(b). Local weight equals weight for an infinite profinite group.

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem localWeight_eq_weight_of_infinite_profiniteGroup
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Infinite G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
    localWeight G = weight G
theorem

weight_eq_rho_and_familyCardinal_eq_rho_of_profiniteSpace

L1264 ↗
ProCGroups.LocalWeight.weight_eq_rho_and_familyCardinal_eq_rho_of_profiniteSpace
Documentation

For an infinite profinite space, the weight agrees with the clopen cardinal invariant, and every clopen basis has the same cardinality.

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem weight_eq_rho_and_familyCardinal_eq_rho_of_profiniteSpace
    (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X]
    [TotallyDisconnectedSpace X] [Infinite X] :
    weight X = rho X ∧
      ∀ B : Set (Set X), IsTopologicalBasis B → (∀ U ∈ B, IsClopen U) →
        familyCardinal (X := X) B = rho X
theorem

localWeight_eq_weight_and_weight_eq_rho_of_infinite_profiniteGroup

L1280 ↗
ProCGroups.LocalWeight.localWeight_eq_weight_and_weight_eq_rho_of_infinite_profiniteGroup
Documentation

For an infinite profinite group, local weight, weight, and the clopen cardinal invariant all coincide.

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 v
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
Lean source · statement
theorem localWeight_eq_weight_and_weight_eq_rho_of_infinite_profiniteGroup
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Infinite G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
    localWeight G = weight G ∧ weight G = rho G

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.