NYLL
Module

ModPGroupDerivative.lean

Nyll.ProCGroups.ProP.Fox.ModPGroupDerivative
7 declarations indexed from sourceView source ↗

Module documentation

Mod-p Fox derivatives on finite pro-p presentation groups

Reducing every coordinate of the integral completed Fox derivative modulo p gives a continuous crossed homomorphism into the mod-p completed group algebra coordinates. Its coefficient is the completed group-like element of the presentation quotient.

Imports2
Imported by3

Declarations

abbrev

PresentationModPFoxCoordinates

L39 ↗
ClassFieldTower.ProP.PresentationModPFoxCoordinates
Documentation

Mod-p completed Fox-coordinate vectors for the chosen finite basis.

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
abbrev PresentationModPFoxCoordinates
def

presentationModPFoxCoefficient

L43 ↗
ClassFieldTower.ProP.presentationModPFoxCoefficient
Documentation

The mod-p group-like coefficient attached to the presentation quotient.

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
def presentationModPFoxCoefficient
    (P : FiniteProPPresentation p d r sourceData G) :
    sourceData.carrier →* ModPCompletedGroupAlgebra p G
theorem

presentationModPFoxCoefficient_apply

L53 ↗
ClassFieldTower.ProP.presentationModPFoxCoefficient_apply
Documentation

The mod-p coefficient is the completed group-like element of the presentation quotient.

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 presentationModPFoxCoefficient_apply
    (P : FiniteProPPresentation p d r sourceData G)
    (f : sourceData.carrier) :
    presentationModPFoxCoefficient P f =
      completedGroupAlgebraOfInClass
        (FiniteGroupClass.pGroup p) (ZMod p) G (P.quotient f)
def

presentationModPFoxDerivative

L68 ↗
ClassFieldTower.ProP.presentationModPFoxDerivative
Documentation

The presentation Fox derivative with every coordinate reduced modulo p, bundled with its crossed-product law.

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 presentationModPFoxDerivative
    (P : FiniteProPPresentation p d r sourceData G) :
    ScalarCrossedHom
      (presentationModPFoxCoefficient P)
      (PresentationModPFoxCoordinates (p := p) (d := d) (G := G)) where
  toFun f i :=
    modPCoefficientReduction p G (presentationFoxDerivative P f i)
  map_mul' f g := by
    funext i
    change modPCoefficientReduction p G
        (presentationFoxDerivative P (f * g) i) =
      modPCoefficientReduction p G (presentationFoxDerivative P f i) +
        presentationModPFoxCoefficient P f *
          modPCoefficientReduction p G (presentationFoxDerivative P g i)
    rw [ScalarCrossedHom.map_mul]
    simp only [Pi.add_apply, Pi.smul_apply, map_add, map_mul, smul_eq_mul]
    rfl
theorem

presentationModPFoxDerivative_apply

L89 ↗
ClassFieldTower.ProP.presentationModPFoxDerivative_apply
Documentation

Evaluation of a mod-p Fox coordinate is coefficient reduction of the corresponding integral coordinate.

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_apply
    (P : FiniteProPPresentation p d r sourceData G)
    (f : sourceData.carrier) (i : ULift.{u} (Fin d)) :
    presentationModPFoxDerivative P f i =
      modPCoefficientReduction p G (presentationFoxDerivative P f i)
theorem

continuous_presentationModPFoxDerivative

L97 ↗
ClassFieldTower.ProP.continuous_presentationModPFoxDerivative
Documentation

The coordinatewise mod-p presentation Fox derivative is continuous.

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 continuous_presentationModPFoxDerivative
    (P : FiniteProPPresentation p d r sourceData G) :
    Continuous (presentationModPFoxDerivative P)
theorem

presentationModPFoxDerivative_mul

L107 ↗
ClassFieldTower.ProP.presentationModPFoxDerivative_mul
Documentation

The crossed-product law written with the presentation quotient's mod-p group-like coefficient.

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_mul
    (P : FiniteProPPresentation p d r sourceData G)
    (f g : sourceData.carrier) :
    presentationModPFoxDerivative P (f * g) =
      presentationModPFoxDerivative P f +
        completedGroupAlgebraOfInClass
            (FiniteGroupClass.pGroup p) (ZMod p) G (P.quotient f) •
          presentationModPFoxDerivative P g

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