Module

Rows.lean

Nyll.ProCGroups.ProP.Fox.Rows

6 declarations indexed from sourceView source ↗

Module documentation

Completed Fox rows of displayed relators

The displayed finite relation family and the whole presentation kernel are mapped into the same completed Fox-coordinate module. The closed coefficient span below is the finite relation module used by the filtered construction.

Imports1

Nyll.ProCGroups.ProP.Fox.Derivative

Imported by3

def

displayedRelatorInKernel

L35 ↗

ClassFieldTower.ProP.displayedRelatorInKernel

Documentation

A displayed relator bundled as a point of the presentation kernel.

Source context 9 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 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 displayedRelatorInKernel
    (P : FiniteProPPresentation p d r sourceData G) (i : Fin r) :
    P.quotient.toMonoidHom.ker

def

displayedRelatorFoxRow

L41 ↗

ClassFieldTower.ProP.displayedRelatorFoxRow

Documentation

The completed Fox row produced by one displayed relator.

Source context 9 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 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 displayedRelatorFoxRow
    (P : FiniteProPPresentation p d r sourceData G) (i : Fin r) :
    PresentationFoxCoordinates (p := p) (d := d) (G := G)

def

kernelFoxRow

L47 ↗

ClassFieldTower.ProP.kernelFoxRow

Documentation

The completed Fox row produced by an arbitrary kernel element.

Source context 9 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 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 kernelFoxRow
    (P : FiniteProPPresentation p d r sourceData G)
    (x : P.quotient.toMonoidHom.ker) :
    PresentationFoxCoordinates (p := p) (d := d) (G := G)

theorem

kernelFoxRow_displayedRelator

L54 ↗

ClassFieldTower.ProP.kernelFoxRow_displayedRelator

Documentation

Displayed rows are the restriction of the full kernel-row family.

Source context 9 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 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 kernelFoxRow_displayedRelator
    (P : FiniteProPPresentation p d r sourceData G) (i : Fin r) :
    kernelFoxRow P (displayedRelatorInKernel P i) =
      displayedRelatorFoxRow P i

theorem

kernel_eq_displayed_closedNormalClosure

L62 ↗

ClassFieldTower.ProP.kernel_eq_displayed_closedNormalClosure

Documentation

The kernel is the closed normal closure of the displayed family at the completed-Fox interface.

Source context 9 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 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_displayed_closedNormalClosure
    (P : FiniteProPPresentation p d r sourceData G) :
    P.quotient.toMonoidHom.ker =
      ProCGroups.Presentations.closedNormalClosure (Set.range P.relator)

def

displayedRelatorFoxRowClosedSpan

L69 ↗

ClassFieldTower.ProP.displayedRelatorFoxRowClosedSpan

Documentation

Closed coefficient submodule generated by the finite displayed rows.

Source context 9 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 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 displayedRelatorFoxRowClosedSpan
    (P : FiniteProPPresentation p d r sourceData G) :
    Submodule
      (PresentationFoxCoefficientRing (p := p) (G := G))
      (PresentationFoxCoordinates (p := p) (d := d) (G := G))

Module documentation

Completed Fox rows of displayed relators

Declarations

displayedRelatorInKernel

displayedRelatorFoxRow

kernelFoxRow

kernelFoxRow_displayedRelator

kernel_eq_displayed_closedNormalClosure

displayedRelatorFoxRowClosedSpan