Module

QuotientCriteria.lean

Nyll.ProCGroups.Generation.QuotientCriteria

3 declarations indexed from sourceView source ↗

Module documentation

Detecting topological generation in finite quotients

This module characterizes topological generation in inverse limits by generation of every finite-stage image. It specializes the criterion to quotients by open normal subgroups, both for a set alone and for a set together with a fixed subgroup.

Imports5

Imported by5

theorem

topologicallyGenerates_iff_forall_projection_inverseLimit

L38 ↗

ProCGroups.Generation.topologicallyGenerates_iff_forall_projection_inverseLimit

Documentation

Topological generation in a surjective inverse system can be checked after every projection.

Source context 9 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.InverseSystems
open ProCGroups.ProC
open ProCGroups
section Generators
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem topologicallyGenerates_iff_forall_projection_inverseLimit
    {I : Type v} [Preorder I] {S : InverseSystem (I := I)} [Nonempty I]
    [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (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))
    {X : Set S.inverseLimit} :
    TopologicallyGenerates (G := S.inverseLimit) X ↔
      ∀ i, TopologicallyGenerates (G := S.X i) (S.projection i '' X)

theorem

topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient

L115 ↗

ProCGroups.Generation.topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient

Documentation

A closed-normal quotient version of topological generation: \(X \cup N\) generates if and only if the image of \(X\) generates modulo every open normal subgroup containing \(N\).

Source context 10 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.InverseSystems
open ProCGroups.ProC
open ProCGroups
section Generators
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [T2Space G] in

Lean source · statement

theorem topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient
    {N : Subgroup G} [N.Normal]
    {X : Set G} :
    TopologicallyGenerates (G := G) (X ∪ (N : Set G)) ↔
      ∀ U : OpenNormalSubgroup G, N ≤ (U : Subgroup G) →
        TopologicallyGenerates (G := G ⧸ (U : Subgroup G))
          ((QuotientGroup.mk' (U : Subgroup G)) '' X)

theorem

topologicallyGenerates_iff_forall_quotientProj_image

L258 ↗

ProCGroups.Generation.topologicallyGenerates_iff_forall_quotientProj_image

Documentation

This is the direct finite-quotient test for topological generation, phrased with the bundled quotient projections.

Source context 10 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.InverseSystems
open ProCGroups.ProC
open ProCGroups
section Generators
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [T2Space G] in

Lean source · statement

theorem topologicallyGenerates_iff_forall_quotientProj_image
    {X : Set G} :
    TopologicallyGenerates (G := G) X ↔
      ∀ U : OpenNormalSubgroup G,
        TopologicallyGenerates (G := G ⧸ (U : Subgroup G))
          (OpenNormalSubgroup.quotientProj U '' X)

Module documentation

Detecting topological generation in finite quotients

Declarations

topologicallyGenerates_iff_forall_projection_inverseLimit

topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient

topologicallyGenerates_iff_forall_quotientProj_image