NYLL
Module

ModPDisplayedSpan.lean

Nyll.ProCGroups.ProP.Fox.ModPDisplayedSpan
9 declarations indexed from sourceView source ↗

Module documentation

Mod-p images of the displayed Fox-row span

Coordinatewise coefficient reduction sends the integral completed Fox rows to their mod-p counterparts. The integral closed-span theorem and the closed range of the finite mod-p relation matrix then show that every kernel Fox row belongs to that matrix range.

Imports3
Imported by3

Declarations

def

presentationFoxCoordinatesModPReduction

L41 ↗
ClassFieldTower.ProP.presentationFoxCoordinatesModPReduction
Documentation

Coordinatewise continuous reduction from integral completed Fox coordinates to mod-p completed Fox coordinates.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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
def presentationFoxCoordinatesModPReduction :
    ContinuousAddMonoidHom
      (PresentationFoxCoordinates (p := p) (d := d) (G := G))
      (PresentationModPFoxCoordinates (p := p) (d := d) (G := G)) where
  toFun v i := modPCoefficientReduction p G (v i)
  map_zero' := by
    funext i
    exact map_zero (modPCoefficientReduction p G)
  map_add' v w := by
    funext i
    exact map_add (modPCoefficientReduction p G) (v i) (w i)
  continuous_toFun := by
    apply continuous_pi
    intro i
    exact (continuous_modPCoefficientReduction p G).comp (continuous_apply i)
theorem

presentationFoxCoordinatesModPReduction_apply

L60 ↗
ClassFieldTower.ProP.presentationFoxCoordinatesModPReduction_apply
Documentation

Coordinatewise evaluation of mod-p reduction.

Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem presentationFoxCoordinatesModPReduction_apply
    (v : PresentationFoxCoordinates (p := p) (d := d) (G := G))
    (i : ULift.{u} (Fin d)) :
    presentationFoxCoordinatesModPReduction (p := p) (G := G) v i =
      modPCoefficientReduction p G (v i)
theorem

presentationFoxCoordinatesModPReduction_smul

L69 ↗
ClassFieldTower.ProP.presentationFoxCoordinatesModPReduction_smul
Documentation

Coordinatewise reduction is semilinear for coefficient reduction.

Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem presentationFoxCoordinatesModPReduction_smul
    (a : PresentationFoxCoefficientRing (p := p) (G := G))
    (v : PresentationFoxCoordinates (p := p) (d := d) (G := G)) :
    presentationFoxCoordinatesModPReduction (p := p) (G := G) (a • v) =
      modPCoefficientReduction p G a •
        presentationFoxCoordinatesModPReduction (p := p) (G := G) v
theorem

presentationFoxCoordinatesModPReduction_derivative

L82 ↗
ClassFieldTower.ProP.presentationFoxCoordinatesModPReduction_derivative
Documentation

Reduction of the integral presentation derivative is the mod-p presentation derivative.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 presentationFoxCoordinatesModPReduction_derivative
    (P : FiniteProPPresentation p d r sourceData G)
    (f : sourceData.carrier) :
    presentationFoxCoordinatesModPReduction (p := p) (G := G)
        (presentationFoxDerivative P f) =
      presentationModPFoxDerivative P f
theorem

presentationFoxCoordinatesModPReduction_displayedRelatorFoxRow

L94 ↗
ClassFieldTower.ProP.presentationFoxCoordinatesModPReduction_displayedRelatorFoxRow
Documentation

Reduction sends every integral displayed row to its mod-p displayed row.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 presentationFoxCoordinatesModPReduction_displayedRelatorFoxRow
    (P : FiniteProPPresentation p d r sourceData G)
    (i : Fin r) :
    presentationFoxCoordinatesModPReduction (p := p) (G := G)
        (displayedRelatorFoxRow P i) =
      displayedRelatorModPFoxRow P i
theorem

presentationFoxCoordinatesModPReduction_kernelFoxRow

L105 ↗
ClassFieldTower.ProP.presentationFoxCoordinatesModPReduction_kernelFoxRow
Documentation

Reduction of an integral kernel row is the mod-p derivative of its underlying kernel element.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 presentationFoxCoordinatesModPReduction_kernelFoxRow
    (P : FiniteProPPresentation p d r sourceData G)
    (n : P.quotient.toMonoidHom.ker) :
    presentationFoxCoordinatesModPReduction (p := p) (G := G)
        (kernelFoxRow P n) =
      presentationModPFoxDerivative P n.1
theorem

displayedRelatorModPFoxRow_mem_relationMatrix_range

L114 ↗
ClassFieldTower.ProP.displayedRelatorModPFoxRow_mem_relationMatrix_range
Documentation

Each displayed mod-p row belongs to the finite relation-matrix range.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 displayedRelatorModPFoxRow_mem_relationMatrix_range
    (P : FiniteProPPresentation p d r sourceData G)
    (i : Fin r) :
    displayedRelatorModPFoxRow P i ∈
      LinearMap.range (presentationModPRelationMatrix P)
theorem

presentationFoxCoordinatesModPReduction_mem_relationMatrix_range_of_mem_span

L124 ↗
ClassFieldTower.ProP.presentationFoxCoordinatesModPReduction_mem_relationMatrix_range_of_mem_span
Documentation

Coordinatewise reduction sends the algebraic integral displayed-row span into the mod-p relation-matrix range.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 presentationFoxCoordinatesModPReduction_mem_relationMatrix_range_of_mem_span
    (P : FiniteProPPresentation p d r sourceData G)
    (v : PresentationFoxCoordinates (p := p) (d := d) (G := G))
    (hv : v ∈ Submodule.span
      (PresentationFoxCoefficientRing (p := p) (G := G))
      (Set.range (displayedRelatorFoxRow P))) :
    presentationFoxCoordinatesModPReduction (p := p) (G := G) v ∈
      LinearMap.range (presentationModPRelationMatrix P)
theorem

presentationModPFoxDerivative_mem_relationMatrix_range

L151 ↗
ClassFieldTower.ProP.presentationModPFoxDerivative_mem_relationMatrix_range
Documentation

Every presentation-kernel Fox row modulo p belongs to the range of the finite displayed relation matrix.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 presentationModPFoxDerivative_mem_relationMatrix_range
    (P : FiniteProPPresentation p d r sourceData G)
    (n : P.quotient.toMonoidHom.ker) :
    presentationModPFoxDerivative P n.1 ∈
      LinearMap.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.