NYLL
Module

Basic.lean

Nyll.ProCGroups.ProP.Presentation.Basic
6 declarations indexed from sourceView source ↗

Module documentation

Finite pro-p presentations

This leaf packages an actual finite free pro-p source, a displayed finite relator family, and the existing IsFreePresentationOf certificate. The free source data is a type index, rather than a structure field, so its canonical group and topology instances remain syntactically determined.

Imports2
Imported by6

Declarations

structure

FiniteProPPresentation

L32 ↗
ClassFieldTower.ProP.FiniteProPPresentation
Documentation

A finite pro-p presentation with d generators and r displayed relators.

Source context 6 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.Presentations
noncomputable section
universe u
Lean source · full declaration
structure FiniteProPPresentation
    (p d r : ℕ) [Fact p.Prime]
    (sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p))
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] where
  /-- The chosen free basis has cardinality `d`. -/
  basisCard : Cardinal.mk sourceData.basis = d
  /-- The displayed family of `r` relators in the free source. -/
  relator : Fin r → sourceData.carrier
  /-- The quotient is the closed normal quotient by the displayed relators. -/
  isPresentation :
    IsFreePresentationOf
      (X := ULift.{u} (Fin d))
      (F := sourceData.carrier)
      (G := G)
      (FiniteGroupClass.pGroup p)
      (CrowellExactSequence.freeProCChosenULiftFamilyOfBasisCard
        sourceData basisCard)
      (Set.range relator)
def

quotient

L64 ↗
ClassFieldTower.ProP.FiniteProPPresentation.quotient
Documentation

The canonical quotient map selected by the underlying presentation.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.Presentations
noncomputable section
universe u
namespace FiniteProPPresentation
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def quotient (P : FiniteProPPresentation p d r sourceData G) :
    sourceData.carrier →ₜ* G
theorem

quotient_surjective

L69 ↗
ClassFieldTower.ProP.FiniteProPPresentation.quotient_surjective
Documentation

The presentation quotient is surjective.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.Presentations
noncomputable section
universe u
namespace FiniteProPPresentation
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem quotient_surjective (P : FiniteProPPresentation p d r sourceData G) :
    Function.Surjective P.quotient
theorem

kernel_eq_closedNormalClosure

L74 ↗
ClassFieldTower.ProP.FiniteProPPresentation.kernel_eq_closedNormalClosure
Documentation

The kernel is the closed normal closure of the displayed relators.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.Presentations
noncomputable section
universe u
namespace FiniteProPPresentation
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem kernel_eq_closedNormalClosure
    (P : FiniteProPPresentation p d r sourceData G) :
    P.quotient.toMonoidHom.ker = closedNormalClosure (Set.range P.relator)
theorem

targetProP

L80 ↗
ClassFieldTower.ProP.FiniteProPPresentation.targetProP
Documentation

The target has a pro-p open-normal basis.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.Presentations
noncomputable section
universe u
namespace FiniteProPPresentation
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem targetProP (P : FiniteProPPresentation p d r sourceData G) :
    ProC.HasPGroupOpenNormalBasis p G
theorem

relator_mem_kernel

L85 ↗
ClassFieldTower.ProP.FiniteProPPresentation.relator_mem_kernel
Documentation

Every displayed relator lies in the presentation kernel.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open ProCGroups.Presentations
noncomputable section
universe u
namespace FiniteProPPresentation
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem relator_mem_kernel
    (P : FiniteProPPresentation p d r sourceData G) (i : Fin r) :
    P.relator i ∈ P.quotient.toMonoidHom.ker

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