NYLL
Module

ModPBoundary.lean

Nyll.ProCGroups.ProP.Fox.ModPBoundary
15 declarations indexed from sourceView source ↗

Module documentation

Mod-p Fox boundary and displayed relation matrix

The chosen presentation generators define the completed mod-p Fox boundary. The mod-p presentation derivative satisfies its fundamental formula, so the displayed relator rows give a finite linear map whose composite with the boundary is zero.

Imports3
Imported by4

Declarations

abbrev

presentationChosenGenerator

L41 ↗
ClassFieldTower.ProP.presentationChosenGenerator
Documentation

The chosen finite free generator attached to a presentation coordinate.

Source context 12 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
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 presentationChosenGenerator
    (P : FiniteProPPresentation p d r sourceData G)
    (i : ULift.{u} (Fin d)) : sourceData.carrier
def

presentationModPFoxBoundary

L47 ↗
ClassFieldTower.ProP.presentationModPFoxBoundary
Documentation

The mod-p Fox boundary determined by the images of the chosen generators.

Source context 12 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
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 presentationModPFoxBoundary
    (P : FiniteProPPresentation p d r sourceData G) :
    PresentationModPFoxCoordinates (p := p) (d := d) (G := G) →ₗ[
      ModPCompletedGroupAlgebra p G] ModPCompletedGroupAlgebra p G
theorem

presentationModPFoxBoundary_apply

L55 ↗
ClassFieldTower.ProP.presentationModPFoxBoundary_apply
Documentation

Evaluation of the presentation boundary is its finite Fox sum.

Source context 12 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
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 presentationModPFoxBoundary_apply
    (P : FiniteProPPresentation p d r sourceData G)
    (v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G)) :
    presentationModPFoxBoundary P v =
      ∑ i, v i *
        groupLikeDifference p G (P.quotient (presentationChosenGenerator P i))
theorem

presentationFoxDerivative_chosenGenerator

L64 ↗
ClassFieldTower.ProP.presentationFoxDerivative_chosenGenerator
Documentation

The integral presentation derivative has standard values on the chosen generators.

Source context 12 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
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 presentationFoxDerivative_chosenGenerator
    (P : FiniteProPPresentation p d r sourceData G)
    (i : ULift.{u} (Fin d)) :
    presentationFoxDerivative P (presentationChosenGenerator P i) =
      Pi.single i (1 : PresentationFoxCoefficientRing (p := p) (G := G))
theorem

presentationFoxBoundary_derivative

L97 ↗
ClassFieldTower.ProP.presentationFoxBoundary_derivative
Documentation

The integral completed Fox boundary of the presentation derivative.

Source context 12 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
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 · full declaration
theorem presentationFoxBoundary_derivative
    (P : FiniteProPPresentation p d r sourceData G)
    (f : sourceData.carrier) :
    freeProCZCCompletedFoxBoundary
        (FiniteGroupClass.pGroup p)
        (fun i : ULift.{u} (Fin d) ↦
          P.quotient (presentationChosenGenerator P i))
        (presentationFoxDerivative P f) =
      zcCompletedGroupAlgebraBoundary
        (FiniteGroupClass.pGroup p) P.quotient.toMonoidHom f := by
  exact freeProCZCBoundary_of_topologicalGeneration
    (FiniteGroupClass.pGroup p)
    (freeProCChosenULiftFamilyOfBasisCard_generates sourceData P.basisCard)
    P.quotient.toMonoidHom (presentationFoxDerivative P)
    (continuous_presentationFoxDerivative P) P.quotient.continuous
    (presentationFoxDerivative_chosenGenerator P) f
theorem

presentationModPFoxBoundary_derivative

L115 ↗
ClassFieldTower.ProP.presentationModPFoxBoundary_derivative
Documentation

The mod-p Fox fundamental formula for the presentation derivative.

Source context 12 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
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 presentationModPFoxBoundary_derivative
    (P : FiniteProPPresentation p d r sourceData G)
    (f : sourceData.carrier) :
    presentationModPFoxBoundary P (presentationModPFoxDerivative P f) =
      groupLikeDifference p G (P.quotient f)
def

