Module

Profinite.lean

Nyll.ProCGroups.Presentations.Profinite

12 declarations indexed from sourceView source ↗

Module documentation

Presentations of profinite and pro-`C` groups

This module defines closed normal closures of relators and free pro-C presentations, together with their basic kernel and universal-property consequences.

Imports3

Mathlib.GroupTheory.PGroup
Nyll.ProCGroups.FreeProC.Basic
Nyll.ProCGroups.Topologies.TopologicallyCharacteristicSubgroups

Imported by12

def

closedNormalClosure

L29 ↗

ProCGroups.Presentations.Subgroup.closedNormalClosure

Documentation

The closed normal subgroup generated by a set of profinite relators.

Source context 5 commands

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

noncomputable section
namespace ProCGroups.Presentations
universe u
section ClosedNormalClosure
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

def Subgroup.closedNormalClosure (R : Set F) : Subgroup F

abbrev

closedNormalClosure

L33 ↗

ProCGroups.Presentations.closedNormalClosure

Documentation

The closed normal subgroup generated by a set of profinite relators.

Source context 5 commands

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

noncomputable section
namespace ProCGroups.Presentations
universe u
section ClosedNormalClosure
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

abbrev closedNormalClosure (R : Set F) : Subgroup F

instance

closedNormalClosure_normal

L37 ↗

ProCGroups.Presentations.closedNormalClosure_normal

Documentation

The closed normal closure of a relator set is a normal subgroup.

Source context 5 commands

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

noncomputable section
namespace ProCGroups.Presentations
universe u
section ClosedNormalClosure
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

instance closedNormalClosure_normal (R : Set F) : (closedNormalClosure R).Normal

theorem

closedNormalClosure_isClosed

L42 ↗

ProCGroups.Presentations.closedNormalClosure_isClosed

Documentation

The closed normal closure of a relator set is a closed subgroup.

Source context 5 commands

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

noncomputable section
namespace ProCGroups.Presentations
universe u
section ClosedNormalClosure
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

theorem closedNormalClosure_isClosed (R : Set F) :
    IsClosed ((closedNormalClosure R : Subgroup F) : Set F)

theorem

subset_closedNormalClosure

L47 ↗

ProCGroups.Presentations.subset_closedNormalClosure

Documentation

Every relator in \(R\) lies in the closed normal closure of \(R\).

Source context 5 commands

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

noncomputable section
namespace ProCGroups.Presentations
universe u
section ClosedNormalClosure
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

theorem subset_closedNormalClosure (R : Set F) :
    R ⊆ closedNormalClosure R

theorem

closedNormalClosure_le_closed_normal

L58 ↗

ProCGroups.Presentations.closedNormalClosure_le_closed_normal

Documentation

The closed normal closure of \(R\) is contained in any closed normal subgroup that contains \(R\).

Source context 5 commands

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

noncomputable section
namespace ProCGroups.Presentations
universe u
section ClosedNormalClosure
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

theorem closedNormalClosure_le_closed_normal
    {R : Set F} {N : Subgroup F} [N.Normal]
    (hNclosed : IsClosed (N : Set F)) (hR : R ⊆ N) :
    closedNormalClosure R ≤ N

def

IsFreePresentationOf

L68 ↗

ProCGroups.Presentations.IsFreePresentationOf

Documentation

A relator presentation whose source is a chosen free pro-C group.

Source context 3 commands

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

noncomputable section
namespace ProCGroups.Presentations
universe u

Lean source · statement

def IsFreePresentationOf
    (C : ProCGroups.FiniteGroupClass.{u})
    {X F G : Type u} [TopologicalSpace X]
    [Group F] [Group G]
    [TopologicalSpace F] [TopologicalSpace G]
    [IsTopologicalGroup F] [IsTopologicalGroup G]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (ι : X → F) (R : Set F) : Prop

def

π

L91 ↗

ProCGroups.Presentations.IsFreePresentationOf.π

Documentation

The chosen quotient map recorded by a free pro-C presentation.

Source context 11 commands

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

noncomputable section
namespace ProCGroups.Presentations
universe u
namespace IsFreePresentationOf
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F G : Type u} [TopologicalSpace X]
variable [Group F] [Group G]
variable [TopologicalSpace F] [TopologicalSpace G]
variable [IsTopologicalGroup F] [IsTopologicalGroup G]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F} {R : Set F}

Lean source · statement

def π (h : IsFreePresentationOf (G := G) C ι R) : F →ₜ* G

theorem

freeSource

L95 ↗

ProCGroups.Presentations.IsFreePresentationOf.freeSource

Documentation

The source of a free presentation is free pro-C.

Source context 11 commands

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

noncomputable section
namespace ProCGroups.Presentations
universe u
namespace IsFreePresentationOf
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F G : Type u} [TopologicalSpace X]
variable [Group F] [Group G]
variable [TopologicalSpace F] [TopologicalSpace G]
variable [IsTopologicalGroup F] [IsTopologicalGroup G]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F} {R : Set F}

Lean source · statement

theorem freeSource (h : IsFreePresentationOf (G := G) C ι R) :
    ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι

theorem

targetProC

L100 ↗

ProCGroups.Presentations.IsFreePresentationOf.targetProC

Documentation

The target of a free presentation is pro-C.

Source context 11 commands

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

noncomputable section
namespace ProCGroups.Presentations
universe u
namespace IsFreePresentationOf
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F G : Type u} [TopologicalSpace X]
variable [Group F] [Group G]
variable [TopologicalSpace F] [TopologicalSpace G]
variable [IsTopologicalGroup F] [IsTopologicalGroup G]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F} {R : Set F}

Lean source · statement

theorem targetProC (h : IsFreePresentationOf (G := G) C ι R) :
    ProCGroups.ProC.HasOpenNormalBasisInClass C G

theorem

π_surjective

L105 ↗

ProCGroups.Presentations.IsFreePresentationOf.π_surjective

Documentation

The chosen quotient map is surjective.

Source context 11 commands

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

noncomputable section
namespace ProCGroups.Presentations
universe u
namespace IsFreePresentationOf
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F G : Type u} [TopologicalSpace X]
variable [Group F] [Group G]
variable [TopologicalSpace F] [TopologicalSpace G]
variable [IsTopologicalGroup F] [IsTopologicalGroup G]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F} {R : Set F}

Lean source · statement

theorem π_surjective (h : IsFreePresentationOf (G := G) C ι R) :
    Function.Surjective h.π

theorem

kernel_eq_closedNormalClosure

L110 ↗

ProCGroups.Presentations.IsFreePresentationOf.kernel_eq_closedNormalClosure

Documentation

The kernel of the chosen quotient map is the closed normal closure of the relators.

Source context 11 commands

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

noncomputable section
namespace ProCGroups.Presentations
universe u
namespace IsFreePresentationOf
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {X F G : Type u} [TopologicalSpace X]
variable [Group F] [Group G]
variable [TopologicalSpace F] [TopologicalSpace G]
variable [IsTopologicalGroup F] [IsTopologicalGroup G]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable {ι : X → F} {R : Set F}

Lean source · statement

theorem kernel_eq_closedNormalClosure (h : IsFreePresentationOf (G := G) C ι R) :
    h.π.toMonoidHom.ker = closedNormalClosure R

Module documentation

Presentations of profinite and pro-C groups

Declarations

Presentations of profinite and pro-`C` groups