NYLL
Module

CompletedFiltration.lean

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

Module documentation

Filtration drop for the completed presentation Fox operator

Each coordinate of the completed mod-p Fox operator is a continuous linear map. Its right Fox--Leibniz rule lowers the closed augmentation filtration by one, so the Fox derivative of a group element of Zassenhaus depth at least n + 1 has every coordinate in target depth at least n.

Imports3
Imported by2

Declarations

def

presentationCompletedModPFoxCoordinate

L41 ↗
ClassFieldTower.ProP.presentationCompletedModPFoxCoordinate
Documentation

Evaluation of one coordinate of the completed presentation Fox operator, bundled as a continuous linear map.

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 presentationCompletedModPFoxCoordinate
    (P : FiniteProPPresentation p d r sourceData G)
    (i : ULift.{u} (Fin d)) :
    ModPCompletedGroupAlgebra p sourceData.carrier →L[ZMod p]
      ModPCompletedGroupAlgebra p G where
  toFun x := presentationCompletedModPFoxOperator P x i
  map_add' x y := by
    exact congrFun (map_add (presentationCompletedModPFoxOperator P) x y) i
  map_smul' c x := by
    exact congrFun (map_smul (presentationCompletedModPFoxOperator P) c x) i
  cont := (continuous_apply i).comp
    (presentationCompletedModPFoxOperator P).continuous
theorem

presentationCompletedModPFoxCoordinate_rightLeibniz

L56 ↗
ClassFieldTower.ProP.presentationCompletedModPFoxCoordinate_rightLeibniz
Documentation

A coordinate of the completed operator satisfies the right Fox--Leibniz rule.

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 presentationCompletedModPFoxCoordinate_rightLeibniz
    (P : FiniteProPPresentation p d r sourceData G)
    (i : ULift.{u} (Fin d))
    (x y : ModPCompletedGroupAlgebra p sourceData.carrier) :
    presentationCompletedModPFoxCoordinate P i (x * y) =
      algebraMap (ZMod p) (ModPCompletedGroupAlgebra p G)
          (completedGroupAlgebraCanonicalAugmentationInClass
            (R := ZMod p) (G := sourceData.carrier)
            (FiniteGroupClass.pGroup p) y) *
        presentationCompletedModPFoxCoordinate P i x +
      modPCompletedGroupAlgebraMap p P.quotient x *
        presentationCompletedModPFoxCoordinate P i y
theorem

presentationModPCompletedGroupAlgebraMap_mem_augmentationIdeal

L82 ↗
ClassFieldTower.ProP.presentationModPCompletedGroupAlgebraMap_mem_augmentationIdeal
Documentation

The presentation-induced completed group-algebra map sends the source augmentation kernel into the target augmentation ideal.

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 presentationModPCompletedGroupAlgebraMap_mem_augmentationIdeal
    (P : FiniteProPPresentation p d r sourceData G)
    {x : ModPCompletedGroupAlgebra p sourceData.carrier}
    (hx : x ∈ RingHom.ker
      (completedGroupAlgebraCanonicalAugmentationInClass
        (R := ZMod p) (G := sourceData.carrier)
        (FiniteGroupClass.pGroup p))) :
    modPCompletedGroupAlgebraMap p P.quotient x ∈
      modPAugmentationIdeal p G
theorem

presentationCompletedModPFoxCoordinate_mem_closedAugmentationPower

L100 ↗
ClassFieldTower.ProP.presentationCompletedModPFoxCoordinate_mem_closedAugmentationPower
Documentation

Each coordinate of the completed Fox operator lowers closed augmentation powers by one.

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 presentationCompletedModPFoxCoordinate_mem_closedAugmentationPower
    (P : FiniteProPPresentation p d r sourceData G)
    (i : ULift.{u} (Fin d)) (n : ℕ)
    {x : ModPCompletedGroupAlgebra p sourceData.carrier}
    (hx : x ∈ closedAugmentationPower p sourceData.carrier (n + 1)) :
    presentationCompletedModPFoxCoordinate P i x ∈
      closedAugmentationPower p G n
theorem

presentationCompletedModPFoxOperator_one

L124 ↗
ClassFieldTower.ProP.presentationCompletedModPFoxOperator_one
Documentation

The completed presentation Fox operator vanishes at the unit.

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 presentationCompletedModPFoxOperator_one
    (P : FiniteProPPresentation p d r sourceData G) :
    presentationCompletedModPFoxOperator P 1 = 0
theorem

presentationCompletedModPFoxOperator_groupLikeDifference

L136 ↗
ClassFieldTower.ProP.presentationCompletedModPFoxOperator_groupLikeDifference
Documentation

On a group-like difference, the completed operator is the original group-level mod-p Fox 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 presentationCompletedModPFoxOperator_groupLikeDifference
    (P : FiniteProPPresentation p d r sourceData G)
    (f : sourceData.carrier) :
    presentationCompletedModPFoxOperator P
        (groupLikeDifference p sourceData.carrier f) =
      presentationModPFoxDerivative P f
theorem

presentationCompletedModPFoxCoordinate_groupLikeDifference

L152 ↗
ClassFieldTower.ProP.presentationCompletedModPFoxCoordinate_groupLikeDifference
Documentation

On a group-like difference, a completed coordinate is the corresponding group-level mod-p Fox derivative 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 presentationCompletedModPFoxCoordinate_groupLikeDifference
    (P : FiniteProPPresentation p d r sourceData G)
    (f : sourceData.carrier) (i : ULift.{u} (Fin d)) :
    presentationCompletedModPFoxCoordinate P i
        (groupLikeDifference p sourceData.carrier f) =
      presentationModPFoxDerivative P f i
theorem

presentationModPFoxDerivative_mem_closedAugmentationPower

L165 ↗
ClassFieldTower.ProP.presentationModPFoxDerivative_mem_closedAugmentationPower
Documentation

A group element of Zassenhaus depth at least n + 1 has every mod-p Fox derivative coordinate in the target closed augmentation power n.

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_closedAugmentationPower
    (P : FiniteProPPresentation p d r sourceData G)
    (n : ℕ) (f : sourceData.carrier) (i : ULift.{u} (Fin d))
    (hf : ZassenhausDepthAtLeast p (n + 1) f) :
    presentationModPFoxDerivative P f i ∈
      closedAugmentationPower p G n
theorem

displayedRelatorModPFoxDerivative_mem_closedAugmentationPower

L177 ↗
ClassFieldTower.ProP.displayedRelatorModPFoxDerivative_mem_closedAugmentationPower
Documentation

Every coordinate of a displayed relator of depth at least n + 1 lies in the target closed augmentation power n.

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 displayedRelatorModPFoxDerivative_mem_closedAugmentationPower
    (P : FiniteProPPresentation p d r sourceData G)
    (n : ℕ) (j : Fin r) (i : ULift.{u} (Fin d))
    (hj : P.RelatorZassenhausDepthAtLeast (n + 1) j) :
    presentationModPFoxDerivative P (P.relator j) i ∈
      closedAugmentationPower p G n

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