Module

Predicates.lean

Nyll.ProCGroups.ProC.InverseLimits.Predicates

5 declarations indexed from sourceView source ↗

Module documentation

Finite-quotient predicates for profinite groups

This file defines cyclic, abelian, and \(p\)-group open-normal quotient bases. It derives the cyclic basis associated with a single topological generator and the basic implications between these predicates.

Imports3

Imported by21

def

HasCyclicOpenNormalBasis

L33 ↗

ProCGroups.ProC.HasCyclicOpenNormalBasis

Documentation

The identity-neighborhood basis property for open normal subgroups with cyclic quotients.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
section
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def HasCyclicOpenNormalBasis
    (G : Type u) [Group G] [TopologicalSpace G] : Prop

def

HasAbelianOpenNormalBasis

L38 ↗

ProCGroups.ProC.HasAbelianOpenNormalBasis

Documentation

The identity-neighborhood basis property for open normal subgroups with abelian quotients.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
section
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def HasAbelianOpenNormalBasis
    (G : Type u) [Group G] [TopologicalSpace G] : Prop

def

HasPGroupOpenNormalBasis

L44 ↗

ProCGroups.ProC.HasPGroupOpenNormalBasis

Documentation

The identity-neighborhood basis property for open normal subgroups with finite \(p\)-group quotients.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
section
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def HasPGroupOpenNormalBasis (p : ℕ) [Fact (Nat.Prime p)]
    (G : Type u) [Group G] [TopologicalSpace G] : Prop

theorem

hasAbelianOpenNormalBasis

L51 ↗

ProCGroups.ProC.HasCyclicOpenNormalBasis.hasAbelianOpenNormalBasis

Documentation

A cyclic open-normal quotient basis is also an abelian open-normal quotient basis.

Source context 8 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
section
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace HasCyclicOpenNormalBasis

Lean source · statement

theorem hasAbelianOpenNormalBasis (hG : HasCyclicOpenNormalBasis G) : HasAbelianOpenNormalBasis
    G

theorem

hasCyclicOpenNormalBasis_of_topologicallyGenerates_singleton

L62 ↗

ProCGroups.ProC.hasCyclicOpenNormalBasis_of_topologicallyGenerates_singleton

Documentation

A profinite group topologically generated by one element has a cyclic open-normal quotient basis.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
section
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem hasCyclicOpenNormalBasis_of_topologicallyGenerates_singleton
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G] {g : G}
    (hg : Generation.TopologicallyGenerates (G := G) ({g} : Set G)) :
    HasCyclicOpenNormalBasis G

Module documentation

Finite-quotient predicates for profinite groups

Declarations

HasCyclicOpenNormalBasis

HasAbelianOpenNormalBasis

HasPGroupOpenNormalBasis

hasAbelianOpenNormalBasis

hasCyclicOpenNormalBasis_of_topologicallyGenerates_singleton