Module

InitialForm.lean

Nyll.ProCGroups.ProP.Presentation.InitialForm

7 declarations indexed from sourceView source ↗

Module documentation

Initial forms in the augmentation filtration

The degree-n initial form is constructed in the concrete quotient Iⁿ/Iⁿ⁺¹. A supplied depth witness produces the numerator element, and the quotient criterion identifies vanishing with membership one layer deeper.

Imports1

Nyll.ProCGroups.ProP.Presentation.RelatorDepth

Imported by1

Nyll.ProCGroups.ProP.Presentation.All

def

nextClosedAugmentationLayerIn

L33 ↗

ClassFieldTower.ProP.nextClosedAugmentationLayerIn

Documentation

The next closed augmentation layer, viewed inside the current layer.

Source context 7 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}

Lean source · statement

def nextClosedAugmentationLayerIn (n : ℕ) :
    Submodule (ModPCompletedGroupAlgebra p sourceData.carrier)
      (closedAugmentationPower p sourceData.carrier n)

abbrev

AugmentationInitialFormSpace

L41 ↗

ClassFieldTower.ProP.AugmentationInitialFormSpace

Documentation

The degree-n associated-graded augmentation piece Iⁿ/Iⁿ⁺¹.

Source context 7 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}

Lean source · statement

abbrev AugmentationInitialFormSpace (n : ℕ)

def

zassenhausInitialFormAt

L46 ↗

ClassFieldTower.ProP.zassenhausInitialFormAt

Documentation

The degree-n initial form of an element with a depth-n witness.

Source context 7 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}

Lean source · statement

def zassenhausInitialFormAt
    (n : ℕ) (g : sourceData.carrier)
    (hg : ZassenhausDepthAtLeast p n g) :
    AugmentationInitialFormSpace (p := p) (sourceData := sourceData) n

theorem

zassenhausInitialFormAt_eq_zero_iff

L55 ↗

ClassFieldTower.ProP.zassenhausInitialFormAt_eq_zero_iff

Documentation

The initial form vanishes exactly when the element lies one layer deeper.

Source context 7 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}

Lean source · statement

theorem zassenhausInitialFormAt_eq_zero_iff
    (n : ℕ) (g : sourceData.carrier)
    (hg : ZassenhausDepthAtLeast p n g) :
    zassenhausInitialFormAt (sourceData := sourceData) n g hg = 0 ↔
      ZassenhausDepthAtLeast p (n + 1) g

def

relatorInitialFormAt

L71 ↗

ClassFieldTower.ProP.FiniteProPPresentation.relatorInitialFormAt

Documentation

Initial form of one displayed relator.

Source context 11 commands

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

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

Lean source · statement

def relatorInitialFormAt
    (P : FiniteProPPresentation p d r sourceData G)
    (n : ℕ) (i : Fin r) (hi : P.RelatorZassenhausDepthAtLeast n i) :
    AugmentationInitialFormSpace (p := p) (sourceData := sourceData) n

def

relatorInitialFormFamilyAt

L78 ↗

ClassFieldTower.ProP.FiniteProPPresentation.relatorInitialFormFamilyAt

Documentation

The displayed relation family in one associated-graded degree.

Source context 11 commands

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

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

Lean source · statement

def relatorInitialFormFamilyAt
    (P : FiniteProPPresentation p d r sourceData G)
    (n : ℕ) (hrel : ∀ i, P.RelatorZassenhausDepthAtLeast n i) :
    Fin r → AugmentationInitialFormSpace (p := p) (sourceData := sourceData) n

def

minimalRelatorInitialFormFamily

L85 ↗

ClassFieldTower.ProP.FiniteProPPresentation.minimalRelatorInitialFormFamily

Documentation

Minimality canonically produces the degree-two initial-form family.

Source context 11 commands

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

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

Lean source · statement

def minimalRelatorInitialFormFamily
    (P : FiniteProPPresentation p d r sourceData G) (hP : P.IsMinimal) :
    Fin r → AugmentationInitialFormSpace (p := p) (sourceData := sourceData) 2

Module documentation

Initial forms in the augmentation filtration

Declarations

nextClosedAugmentationLayerIn

AugmentationInitialFormSpace

zassenhausInitialFormAt

zassenhausInitialFormAt_eq_zero_iff

relatorInitialFormAt

relatorInitialFormFamilyAt

minimalRelatorInitialFormFamily