NYLL
Module

CompletedOperator.lean

Nyll.ProCGroups.ProP.Fox.CompletedOperator
8 declarations indexed from sourceView source ↗

Module documentation

Completed mod-p Fox operators

The continuous mod-p Fox derivative on a free pro-p group extends uniquely to its completed group algebra. The resulting continuous linear map is then transported from the all-finite completion to the p-group-indexed model used by the Zassenhaus filtration.

Imports3
Imported by2

Declarations

def

modPProfiniteCommRing

L33 ↗
ClassFieldTower.ProP.modPProfiniteCommRing
Documentation

ZMod p, with its finite discrete topology, as a bundled profinite commutative coefficient ring.

Source context 6 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
Lean source · full declaration
def modPProfiniteCommRing (p : ℕ) [Fact p.Prime] : ProfiniteCommRing where
  toProfinite := Profinite.of (ZMod p)
  commRing := inferInstance
  isTopologicalRing := inferInstance
def

modPFoxCoordinatesProfiniteModule

L40 ↗
ClassFieldTower.ProP.modPFoxCoordinatesProfiniteModule
Documentation

A finite row of mod-p completed group algebras as a profinite module over ZMod p.

Source context 6 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
Lean source · statement
def modPFoxCoordinatesProfiniteModule
    (p d : ℕ) [Fact p.Prime]
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    ProfiniteModule.{0, u} (modPProfiniteCommRing p).toProfiniteRing
def

completedModPFoxLift

L75 ↗
ClassFieldTower.ProP.completedModPFoxLift
Documentation

The unique continuous ZMod p-linear extension of a continuous map from a profinite group to a finite row of mod-p completed group algebras.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F G : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [TotallyDisconnectedSpace F]
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def completedModPFoxLift
    (d : ℕ)
    (f : F → (ULift.{u} (Fin d) → ModPCompletedGroupAlgebra p G))
    (hf : Continuous f) :
    CompletedGroupAlgebraCarrier (ZMod p) F →L[ZMod p]
      (ULift.{u} (Fin d) → ModPCompletedGroupAlgebra p G)
theorem

completedModPFoxLift_apply_of

L94 ↗
ClassFieldTower.ProP.completedModPFoxLift_apply_of
Documentation

The all-finite completed lift agrees with its input on group-like elements.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F G : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [TotallyDisconnectedSpace F]
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem completedModPFoxLift_apply_of
    (d : ℕ)
    (f : F → (ULift.{u} (Fin d) → ModPCompletedGroupAlgebra p G))
    (hf : Continuous f) (g : F) :
    completedModPFoxLift (G := G) d f hf
        (completedGroupAlgebraOf (ZMod p) F g) =
      f g
def

completedModPFoxInClassLift

L113 ↗
ClassFieldTower.ProP.completedModPFoxInClassLift
Documentation

Precompose the all-finite completed lift with the comparison map from the p-group-indexed completed group algebra.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F G : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [TotallyDisconnectedSpace F]
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def completedModPFoxInClassLift
    (d : ℕ)
    (hF : ProC.HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) F)
    (f : F → (ULift.{u} (Fin d) → ModPCompletedGroupAlgebra p G))
    (hf : Continuous f) :
    ModPCompletedGroupAlgebra p F →L[ZMod p]
      (ULift.{u} (Fin d) → ModPCompletedGroupAlgebra p G)
theorem

completedModPFoxInClassLift_apply_of

L166 ↗
ClassFieldTower.ProP.completedModPFoxInClassLift_apply_of
Documentation

The class-indexed completed lift agrees with its input on group-like elements.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F G : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [TotallyDisconnectedSpace F]
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem completedModPFoxInClassLift_apply_of
    (d : ℕ)
    (hF : ProC.HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) F)
    (f : F → (ULift.{u} (Fin d) → ModPCompletedGroupAlgebra p G))
    (hf : Continuous f) (g : F) :
    completedModPFoxInClassLift (G := G) d hF f hf
        (completedGroupAlgebraOfInClass
          (FiniteGroupClass.pGroup p) (ZMod p) F g) =
      f g
def

presentationCompletedModPFoxOperator

L192 ↗
ClassFieldTower.ProP.presentationCompletedModPFoxOperator
Documentation

The continuous completed mod-p Fox operator attached to a finite pro-p presentation.

Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F G : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [TotallyDisconnectedSpace F]
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def presentationCompletedModPFoxOperator
    (P : FiniteProPPresentation p d r sourceData G) :
    ModPCompletedGroupAlgebra p sourceData.carrier →L[ZMod p]
      PresentationModPFoxCoordinates (p := p) (d := d) (G := G)
theorem

presentationCompletedModPFoxOperator_apply_groupLike

L204 ↗
ClassFieldTower.ProP.presentationCompletedModPFoxOperator_apply_groupLike
Documentation

On completed group-like elements, the completed operator is the original mod-p presentation Fox derivative.

Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F G : Type u}
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [TotallyDisconnectedSpace F]
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem presentationCompletedModPFoxOperator_apply_groupLike
    (P : FiniteProPPresentation p d r sourceData G)
    (f : sourceData.carrier) :
    presentationCompletedModPFoxOperator
        (p := p) (d := d) (r := r) (sourceData := sourceData) (G := G) P
        (completedGroupAlgebraOfInClass
          (FiniteGroupClass.pGroup p) (ZMod p) sourceData.carrier f) =
      presentationModPFoxDerivative P f

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