Module

Basic.lean

Nyll.ProCGroups.Generation.Basic

41 declarations indexed from sourceView source ↗

Module documentation

Topological generation and convergent generating sets

This module defines topological generation, convergence to one, the corresponding cardinal ranks, and the finite word-product filtration of a set. It develops extensionality, closed-generated-subgroup, image, quotient, and continuous-equivalence lemmas that form the basic API for generator arguments in profinite groups.

Imports3

Mathlib.Topology.Algebra.ClopenNhdofOne
Mathlib.Topology.Algebra.ContinuousMonoidHom
Mathlib.Topology.Algebra.Nonarchimedean.Basic

Imported by19

def

TopologicallyGenerates

L32 ↗

ProCGroups.Generation.TopologicallyGenerates

Documentation

X topologically generates G if the abstract subgroup generated by X is dense in G.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def TopologicallyGenerates (X : Set G) : Prop

def

ConvergesToOne

L36 ↗

ProCGroups.Generation.ConvergesToOne

Documentation

A set converges to 1 when its subtype inclusion tends to 1 along the cofinite filter.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def ConvergesToOne (X : Set G) : Prop

def

ConvergesToOneAlongOpenSubgroups

L43 ↗

ProCGroups.Generation.ConvergesToOneAlongOpenSubgroups

Documentation

The weaker condition obtained by testing convergence only against open subgroups.

This agrees with ConvergesToOne for nonarchimedean groups, but is deliberately kept separate: on a general topological group, open subgroups need not form a neighborhood basis at 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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def ConvergesToOneAlongOpenSubgroups (X : Set G) : Prop

theorem

of_finite

L48 ↗

ProCGroups.Generation.ConvergesToOne.of_finite

Documentation

A finite set converges 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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem ConvergesToOne.of_finite {X : Set G} (hX : X.Finite) :
    ConvergesToOne (G := G) X

theorem

of_finite

L56 ↗

ProCGroups.Generation.ConvergesToOneAlongOpenSubgroups.of_finite

Documentation

Every finite set satisfies the open-subgroup convergence condition.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem ConvergesToOneAlongOpenSubgroups.of_finite {X : Set G} (hX : X.Finite) :
    ConvergesToOneAlongOpenSubgroups (G := G) X

theorem

to_alongOpenSubgroups

L65 ↗

ProCGroups.Generation.ConvergesToOne.to_alongOpenSubgroups

Documentation

Genuine convergence implies convergence when tested only on open subgroups.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem ConvergesToOne.to_alongOpenSubgroups {X : Set G}
    (hX : ConvergesToOne (G := G) X) :
    ConvergesToOneAlongOpenSubgroups (G := G) X

theorem

to_convergesToOne

L86 ↗

ProCGroups.Generation.ConvergesToOneAlongOpenSubgroups.to_convergesToOne

Documentation

In a nonarchimedean group, testing against open subgroups detects genuine convergence.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem ConvergesToOneAlongOpenSubgroups.to_convergesToOne
    [NonarchimedeanGroup G] {X : Set G}
    (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) :
    ConvergesToOne (G := G) X

theorem

convergesToOne_iff_alongOpenSubgroups

L110 ↗

ProCGroups.Generation.convergesToOne_iff_alongOpenSubgroups

Documentation

For nonarchimedean groups, the genuine and open-subgroup convergence predicates agree.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem convergesToOne_iff_alongOpenSubgroups [NonarchimedeanGroup G] {X : Set G} :
    ConvergesToOne (G := G) X ↔
      ConvergesToOneAlongOpenSubgroups (G := G) X

def

GeneratesAndConvergesToOne

L117 ↗

ProCGroups.Generation.GeneratesAndConvergesToOne

Documentation

A set which topologically generates and converges to 1 in the filter sense.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def GeneratesAndConvergesToOne (X : Set G) : Prop

def

GeneratesAndConvergesToOneAlongOpenSubgroups

