Module

CompletedOperatorCompatibility.lean

Nyll.ProCGroups.ProP.Fox.CompletedOperatorCompatibility

14 declarations indexed from sourceView source ↗

Module documentation

Fox--Leibniz compatibility for the completed mod-p operator

The universal all-finite lift of the mod-p presentation derivative inherits its crossed-product law from group-like elements. The comparison equivalence between all-finite and pro-p-indexed completed group algebras then transports this law to the completed operator used by the Zassenhaus filtration.

Imports5

Imported by2

def

allFiniteModPAugmentation

L42 ↗

ClassFieldTower.ProP.allFiniteModPAugmentation

Documentation

The continuous canonical augmentation of the all-finite completed group algebra over ZMod p.

Source context 10 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 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 allFiniteModPAugmentation (P : ProfiniteGrp.{u}) :
    CompletedGroupAlgebraCarrier (ZMod p) P →A[ZMod p] ZMod p where
  toAlgHom :=
    { toRingHom := completedGroupAlgebraCanonicalAugmentation (ZMod p) P
      commutes' := by
        intro a
        let U := terminalCompletedGroupAlgebraIndex P
        change completedGroupAlgebraStageAugmentation (ZMod p) P U
            (completedGroupAlgebraProjection (ZMod p) P U
              (algebraMap (ZMod p)
                (CompletedGroupAlgebraCarrier (ZMod p) P) a)) = a
        change groupAlgebraAugmentation (ZMod p)
            (CompletedGroupAlgebraQuotient P U)
            (algebraMap (ZMod p)
              (CompletedGroupAlgebraStage (ZMod p) P U) a) = a
        exact groupAlgebraAugmentation_algebraMap
          (ZMod p) (CompletedGroupAlgebraQuotient P U) a }
  cont := continuous_completedGroupAlgebraCanonicalAugmentation (ZMod p) P

theorem

allFiniteModPAugmentation_groupLike

L65 ↗

ClassFieldTower.ProP.allFiniteModPAugmentation_groupLike

Documentation

The all-finite mod-p augmentation sends every completed group-like element to one.

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 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 [Fact p.Prime] in

Lean source · statement

theorem allFiniteModPAugmentation_groupLike
    (P : ProfiniteGrp.{u}) (g : P) :
    allFiniteModPAugmentation (p := p) P
        (completedGroupAlgebraOf (ZMod p) P g) = 1

def

presentationAllFiniteModPCoefficient

L74 ↗

ClassFieldTower.ProP.presentationAllFiniteModPCoefficient

Documentation

The continuous algebra map from the all-finite source completion to the pro-p-indexed target completion induced by the presentation quotient.

Source context 10 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 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 presentationAllFiniteModPCoefficient
    (P : FiniteProPPresentation p d r sourceData G) :
    CompletedGroupAlgebraCarrier (ZMod p) sourceData.carrier.obj →A[ZMod p]
      ModPCompletedGroupAlgebra p G where
  toAlgHom :=
    (completedGroupAlgebraToInClassAlgHom
      (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p)).comp
      (completedGroupAlgebraMapAlgHom
        (G := sourceData.carrier) (H := G) (ZMod p)
        P.quotient.toMonoidHom P.quotient.continuous)
  cont :=
    (continuous_completedGroupAlgebraToInClass
      (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p)).comp
      (continuous_completedGroupAlgebraMap
        (G := sourceData.carrier) (H := G) (ZMod p)
        P.quotient.toMonoidHom P.quotient.continuous)

theorem

presentationAllFiniteModPCoefficient_groupLike

L94 ↗

ClassFieldTower.ProP.presentationAllFiniteModPCoefficient_groupLike

Documentation

The quotient-induced coefficient map has the expected value on completed group-like elements.

Source context 10 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 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 presentationAllFiniteModPCoefficient_groupLike
    (P : FiniteProPPresentation p d r sourceData G)
    (f : sourceData.carrier) :
    presentationAllFiniteModPCoefficient P
        (completedGroupAlgebraOf (ZMod p) sourceData.carrier.obj f) =
      completedGroupAlgebraOfInClass
        (FiniteGroupClass.pGroup p) (ZMod p) G (P.quotient f)

def

presentationAllFiniteModPCoordinateCoefficient

L112 ↗

ClassFieldTower.ProP.presentationAllFiniteModPCoordinateCoefficient

Documentation

The quotient coefficient acts diagonally on a completed Fox row.

Source context 10 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 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 presentationAllFiniteModPCoordinateCoefficient
    (P : FiniteProPPresentation p d r sourceData G) :
    CompletedGroupAlgebraCarrier (ZMod p) sourceData.carrier.obj →A[ZMod p]
      PresentationModPFoxCoordinates (p := p) (d := d) (G := G) where
  toAlgHom := AlgHom.pi fun _ ↦
    (presentationAllFiniteModPCoefficient P).toAlgHom
  cont := continuous_pi fun _ ↦
    (presentationAllFiniteModPCoefficient P).continuous

