NYLL
Module

Convergence.lean

Nyll.ProCGroups.Generation.Convergence
9 declarations indexed from sourceView source ↗

Module documentation

Convergence of generating sets in profinite groups

The open-subgroup convergence predicate is shown to be stable under pointed continuous maps, subsets, and finite modifications. For a generating set containing one, the module identifies its closure with a compact one-point extension and proves that the convergent set is closed.

Imports4
Imported by2

Declarations

theorem

image_of_continuous_pointed

L35 ↗
ProCGroups.Generation.ConvergesToOneAlongOpenSubgroups.image_of_continuous_pointed
Documentation

A continuous map between topological groups that sends \(1\) to \(1\) carries convergent sets to convergent sets, provided the source is profinite.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.Generation
universe u v
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem ConvergesToOneAlongOpenSubgroups.image_of_continuous_pointed
    {H : Type v} [Group H] [TopologicalSpace H]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {f : G → H} (hf : Continuous f) (hf1 : f 1 = 1)
    {X : Set G} (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) :
    ConvergesToOneAlongOpenSubgroups (G := H) (f '' X)
theorem

mono

L58 ↗
ProCGroups.Generation.ConvergesToOneAlongOpenSubgroups.mono
Documentation

Passing to a subset preserves convergence to \(1\).

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.Generation
universe u v
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem ConvergesToOneAlongOpenSubgroups.mono {X Y : Set G}
    (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) (hYX : Y ⊆ X) :
    ConvergesToOneAlongOpenSubgroups (G := G) Y
theorem

union_finite

L68 ↗
ProCGroups.Generation.ConvergesToOneAlongOpenSubgroups.union_finite
Documentation

Finite enlargements preserve convergence to \(1\).

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.Generation
universe u v
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem ConvergesToOneAlongOpenSubgroups.union_finite {X F : Set G}
    (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) (hF : F.Finite) :
    ConvergesToOneAlongOpenSubgroups (G := G) (X ∪ F)
theorem

union_finite_iff

L89 ↗
ProCGroups.Generation.ConvergesToOneAlongOpenSubgroups.union_finite_iff
Documentation

Convergence to \(1\) is preserved and reflected by the indicated finite union, insertion, or continuous equivalence operation.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.Generation
universe u v
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem ConvergesToOneAlongOpenSubgroups.union_finite_iff {X F : Set G}
    (hF : F.Finite) :
    ConvergesToOneAlongOpenSubgroups (G := G) (X ∪ F) ↔ ConvergesToOneAlongOpenSubgroups (G :=
        G) X
theorem

insert_iff

L106 ↗
ProCGroups.Generation.ConvergesToOneAlongOpenSubgroups.insert_iff
Documentation

Convergence to \(1\) is preserved and reflected by the indicated finite union, insertion, or continuous equivalence operation.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.Generation
universe u v
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem ConvergesToOneAlongOpenSubgroups.insert_iff {X : Set G} {x : G} :
    ConvergesToOneAlongOpenSubgroups (G := G) (Set.insert x X) ↔
        ConvergesToOneAlongOpenSubgroups (G := G) X
theorem

union_one_iff

L129 ↗
ProCGroups.Generation.ConvergesToOneAlongOpenSubgroups.union_one_iff
Documentation

Convergence to \(1\) is preserved and reflected by the indicated finite union, insertion, or continuous equivalence operation.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.Generation
universe u v
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem ConvergesToOneAlongOpenSubgroups.union_one_iff {X : Set G} :
    ConvergesToOneAlongOpenSubgroups (G := G) (X ∪ ({1} : Set G)) ↔
        ConvergesToOneAlongOpenSubgroups (G := G) X
theorem

closure_generatorsConvergingToOne

L139 ↗
ProCGroups.Generation.closure_generatorsConvergingToOne
Documentation

A set converging to \(1\) is discrete away from \(1\), and if it is infinite its closure is obtained by adjoining the unique possible limit point \(1\).

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.Generation
universe u v
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem closure_generatorsConvergingToOne
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] {X : Set G}
    (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) :
    IsDiscrete (X \ {1}) ∧
      (Set.Infinite X → closure X = X ∪ ({1} : Set G))
theorem

isClosed_of_one_mem

L236 ↗
ProCGroups.Generation.ConvergesToOneAlongOpenSubgroups.isClosed_of_one_mem
Documentation

A convergent set containing its only possible limit point \(1\) is closed.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.Generation
universe u v
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem ConvergesToOneAlongOpenSubgroups.isClosed_of_one_mem
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] {X : Set G}
    (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) (h1 : (1 : G) ∈ X) :
    IsClosed X
def

closure_generatorsConvergingToOne_homeomorph_onePoint

L254 ↗
ProCGroups.Generation.closure_generatorsConvergingToOne_homeomorph_onePoint
Documentation

If \(X\) is infinite, converges to \(1\), and does not contain \(1\), then \(closure X\) is homeomorphic to the one-point compactification of the discrete space \(X\).

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.Generation
universe u v
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def closure_generatorsConvergingToOne_homeomorph_onePoint
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] {X : Set G}
    (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) (hXinfinite : X.Infinite) (h1X : (1 : G)
        ∉ X) :
    OnePoint X ≃ₜ closure X

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