displayedRelatorModPFoxRow

L142 ↗
ClassFieldTower.ProP.displayedRelatorModPFoxRow
Documentation

The mod-p Fox row of one displayed relator.

Source context 12 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
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 displayedRelatorModPFoxRow
    (P : FiniteProPPresentation p d r sourceData G) (i : Fin r) :
    PresentationModPFoxCoordinates (p := p) (d := d) (G := G)
def

presentationModPRelationMatrix

L148 ↗
ClassFieldTower.ProP.presentationModPRelationMatrix
Documentation

The finite displayed relation matrix over the mod-p completed group algebra.

Source context 12 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
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 presentationModPRelationMatrix
    (P : FiniteProPPresentation p d r sourceData G) :
    (Fin r → ModPCompletedGroupAlgebra p G) →ₗ[
      ModPCompletedGroupAlgebra p G]
      PresentationModPFoxCoordinates (p := p) (d := d) (G := G)
theorem

presentationModPFoxBoundary_displayedRelatorModPFoxRow

L157 ↗
ClassFieldTower.ProP.presentationModPFoxBoundary_displayedRelatorModPFoxRow
Documentation

Each displayed relation row is killed by the mod-p Fox boundary.

Source context 12 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
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 presentationModPFoxBoundary_displayedRelatorModPFoxRow
    (P : FiniteProPPresentation p d r sourceData G) (i : Fin r) :
    presentationModPFoxBoundary P (displayedRelatorModPFoxRow P i) = 0
theorem

presentationModPFoxBoundary_comp_relationMatrix

L165 ↗
ClassFieldTower.ProP.presentationModPFoxBoundary_comp_relationMatrix
Documentation

The displayed relation matrix followed by the Fox boundary is zero.

Source context 12 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
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 presentationModPFoxBoundary_comp_relationMatrix
    (P : FiniteProPPresentation p d r sourceData G) :
    (presentationModPFoxBoundary P).comp (presentationModPRelationMatrix P) = 0
theorem

continuous_presentationModPFoxBoundary

L176 ↗
ClassFieldTower.ProP.continuous_presentationModPFoxBoundary
Documentation

The mod-p Fox boundary is continuous.

Source context 12 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
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 continuous_presentationModPFoxBoundary
    (P : FiniteProPPresentation p d r sourceData G) :
    Continuous (presentationModPFoxBoundary P)
theorem

continuous_presentationModPRelationMatrix

L182 ↗
ClassFieldTower.ProP.continuous_presentationModPRelationMatrix
Documentation

The finite displayed relation matrix is continuous.

Source context 12 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
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 continuous_presentationModPRelationMatrix
    (P : FiniteProPPresentation p d r sourceData G) :
    Continuous (presentationModPRelationMatrix P)
theorem

presentationModPRelationMatrix_range_eq_span

L190 ↗
ClassFieldTower.ProP.presentationModPRelationMatrix_range_eq_span
Documentation

The relation-matrix range is the coefficient span of the displayed rows.

Source context 12 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
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 presentationModPRelationMatrix_range_eq_span
    (P : FiniteProPPresentation p d r sourceData G) :
    LinearMap.range (presentationModPRelationMatrix P) =
      Submodule.span (ModPCompletedGroupAlgebra p G)
        (Set.range (displayedRelatorModPFoxRow P))
theorem

isCompact_range_presentationModPRelationMatrix

L198 ↗
ClassFieldTower.ProP.isCompact_range_presentationModPRelationMatrix
Documentation

The range of the finite displayed relation matrix is compact.

Source context 12 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
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 isCompact_range_presentationModPRelationMatrix
    (P : FiniteProPPresentation p d r sourceData G) :
    IsCompact (Set.range (presentationModPRelationMatrix P))
theorem

isClosed_range_presentationModPRelationMatrix

L208 ↗
ClassFieldTower.ProP.isClosed_range_presentationModPRelationMatrix
Documentation

The range of the finite displayed relation matrix is closed.

Source context 12 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
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 isClosed_range_presentationModPRelationMatrix
    (P : FiniteProPPresentation p d r sourceData G) :
    IsClosed (Set.range (presentationModPRelationMatrix P))

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