Module

ModPFiniteStage.lean

Nyll.ProCGroups.ProP.Fox.ModPFiniteStage

9 declarations indexed from sourceView source ↗

Module documentation

Finite mod-p Fox stages of a presentation

A finite p-group quotient of the presented group determines a reflected finite Fox stage. Relation-ideal differentiation supplies module-level and function-level exactness of the relation boundary followed by the Fox boundary at that stage.

Imports3

Imported by2

def

presentationModPFiniteStageIndex

L43 ↗

ClassFieldTower.ProP.presentationModPFiniteStageIndex

Documentation

The p-coefficient differential-module index over a chosen target finite p-group quotient.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
noncomputable section
universe u
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 presentationModPFiniteStageIndex
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    ZCCompletedDifferentialModuleIndex
      (FiniteGroupClass.pGroup p) P.quotient.toMonoidHom

abbrev

presentationModPFiniteStageKernel

L56 ↗

ClassFieldTower.ProP.presentationModPFiniteStageKernel

Documentation

The reflected free-group kernel at the selected mod-p stage.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
noncomputable section
universe u
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

abbrev presentationModPFiniteStageKernel
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    Subgroup (FreeGroup (ULift.{u} (Fin d)))

abbrev

presentationModPFiniteStageTarget

L66 ↗

ClassFieldTower.ProP.presentationModPFiniteStageTarget

Documentation

The reflected target quotient at the selected mod-p stage.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
noncomputable section
universe u
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

abbrev presentationModPFiniteStageTarget
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) : Type u

def

presentationModPFiniteStageQMap

L74 ↗

ClassFieldTower.ProP.presentationModPFiniteStageQMap

Documentation

The canonical comparison from G/U to the reflected free quotient.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
noncomputable section
universe u
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 presentationModPFiniteStageQMap
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    (G ⧸ (U : Subgroup G)) →* presentationModPFiniteStageTarget P U hU

theorem

presentationModPFiniteStageQMap_injective

L84 ↗

ClassFieldTower.ProP.presentationModPFiniteStageQMap_injective

Documentation

The quotient comparison is injective.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
noncomputable section
universe u
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 presentationModPFiniteStageQMap_injective
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    Function.Injective (presentationModPFiniteStageQMap P U hU)

theorem

presentationModPFiniteStageQMap_generator

L118 ↗

ClassFieldTower.ProP.presentationModPFiniteStageQMap_generator

Documentation

The quotient comparison identifies each chosen presentation generator with the corresponding generator of the reflected free quotient.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
noncomputable section
universe u
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 presentationModPFiniteStageQMap_generator
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (x : ULift.{u} (Fin d)) :
    presentationModPFiniteStageQMap P U hU
        (QuotientGroup.mk (P.quotient (presentationChosenGenerator P x))) =
      QuotientGroup.mk'
        (presentationModPFiniteStageKernel P U hU) (FreeGroup.of x)

theorem

presentationModPFiniteStageIndex_modulus

L132 ↗

ClassFieldTower.ProP.presentationModPFiniteStageIndex_modulus

Documentation

The selected relation-reflection stage has coefficient modulus p.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
noncomputable section
universe u
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 presentationModPFiniteStageIndex_modulus
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    (presentationModPFiniteStageIndex P U hU).target.1.modulus = p

theorem

presentationModPFiniteStageRelationBoundaryModuleExact

L141 ↗

ClassFieldTower.ProP.presentationModPFiniteStageRelationBoundaryModuleExact

Documentation

Relation-ideal differentiation gives module-level exactness at the selected mod-p reflected stage.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
noncomputable section
universe u
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 presentationModPFiniteStageRelationBoundaryModuleExact
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    foxAlgebraicStageRelationBoundaryModuleExact
      (X := ULift.{u} (Fin d))
      (presentationModPFiniteStageKernel P U hU) p

theorem

presentationModPFiniteStageRelationBoundaryExact

L153 ↗

ClassFieldTower.ProP.presentationModPFiniteStageRelationBoundaryExact

Documentation

The finite-stage relation boundary followed by the Fox boundary is exact.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
noncomputable section
universe u
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 presentationModPFiniteStageRelationBoundaryExact
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    foxAlgebraicStageRelationBoundaryExact
      (X := ULift.{u} (Fin d))
      (presentationModPFiniteStageKernel P U hU) p

Module documentation

Finite mod-p Fox stages of a presentation

Declarations