L121 ↗

ProCGroups.Generation.GeneratesAndConvergesToOneAlongOpenSubgroups

Documentation

A generating set satisfying only the weaker open-subgroup convergence condition.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def GeneratesAndConvergesToOneAlongOpenSubgroups (X : Set G) : Prop

def

topologicalRank

L129 ↗

ProCGroups.Generation.topologicalRank

Documentation

The least cardinality of a topological generating set.

The candidate set is always nonempty: Set.univ topologically generates every group. Thus this definition never uses the accidental value Cardinal.sInf ∅ = 0.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def topologicalRank
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Cardinal

def

convergentGeneratorRank

L139 ↗

ProCGroups.Generation.convergentGeneratorRank

Documentation

The optional least size of a generating set which also converges to 1.

Unlike topologicalRank, the relevant family of cardinals can be empty, so absence is represented by none instead of being silently identified with cardinal zero.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def convergentGeneratorRank
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Option Cardinal

theorem

topologicalRank_le_mk_of_topologicallyGenerates

L151 ↗

ProCGroups.Generation.topologicalRank_le_mk_of_topologicallyGenerates

Documentation

The topological rank is bounded by the cardinality of any topological generating set.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicalRank_le_mk_of_topologicallyGenerates {X : Set G}
    (hX : TopologicallyGenerates (G := G) X) :
    topologicalRank G ≤ Cardinal.mk X

theorem

topologicalRank_le_mk_of_generatesAndConvergesToOneAlongOpenSubgroups

L159 ↗

ProCGroups.Generation.topologicalRank_le_mk_of_generatesAndConvergesToOneAlongOpenSubgroups

Documentation

In particular, an open-subgroup-convergent generating set bounds the topological rank.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicalRank_le_mk_of_generatesAndConvergesToOneAlongOpenSubgroups {X : Set G}
    (hX : GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X) :
    topologicalRank G ≤ Cardinal.mk X

theorem

exists_topologicallyGenerates_card_eq_topologicalRank

L165 ↗

ProCGroups.Generation.exists_topologicallyGenerates_card_eq_topologicalRank

Documentation

There is a topological generating set whose cardinality is exactly the topological rank.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem exists_topologicallyGenerates_card_eq_topologicalRank :
    ∃ X : Set G, TopologicallyGenerates (G := G) X ∧
      Cardinal.mk X = topologicalRank G

theorem

topologicalRank_ne_zero

L181 ↗

ProCGroups.Generation.topologicalRank_ne_zero

Documentation

A nontrivial T1 topological group has nonzero topological rank.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicalRank_ne_zero [T1Space G] [Nontrivial G] :
    topologicalRank G ≠ 0

def

wordProducts

L214 ↗

ProCGroups.Generation.wordProducts

Documentation

