NYLL
Module

MetrizabilityAndQuotients.lean

Nyll.ProCGroups.LocalWeight.MetrizabilityAndQuotients
10 declarations indexed from sourceView source ↗

Module documentation

Local weight, quotients, and metrizability

This file develops local weight for quotients and open subgroups, relates countable local weight to descending open-normal chains, and characterizes metrizability of profinite groups. It also records consequences of topological finite generation.

Imports7
Imported by2

Declarations

def

quotientLocalWeight

L44 ↗
ProCGroups.LocalWeight.quotientLocalWeight
Documentation
  1. Quotient local weight at the identity coset.
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
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section QuotientLocalWeightStatements
section QuotientLocalWeight
variable (G : Type u) [Group G] [TopologicalSpace G]
Lean source · statement
def quotientLocalWeight (H : Subgroup G) : Cardinal
theorem

quotientLocalWeight_eq_localWeight

L51 ↗
ProCGroups.LocalWeight.quotientLocalWeight_eq_localWeight
Documentation

The quotient by a closed normal subgroup has the expected local weight computed from finite quotients.

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
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section QuotientLocalWeightStatements
section QuotientLocalWeight
variable (G : Type u) [Group G] [TopologicalSpace G]
Lean source · statement
theorem quotientLocalWeight_eq_localWeight (H : Subgroup G) [H.Normal] :
    quotientLocalWeight (G := G) H = localWeight (G ⧸ H)
theorem

quotientLocalWeight_mono_of_le

L56 ↗
ProCGroups.LocalWeight.quotientLocalWeight_mono_of_le
Documentation

Enlarging the denominator subgroup does not increase quotient local weight.

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
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section QuotientLocalWeightStatements
section QuotientLocalWeight
variable (G : Type u) [Group G] [TopologicalSpace G]
Lean source · statement
theorem quotientLocalWeight_mono_of_le
    [IsTopologicalGroup G] {H K : Subgroup G} [H.Normal] [K.Normal] (hHK : H ≤ K) :
    quotientLocalWeight (G := G) K ≤ quotientLocalWeight (G := G) H
theorem

localWeight_openSubgroup_eq

L97 ↗
ProCGroups.LocalWeight.localWeight_openSubgroup_eq
Documentation

An open subgroup has the same local weight as the ambient profinite group.

Source context 10 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
section QuotientLocalWeightStatements
Lean source · statement
theorem localWeight_openSubgroup_eq
    (G : Type u) [Group G] [TopologicalSpace G]
    (H : OpenSubgroup G) :
    localWeight ↥(H : Subgroup G) = localWeight G
theorem

allFinite_normalSubgroupClosed

L159 ↗
ProCGroups.LocalWeight.FiniteGroupClass.allFinite_normalSubgroupClosed
Documentation

The class of all finite groups is closed under normal subgroups.

Source context 10 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
section FiniteGroupClassHelpers
Lean source · statement
theorem FiniteGroupClass.allFinite_normalSubgroupClosed :
    FiniteGroupClass.NormalSubgroupClosed FiniteGroupClass.allFinite
theorem

setInfinite_of_cardinal_ge_aleph0

L166 ↗
ProCGroups.LocalWeight.setInfinite_of_cardinal_ge_aleph0
Documentation

A set whose cardinality is at least \(\aleph_0\) is infinite.

Source context 10 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
section FiniteGroupClassHelpers
Lean source · statement
theorem setInfinite_of_cardinal_ge_aleph0
    {α : Type u} (X : Set α) (hX : ℵ₀ ≤ Cardinal.mk X) : Set.Infinite X
theorem

hasCountableDescendingOpenNormalChainAtOne_of_localWeight_le_aleph0

L179 ↗
ProCGroups.LocalWeight.hasCountableDescendingOpenNormalChainAtOne_of_localWeight_le_aleph0
Documentation

A profinite group with \(w_0(G) \le \aleph_0\) admits a countable descending open-normal basis at \(1\).

Source context 10 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
section FiniteGroupClassHelpers
Lean source · statement
theorem hasCountableDescendingOpenNormalChainAtOne_of_localWeight_le_aleph0
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hcount : localWeight G ≤ ℵ₀) :
    ProCGroups.ProC.HasCountableOpenNormalBasisAtOne G
theorem

normal

L225 ↗
ProCGroups.LocalWeight.IsTopologicallyCharacteristic.normal
Documentation

A topologically characteristic subgroup is normal.

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
open ProCGroups.ProC ProCGroups.Generation
open ProCGroups.FiniteGeneration
section FiniteGroupClassHelpers
section CharacteristicHelpers
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem IsTopologicallyCharacteristic.normal {H : Subgroup G}
    (hH : IsTopologicallyCharacteristic G H) : H.Normal
theorem

metrizable_iff_hasCountableDescendingOpenNormalChainAtOne

L250 ↗
ProCGroups.LocalWeight.metrizable_iff_hasCountableDescendingOpenNormalChainAtOne
Documentation

Helper criterion: metrizability is equivalent to a countable descending open-normal basis at \(1\).

Source context 10 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
section FiniteGroupClassHelpers
Lean source · statement
theorem metrizable_iff_hasCountableDescendingOpenNormalChainAtOne
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
    Nonempty (MetrizableSpace G) ↔ ProCGroups.ProC.HasCountableOpenNormalBasisAtOne G
theorem

hasCountableDescendingOpenNormalChainAtOne_of_topologicallyFinitelyGenerated

L323 ↗
ProCGroups.LocalWeight.hasCountableDescendingOpenNormalChainAtOne_of_topologicallyFinitelyGenerated
Documentation

Topologically finitely generated profinite groups have a countable descending open-normal basis at \(1\).

Source context 10 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
section FiniteGroupClassHelpers
Lean source · statement
theorem hasCountableDescendingOpenNormalChainAtOne_of_topologicallyFinitelyGenerated
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (hgen : TopologicallyFinitelyGenerated G) :
    ProCGroups.ProC.HasCountableOpenNormalBasisAtOne G

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