NYLL
Module

Basic.lean

Nyll.ProCGroups.FiniteGeneration.Basic
21 declarations indexed from sourceView source ↗

Module documentation

Basic results on topological finite generation

This module defines topological finite generation and topologically characteristic subgroups, then relates finite generating sets to free-group maps and generator-converging families.

Imports2
Imported by17

Declarations

def

TopologicallyFinitelyGenerated

L31 ↗
ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated
Documentation

Finitely generated as a topological group.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def TopologicallyFinitelyGenerated
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop
def

IsTopologicallyCharacteristic

L36 ↗
ProCGroups.FiniteGeneration.IsTopologicallyCharacteristic
Documentation

A subgroup is topologically characteristic if every continuous automorphism preserves it.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def IsTopologicallyCharacteristic
    (G : Type u) [Group G] [TopologicalSpace G] (H : Subgroup G) : Prop
theorem

apply_mem_iff

L48 ↗
ProCGroups.FiniteGeneration.IsTopologicallyCharacteristic.apply_mem_iff
Documentation

Membership in a topologically characteristic subgroup is invariant under applying a continuous automorphism.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section Characteristic
omit [IsTopologicalGroup G]
Lean source · statement
theorem IsTopologicallyCharacteristic.apply_mem_iff {H : Subgroup G}
    (hH : IsTopologicallyCharacteristic (G := G) H) (φ : G ≃ₜ* G) {g : G} :
    φ g ∈ H ↔ g ∈ H
theorem

inf

L54 ↗
ProCGroups.FiniteGeneration.IsTopologicallyCharacteristic.inf
Documentation

Intersections of topologically characteristic subgroups are topologically characteristic.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section Characteristic
omit [IsTopologicalGroup G]
Lean source · statement
theorem IsTopologicallyCharacteristic.inf {H K : Subgroup G}
    (hH : IsTopologicallyCharacteristic (G := G) H) (hK : IsTopologicallyCharacteristic (G := G)
        K) :
    IsTopologicallyCharacteristic (G := G) (H ⊓ K)
theorem

sInf

L62 ↗
ProCGroups.FiniteGeneration.IsTopologicallyCharacteristic.sInf
Documentation

Arbitrary infima of topologically characteristic subgroups are topologically characteristic.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section Characteristic
omit [IsTopologicalGroup G]
Lean source · statement
theorem IsTopologicallyCharacteristic.sInf {S : Set (Subgroup G)}
    (hS : ∀ H ∈ S, IsTopologicallyCharacteristic (G := G) H) :
    IsTopologicallyCharacteristic (G := G) (sInf S)
theorem

iInf

L74 ↗
ProCGroups.FiniteGeneration.IsTopologicallyCharacteristic.iInf
Documentation

Indexed infima of topologically characteristic subgroups are topologically characteristic.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section Characteristic
omit [IsTopologicalGroup G]
Lean source · statement
theorem IsTopologicallyCharacteristic.iInf {ι : Sort*} {S : ι → Subgroup G}
    (hS : ∀ i, IsTopologicallyCharacteristic (G := G) (S i)) :
    IsTopologicallyCharacteristic (G := G) (iInf S)
theorem

top

L89 ↗
ProCGroups.FiniteGeneration.IsTopologicallyCharacteristic.top
Documentation

The top subgroup is topologically characteristic, since every continuous automorphism preserves it.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section Characteristic
omit [IsTopologicalGroup G]
Lean source · statement
theorem IsTopologicallyCharacteristic.top :
    IsTopologicallyCharacteristic (G := G) (⊤ : Subgroup G)
def

TopologicallyGeneratedByAtMost

L97 ↗
ProCGroups.FiniteGeneration.TopologicallyGeneratedByAtMost
Documentation