Iterated products of words in \(X\), with \(\mathrm{wordProducts}(X,0)=\{1\}\) and \(\mathrm{wordProducts}(X,n+1)=\mathrm{wordProducts}(X,n)\cdot 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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

def wordProducts (X : Set G) : ℕ → Set G
  | 0 => {1}
  | n + 1 => wordProducts X n * X

theorem

topologicallyGenerates_iff_dense

L219 ↗

ProCGroups.Generation.topologicallyGenerates_iff_dense

Documentation

Topological generation is equivalently density of the abstract subgroup generated by the set.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_iff_dense {X : Set G} :
    TopologicallyGenerates (G := G) X ↔ Dense ((Subgroup.closure X : Subgroup G) : Set G)

theorem

continuousMonoidHom_ext_of_topologicallyGenerates

L228 ↗

ProCGroups.Generation.continuousMonoidHom_ext_of_topologicallyGenerates

Documentation

Continuous homomorphisms out of a topologically generated group are determined by their values on the generating set.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem continuousMonoidHom_ext_of_topologicallyGenerates
    {R : Type v} [Group R] [TopologicalSpace R] [T2Space R]
    {X : Set G} (hX : TopologicallyGenerates (G := G) X)
    {f g : ContinuousMonoidHom G R} (hfg : ∀ x ∈ X, f x = g x) :
    f = g

def

closedSubgroupGenerated

L265 ↗

ProCGroups.Generation.closedSubgroupGenerated

Documentation

The closed subgroup topologically generated by a set.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

def closedSubgroupGenerated (X : Set G) : ClosedSubgroup G where
  toSubgroup := (Subgroup.closure X).topologicalClosure
  isClosed' := Subgroup.isClosed_topologicalClosure _

def

closedSubgroupGeneratedMap

L270 ↗

ProCGroups.Generation.closedSubgroupGeneratedMap

Documentation

The canonical map from an indexed family into the closed subgroup it topologically generates.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def closedSubgroupGeneratedMap {A : Type v} (φ : A → G) :
    A → (closedSubgroupGenerated (G := G) (Set.range φ) : Subgroup G)

theorem

closedSubgroupGeneratedMap_topologicallyGenerates

L276 ↗

ProCGroups.Generation.closedSubgroupGeneratedMap_topologicallyGenerates

Documentation

The canonical indexed family topologically generates its closed generated subgroup.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem closedSubgroupGeneratedMap_topologicallyGenerates {A : Type v} (φ : A → G) :
    TopologicallyGenerates
      (G := (closedSubgroupGenerated (G := G) (Set.range φ) : Subgroup G))
      (Set.range (closedSubgroupGeneratedMap (G := G) φ))

theorem

map_mem_closedSubgroupGenerated_image

L323 ↗

ProCGroups.Generation.map_mem_closedSubgroupGenerated_image

Documentation

Membership in a closed generated subgroup is preserved by continuous homomorphisms, after mapping the generating set.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem map_mem_closedSubgroupGenerated_image
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (φ : G →ₜ* H) {X : Set G} {y : G}
    (hy : y ∈ (closedSubgroupGenerated (G := G) X : Subgroup G)) :
    φ y ∈ (closedSubgroupGenerated (G := H) (φ '' X) : Subgroup H)

theorem

map_mem_closedSubgroupGenerated_singleton

L345 ↗

ProCGroups.Generation.map_mem_closedSubgroupGenerated_singleton

Documentation

Membership in a topologically generated cyclic closed subgroup is preserved by continuous homomorphisms.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem map_mem_closedSubgroupGenerated_singleton
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (φ : G →ₜ* H) (x : G) {y : G}
    (hy : y ∈ (closedSubgroupGenerated (G := G) ({x} : Set G) : Subgroup G)) :
    φ y ∈ (closedSubgroupGenerated (G := H) ({φ x} : Set H) : Subgroup H)

theorem

zpowers_subtype_topologically_generated_by_generator

L355 ↗

ProCGroups.Generation.zpowers_subtype_topologically_generated_by_generator

Documentation

The distinguished element g algebraically generates its subgroup of powers.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

theorem zpowers_subtype_topologically_generated_by_generator
    {G₀ : Type*} [Group G₀] (g : G₀) :
    let cyc : Subgroup G₀ := Subgroup.zpowers g
    let gcyc : cyc := ⟨g, Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩⟩
    ∀ z : cyc, z ∈ Subgroup.zpowers gcyc := by
  intro cyc gcyc z
  rcases Subgroup.mem_zpowers_iff.mp z.2 with ⟨k, hk⟩
  refine Subgroup.mem_zpowers_iff.mpr ⟨k, ?_⟩
  apply Subtype.ext
  simpa [gcyc] using hk

theorem

map_mem_zpowers_of_topologicallyGenerates_singleton

L367 ↗

ProCGroups.Generation.map_mem_zpowers_of_topologicallyGenerates_singleton

Documentation

A finite discrete image of a topologically cyclic group is algebraically cyclic.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem map_mem_zpowers_of_topologicallyGenerates_singleton
    {A : Type u} [TopologicalSpace A] [Group A] [IsTopologicalGroup A]
    {B : Type v} [TopologicalSpace B] [Group B] [IsTopologicalGroup B]
    [DiscreteTopology B]
    (f : A →ₜ* B) {x a : A}
    (hxgen : TopologicallyGenerates (G := A) ({x} : Set A)) :
    f a ∈ Subgroup.zpowers (f x)

theorem

monoidHom_map_mem_zpowers_of_topologicallyGenerates_singleton

L398 ↗

ProCGroups.Generation.monoidHom_map_mem_zpowers_of_topologicallyGenerates_singleton

Documentation

MonoidHom version of map_mem_zpowers_of_topologicallyGenerates_singleton.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem monoidHom_map_mem_zpowers_of_topologicallyGenerates_singleton
    {A : Type u} [TopologicalSpace A] [Group A] [IsTopologicalGroup A]
    {B : Type v} [TopologicalSpace B] [Group B] [IsTopologicalGroup B]
    [DiscreteTopology B]
    (f : A →* B) (hf : Continuous f) {x a : A}
    (hxgen : TopologicallyGenerates (G := A) ({x} : Set A)) :
    f a ∈ Subgroup.zpowers (f x)

theorem

zpowers_image_le_closedSubgroupGenerated_map

L419 ↗

ProCGroups.Generation.zpowers_image_le_closedSubgroupGenerated_map

Documentation

Algebraic powers of the image of \(x\) lie in the image of the closed subgroup generated by \(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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem zpowers_image_le_closedSubgroupGenerated_map
    {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    {B : Type v} [Group B]
    (q : Q →* B) (x : Q) :
    Subgroup.zpowers (q x) ≤
      ((closedSubgroupGenerated ({x} : Set Q) : ClosedSubgroup Q) :
        Subgroup Q).map q

theorem

topologicallyGenerates_singleton_of_denseRange_mint

L443 ↗

ProCGroups.Generation.topologicallyGenerates_singleton_of_denseRange_mint

Documentation

A dense homomorphic image of the infinite cyclic group is topologically generated by the image of \(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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_singleton_of_denseRange_mint
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (f : Multiplicative ℤ →* H) (hf : DenseRange f) :
    TopologicallyGenerates (G := H) ({f (Multiplicative.ofAdd 1)} : Set H)

theorem

topologicallyGenerates_closure_iff

L473 ↗

ProCGroups.Generation.topologicallyGenerates_closure_iff

Documentation

Topological generation is unchanged by closing the generating set.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_closure_iff {X : Set G} :
    TopologicallyGenerates (G := G) X ↔ TopologicallyGenerates (G := G) (closure X)

theorem

topologicallyGenerates_insert_one_iff

L503 ↗

ProCGroups.Generation.topologicallyGenerates_insert_one_iff

Documentation

Adding \(1\) to a topological generating set does not change generation.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_insert_one_iff {X : Set G} :
    TopologicallyGenerates (G := G) (insert (1 : G) X) ↔ TopologicallyGenerates (G := G) X

theorem

topologicallyGenerates_union_one_iff

L508 ↗

ProCGroups.Generation.topologicallyGenerates_union_one_iff

Documentation

Union with \(\{1\}\) does not change topological generation.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_union_one_iff {X : Set G} :
    TopologicallyGenerates (G := G) (X ∪ ({1} : Set G)) ↔ TopologicallyGenerates (G := G) X

theorem

closure_nontrivial_range_eq_closure_range

L517 ↗

ProCGroups.Generation.closure_nontrivial_range_eq_closure_range

Documentation

Removing occurrences of 1 from a parametrized generating range does not change its abstract subgroup closure.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [TopologicalSpace G] [IsTopologicalGroup G] in

Lean source · statement

theorem closure_nontrivial_range_eq_closure_range
    {α : Type v} (f : α → G) :
    Subgroup.closure ({g | ∃ a, g = f a ∧ g ≠ 1} : Set G) =
      Subgroup.closure (Set.range f)

theorem

topologicallyGenerates_mono

L535 ↗

ProCGroups.Generation.topologicallyGenerates_mono

Documentation

Topological generation is monotone in the generating set.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_mono {X Y : Set G}
    (hX : TopologicallyGenerates (G := G) X) (hXY : X ⊆ Y) :
    TopologicallyGenerates (G := G) Y

theorem

topologicallyGenerates_of_subset_closure

L548 ↗

ProCGroups.Generation.topologicallyGenerates_of_subset_closure

Documentation

A topological generating set may be replaced by any set whose abstract closure contains it.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_of_subset_closure {X Y : Set G}
    (hX : TopologicallyGenerates (G := G) X)
    (hXY : X ⊆ ((Subgroup.closure Y : Subgroup G) : Set G)) :
    TopologicallyGenerates (G := G) Y

theorem

topologicallyGenerates_image_of_continuousSurjective

L564 ↗

ProCGroups.Generation.topologicallyGenerates_image_of_continuousSurjective

Documentation

Topological generation pushes forward along continuous surjective homomorphisms.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_image_of_continuousSurjective
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (f : G →* H) (hf : Continuous f) (hfsurj : Function.Surjective f)
    {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
    TopologicallyGenerates (G := H) (f '' X)

theorem

topologicallyGenerates_image_of_continuousMonoidHom_surjective

L583 ↗

ProCGroups.Generation.topologicallyGenerates_image_of_continuousMonoidHom_surjective

Documentation

Continuous-homomorphism form of push-forward for topological generation.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_image_of_continuousMonoidHom_surjective
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (f : G →ₜ* H) (hfsurj : Function.Surjective f)
    {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
    TopologicallyGenerates (G := H) (f '' X)

theorem

continuousMonoidHom_surjective_of_topologicallyGenerates_subset_range

L596 ↗

ProCGroups.Generation.continuousMonoidHom_surjective_of_topologicallyGenerates_subset_range

Documentation

A continuous homomorphism from a compact group onto a Hausdorff target is surjective as soon as its closed range contains a topological generating set of the target.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [IsTopologicalGroup G] in

Lean source · statement

theorem continuousMonoidHom_surjective_of_topologicallyGenerates_subset_range
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    [CompactSpace G] [T2Space H]
    (f : G →ₜ* H) {X : Set H} (hX : TopologicallyGenerates (G := H) X)
    (hXrange : X ⊆ ((f.toMonoidHom.range : Subgroup H) : Set H)) :
    Function.Surjective f

theorem

topologicallyGenerates_quotient_image

L626 ↗

ProCGroups.Generation.topologicallyGenerates_quotient_image

Documentation

Topological generation descends to every quotient by a normal subgroup.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_quotient_image
    (N : Subgroup G) [N.Normal]
    {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
    TopologicallyGenerates (G := G ⧸ N) ((QuotientGroup.mk' N) '' X)

theorem

topologicallyGenerates_continuousMulEquiv_image

L639 ↗

ProCGroups.Generation.topologicallyGenerates_continuousMulEquiv_image

Documentation

Topological generation is preserved by continuous multiplicative equivalences.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_continuousMulEquiv_image
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
    TopologicallyGenerates (G := H) (e '' X)

theorem

topologicallyGenerates_continuousMulEquiv_image_iff

L647 ↗

ProCGroups.Generation.topologicallyGenerates_continuousMulEquiv_image_iff

Documentation

Topological generation is transported across a continuous multiplicative equivalence.

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
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_continuousMulEquiv_image_iff
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) {X : Set G} :
    TopologicallyGenerates (G := H) (e '' X) ↔ TopologicallyGenerates (G := G) X

Module documentation

Topological generation and convergent generating sets

Declarations