theorem

presentationAllFiniteModPCoordinateCoefficient_groupLike

L124 ↗

ClassFieldTower.ProP.presentationAllFiniteModPCoordinateCoefficient_groupLike

Documentation

On a completed group-like element, every diagonal coordinate is the group-like element of the presentation quotient.

Source context 10 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 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 presentationAllFiniteModPCoordinateCoefficient_groupLike
    (P : FiniteProPPresentation p d r sourceData G)
    (f : sourceData.carrier) :
    presentationAllFiniteModPCoordinateCoefficient P
        (completedGroupAlgebraOf (ZMod p) sourceData.carrier.obj f) =
      fun _ ↦ completedGroupAlgebraOfInClass
        (FiniteGroupClass.pGroup p) (ZMod p) G (P.quotient f) := by
  funext i
  exact presentationAllFiniteModPCoefficient_groupLike P f

def

presentationAllFiniteCompletedModPFoxOperator

L136 ↗

ClassFieldTower.ProP.presentationAllFiniteCompletedModPFoxOperator

Documentation

The all-finite continuous linear extension of the mod-p presentation Fox derivative.

Source context 10 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 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 presentationAllFiniteCompletedModPFoxOperator
    (P : FiniteProPPresentation p d r sourceData G) :
    CompletedGroupAlgebraCarrier (ZMod p) sourceData.carrier.obj →L[ZMod p]
      PresentationModPFoxCoordinates (p := p) (d := d) (G := G)

theorem

presentationAllFiniteCompletedModPFoxOperator_groupLike

L147 ↗

ClassFieldTower.ProP.presentationAllFiniteCompletedModPFoxOperator_groupLike

Documentation

The all-finite completed operator restricts to the original group derivative on completed group-like elements.

Source context 10 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 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 presentationAllFiniteCompletedModPFoxOperator_groupLike
    (P : FiniteProPPresentation p d r sourceData G)
    (f : sourceData.carrier) :
    presentationAllFiniteCompletedModPFoxOperator P
        (completedGroupAlgebraOf (ZMod p) sourceData.carrier.obj f) =
      presentationModPFoxDerivative P f

theorem

presentationAllFiniteCompletedModPFoxOperator_groupLike_crossed

L159 ↗

ClassFieldTower.ProP.presentationAllFiniteCompletedModPFoxOperator_groupLike_crossed

Documentation

The group-like values of the all-finite lift satisfy the crossed-product law with the diagonal quotient coefficient.

Source context 10 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 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 presentationAllFiniteCompletedModPFoxOperator_groupLike_crossed
    (P : FiniteProPPresentation p d r sourceData G)
    (f g : sourceData.carrier) :
    presentationAllFiniteCompletedModPFoxOperator P
        (completedGroupAlgebraOf (ZMod p) sourceData.carrier.obj (f * g)) =
      presentationAllFiniteCompletedModPFoxOperator P
          (completedGroupAlgebraOf (ZMod p) sourceData.carrier.obj f) +
        presentationAllFiniteModPCoordinateCoefficient P
            (completedGroupAlgebraOf (ZMod p) sourceData.carrier.obj f) *
          presentationAllFiniteCompletedModPFoxOperator P
            (completedGroupAlgebraOf (ZMod p) sourceData.carrier.obj g)

theorem

presentationAllFiniteCompletedModPFoxOperator_rightLeibniz

L180 ↗

ClassFieldTower.ProP.presentationAllFiniteCompletedModPFoxOperator_rightLeibniz

Documentation

The all-finite completed mod-p Fox operator satisfies the right Fox--Leibniz rule.

Source context 10 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 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 presentationAllFiniteCompletedModPFoxOperator_rightLeibniz
    (P : FiniteProPPresentation p d r sourceData G)
    (x y : CompletedGroupAlgebraCarrier (ZMod p) sourceData.carrier.obj) :
    presentationAllFiniteCompletedModPFoxOperator P (x * y) =
      algebraMap (ZMod p)
          (PresentationModPFoxCoordinates (p := p) (d := d) (G := G))
          (allFiniteModPAugmentation (p := p) sourceData.carrier.obj y) *
        presentationAllFiniteCompletedModPFoxOperator P x +
      presentationAllFiniteModPCoordinateCoefficient P x *
        presentationAllFiniteCompletedModPFoxOperator P y

theorem

presentationAllFiniteModPCoefficient_fromInClass

L235 ↗

ClassFieldTower.ProP.presentationAllFiniteModPCoefficient_fromInClass

Documentation

After comparison from the pro-p-indexed source completion, the all-finite quotient coefficient is the canonical in-class functorial map.