\(G\) can be topologically generated by at most \(n\) elements.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def TopologicallyGeneratedByAtMost
    (n : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Prop
theorem

mono

L103 ↗
ProCGroups.FiniteGeneration.TopologicallyGeneratedByAtMost.mono
Documentation

Increasing the allowed number of generators preserves bounded topological generation.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem TopologicallyGeneratedByAtMost.mono {m n : ℕ}
    (hmn : m ≤ n)
    (hG : TopologicallyGeneratedByAtMost (G := G) m) :
    TopologicallyGeneratedByAtMost (G := G) n
theorem

topologicallyFinitelyGenerated_iff_exists_topologicallyGeneratedByAtMost

L114 ↗
ProCGroups.FiniteGeneration.topologicallyFinitelyGenerated_iff_exists_topologicallyGeneratedByAtMost
Documentation

A group is topologically finitely generated if and only if it is generated by at most \(n\) elements for some natural number \(n\).

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicallyFinitelyGenerated_iff_exists_topologicallyGeneratedByAtMost :
    TopologicallyFinitelyGenerated G ↔
      ∃ n, TopologicallyGeneratedByAtMost (G := G) n
theorem

finiteSet_convergesToOneAlongOpenSubgroups

L125 ↗
ProCGroups.FiniteGeneration.finiteSet_convergesToOneAlongOpenSubgroups
Documentation

A finite set of elements converges to \(1\) in the profinite generating-family sense.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem finiteSet_convergesToOneAlongOpenSubgroups (s : Finset G) :
    ConvergesToOneAlongOpenSubgroups (G := G) (↑s : Set G)
theorem

topologicalRank_le_of_topologicallyGeneratedByAtMost

L133 ↗
ProCGroups.FiniteGeneration.topologicalRank_le_of_topologicallyGeneratedByAtMost
Documentation

If \(G\) is topologically generated by at most \(n\) elements, its topological rank is at most \(n\).

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicalRank_le_of_topologicallyGeneratedByAtMost {n : ℕ}
    (h : TopologicallyGeneratedByAtMost (G := G) n) :
    topologicalRank G ≤ n
theorem

topologicallyGenerates_range_comp_of_surjective

L151 ↗
ProCGroups.FiniteGeneration.topologicallyGenerates_range_comp_of_surjective
Documentation

The image of a topological generating family under a continuous surjective homomorphism topologically generates the codomain.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicallyGenerates_range_comp_of_surjective
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (φ : G →ₜ* H) (hφ : Function.Surjective φ)
    {ι : Sort w} (g : ι → G)
    (hg : TopologicallyGenerates (G := G) (Set.range g)) :
    TopologicallyGenerates (G := H) (Set.range (φ ∘ g))
theorem

of_surjective

L162 ↗
ProCGroups.FiniteGeneration.TopologicallyGeneratedByAtMost.of_surjective
Documentation

Bounded topological generation descends along continuous surjective homomorphisms.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem TopologicallyGeneratedByAtMost.of_surjective
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (φ : G →ₜ* H) (hφ : Function.Surjective φ) {n : ℕ}
    (hG : TopologicallyGeneratedByAtMost (G := G) n) :
    TopologicallyGeneratedByAtMost (G := H) n
theorem

topologicallyFinitelyGenerated_of_continuousSurjective

L175 ↗
ProCGroups.FiniteGeneration.topologicallyFinitelyGenerated_of_continuousSurjective
Documentation

Topological finite generation descends along continuous surjective homomorphisms.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicallyFinitelyGenerated_of_continuousSurjective
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (φ : G →ₜ* H) (hφ : Function.Surjective φ)
    (hG : TopologicallyFinitelyGenerated G) :
    TopologicallyFinitelyGenerated H
theorem

topologicallyGenerates_iff_subgroupClosure_eq_top_of_discrete

L185 ↗
ProCGroups.FiniteGeneration.topologicallyGenerates_iff_subgroupClosure_eq_top_of_discrete
Documentation

In the discrete case, topological generation is abstract subgroup generation.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicallyGenerates_iff_subgroupClosure_eq_top_of_discrete
    [DiscreteTopology G] {X : Set G} :
    TopologicallyGenerates (G := G) X ↔ Subgroup.closure X = ⊤
theorem

freeGroup_lift_surjective_of_topologicallyGenerates_discrete

L199 ↗
ProCGroups.FiniteGeneration.freeGroup_lift_surjective_of_topologicallyGenerates_discrete
Documentation

A map from a free group to a discrete group is surjective when the images of the chosen generators topologically generate the target; in the discrete topology this is exactly abstract generation.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem freeGroup_lift_surjective_of_topologicallyGenerates_discrete
    {X : Type v} [DiscreteTopology G] (g : X → G)
    (hg : TopologicallyGenerates (G := G) (Set.range g)) :
    Function.Surjective (FreeGroup.lift g)
theorem

topologicallyFinitelyGenerated_of_finite

L216 ↗
ProCGroups.FiniteGeneration.topologicallyFinitelyGenerated_of_finite
Documentation

A finite discrete group is topologically finitely generated.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicallyFinitelyGenerated_of_finite [Finite G] [DiscreteTopology G] :
    TopologicallyFinitelyGenerated G
theorem

topologicallyGeneratedByAtMost_of_topologicalRank_eq_nat

L228 ↗
ProCGroups.FiniteGeneration.topologicallyGeneratedByAtMost_of_topologicalRank_eq_nat
Documentation

If the topological rank of a profinite group is the natural number \(n\), then the group is topologically generated by at most \(n\) elements.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem topologicallyGeneratedByAtMost_of_topologicalRank_eq_nat
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] {n : ℕ}
    (hd : topologicalRank G = n) :
    TopologicallyGeneratedByAtMost (G := G) n
theorem

exists_generatingTuple_of_topologicalRank_le_of_finite

L253 ↗
ProCGroups.FiniteGeneration.exists_generatingTuple_of_topologicalRank_le_of_finite
Documentation

A finite upper bound on the topological rank gives an explicit generating tuple of that length.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
section Basic
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem exists_generatingTuple_of_topologicalRank_le_of_finite
    (hG : TopologicallyFinitelyGenerated G) {n : ℕ} (hd : topologicalRank G ≤ n) :
    ∃ g : Fin n → G, TopologicallyGenerates (G := G) (Set.range g)
theorem

topologicalRank_inverseLimit_le_of_componentBound

L320 ↗
ProCGroups.FiniteGeneration.topologicalRank_inverseLimit_le_of_componentBound
Documentation

If every finite stage of a surjective inverse system has topological rank at most \(n\), then so does the inverse limit.

Source context 5 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.FiniteGeneration
universe u v w
open ProCGroups.Generation
Lean source · statement
theorem topologicalRank_inverseLimit_le_of_componentBound
    {I : Type v} [Preorder I]
    (S : ProCGroups.InverseSystems.InverseSystem (I := I))
    [Nonempty I] [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)] [∀ i, Finite (S.X i)]
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I))
    (hsurj : ∀ {i j : I} (hij : i ≤ j), Function.Surjective (S.map hij))
    {n : ℕ} (hbound : ∀ i, topologicalRank (S.X i) ≤ n) :
    topologicalRank S.inverseLimit ≤ n

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