NYLL
Module

Minimal.lean

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

Module documentation

Minimal pro-p presentations

Minimality means that the presentation kernel lies in the source power--commutator core. The quotient therefore descends the source Frattini quotient to a continuous surjection from the target.

Imports2
Imported by5

Declarations

instance

(anonymous instance)

L38 ↗
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
instance : (closedPowerCommutator p sourceData.carrier).Normal
def

IsMinimal

L43 ↗
ClassFieldTower.ProP.FiniteProPPresentation.IsMinimal
Documentation

A finite presentation is minimal when its kernel lies in the source Frattini power--commutator core.

Source context 12 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]
local instance : (closedPowerCommutator p sourceData.carrier).Normal :=
  closedPowerCommutator_normal p sourceData.carrier
Lean source · statement
def IsMinimal (P : FiniteProPPresentation p d r sourceData G) : Prop
theorem

relator_mem_closedPowerCommutator

L48 ↗
ClassFieldTower.ProP.FiniteProPPresentation.relator_mem_closedPowerCommutator
Documentation

Every displayed relator of a minimal presentation lies in the source power--commutator core.

Source context 12 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]
local instance : (closedPowerCommutator p sourceData.carrier).Normal :=
  closedPowerCommutator_normal p sourceData.carrier
Lean source · statement
theorem relator_mem_closedPowerCommutator
    (P : FiniteProPPresentation p d r sourceData G)
    (hP : P.IsMinimal) (i : Fin r) :
    P.relator i ∈ closedPowerCommutator p sourceData.carrier
def

targetToSourcePowerCommutatorQuotient

L56 ↗
ClassFieldTower.ProP.FiniteProPPresentation.targetToSourcePowerCommutatorQuotient
Documentation

A minimal quotient descends the source Frattini quotient map back from the target.

Source context 12 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]
local instance : (closedPowerCommutator p sourceData.carrier).Normal :=
  closedPowerCommutator_normal p sourceData.carrier
Lean source · statement
def targetToSourcePowerCommutatorQuotient
    (P : FiniteProPPresentation p d r sourceData G) (hP : P.IsMinimal) :
    G →ₜ* powerCommutatorQuotient p sourceData.carrier
theorem

targetToSourcePowerCommutatorQuotient_apply

L88 ↗
ClassFieldTower.ProP.FiniteProPPresentation.targetToSourcePowerCommutatorQuotient_apply
Documentation

The descended map agrees with the source Frattini quotient on presentation lifts.

Source context 12 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]
local instance : (closedPowerCommutator p sourceData.carrier).Normal :=
  closedPowerCommutator_normal p sourceData.carrier
Lean source · statement
theorem targetToSourcePowerCommutatorQuotient_apply
    (P : FiniteProPPresentation p d r sourceData G) (hP : P.IsMinimal)
    (x : sourceData.carrier) :
    P.targetToSourcePowerCommutatorQuotient hP (P.quotient x) =
      powerCommutatorQuotientMk p sourceData.carrier x
theorem

targetToSourcePowerCommutatorQuotient_surjective

L105 ↗
ClassFieldTower.ProP.FiniteProPPresentation.targetToSourcePowerCommutatorQuotient_surjective
Documentation

The descended target-to-source Frattini quotient map is surjective.

Source context 12 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]
local instance : (closedPowerCommutator p sourceData.carrier).Normal :=
  closedPowerCommutator_normal p sourceData.carrier
Lean source · statement
theorem targetToSourcePowerCommutatorQuotient_surjective
    (P : FiniteProPPresentation p d r sourceData G) (hP : P.IsMinimal) :
    Function.Surjective (P.targetToSourcePowerCommutatorQuotient hP)

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