Source context 10 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 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 presentationAllFiniteModPCoefficient_fromInClass
    (P : FiniteProPPresentation p d r sourceData G)
    (x : ModPCompletedGroupAlgebra p sourceData.carrier) :
    presentationAllFiniteModPCoefficient P
        (completedGroupAlgebraFromInClass
          (R := ZMod p) (G := sourceData.carrier)
          (FiniteGroupClass.pGroup p)
          (pGroupFullFormation (p := p)).melnikovFormation.formation
          sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass x) =
      modPCompletedGroupAlgebraMap p P.quotient x

theorem

presentationAllFiniteModPCoordinateCoefficient_fromInClass

L277 ↗

ClassFieldTower.ProP.presentationAllFiniteModPCoordinateCoefficient_fromInClass

Documentation

The diagonal all-finite coefficient likewise becomes the in-class functorial map in every Fox coordinate.

Source context 10 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 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 presentationAllFiniteModPCoordinateCoefficient_fromInClass
    (P : FiniteProPPresentation p d r sourceData G)
    (x : ModPCompletedGroupAlgebra p sourceData.carrier) :
    presentationAllFiniteModPCoordinateCoefficient P
        (completedGroupAlgebraFromInClass
          (R := ZMod p) (G := sourceData.carrier)
          (FiniteGroupClass.pGroup p)
          (pGroupFullFormation (p := p)).melnikovFormation.formation
          sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass x) =
      fun _ ↦ modPCompletedGroupAlgebraMap p P.quotient x := by
  funext i
  exact presentationAllFiniteModPCoefficient_fromInClass P x

theorem

allFiniteModPAugmentation_fromInClass

L292 ↗

ClassFieldTower.ProP.allFiniteModPAugmentation_fromInClass

Documentation

The all-finite augmentation transported from the free pro-p source is the canonical pro-p-indexed augmentation.

Source context 10 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 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 allFiniteModPAugmentation_fromInClass
    (x : ModPCompletedGroupAlgebra p sourceData.carrier) :
    allFiniteModPAugmentation (p := p) sourceData.carrier.obj
        (completedGroupAlgebraFromInClass
          (R := ZMod p) (G := sourceData.carrier)
          (FiniteGroupClass.pGroup p)
          (pGroupFullFormation (p := p)).melnikovFormation.formation
          sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass x) =
      completedGroupAlgebraCanonicalAugmentationInClass
        (R := ZMod p) (G := sourceData.carrier)
        (FiniteGroupClass.pGroup p) x

theorem

presentationCompletedModPFoxOperator_rightLeibniz

L311 ↗

ClassFieldTower.ProP.presentationCompletedModPFoxOperator_rightLeibniz

Documentation

The completed presentation Fox operator on the pro-p-indexed source completion satisfies the right Fox--Leibniz rule.

Source context 10 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 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 presentationCompletedModPFoxOperator_rightLeibniz
    (P : FiniteProPPresentation p d r sourceData G)
    (x y : ModPCompletedGroupAlgebra p sourceData.carrier) :
    presentationCompletedModPFoxOperator P (x * y) =
      algebraMap (ZMod p)
          (PresentationModPFoxCoordinates (p := p) (d := d) (G := G))
          (completedGroupAlgebraCanonicalAugmentationInClass
            (R := ZMod p) (G := sourceData.carrier)
            (FiniteGroupClass.pGroup p) y) *
        presentationCompletedModPFoxOperator P x +
      (fun _ ↦ modPCompletedGroupAlgebraMap p P.quotient x) *
        presentationCompletedModPFoxOperator P y := by
  let C := FiniteGroupClass.pGroup p
  let hForm := (pGroupFullFormation (p := p)).melnikovFormation.formation
  let hF := sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass
  let Φ := completedGroupAlgebraFromInClassRingHom
    (R := ZMod p) (G := sourceData.carrier) C hForm hF
  have hall := presentationAllFiniteCompletedModPFoxOperator_rightLeibniz
    P (Φ x) (Φ y)
  have hepsilon :
      allFiniteModPAugmentation (p := p) sourceData.carrier.obj (Φ y) =
        completedGroupAlgebraCanonicalAugmentationInClass
          (R := ZMod p) (G := sourceData.carrier)
          (FiniteGroupClass.pGroup p) y := by
    dsimp [Φ, C, hForm, hF]
    exact allFiniteModPAugmentation_fromInClass y
  have hphi :
      presentationAllFiniteModPCoordinateCoefficient P (Φ x) =
        fun _ ↦ modPCompletedGroupAlgebraMap p P.quotient x := by
    dsimp [Φ, C, hForm, hF]
    exact presentationAllFiniteModPCoordinateCoefficient_fromInClass P x
  rw [hepsilon, hphi] at hall
  change presentationAllFiniteCompletedModPFoxOperator P (Φ (x * y)) = _
  rw [Φ.map_mul]
  exact hall

Module documentation

Fox--Leibniz compatibility for the completed mod-p operator

Declarations