NYLL
Module

ModPStageProjection.lean

Nyll.ProCGroups.ProP.Fox.ModPStageProjection
21 declarations indexed from sourceView source ↗

Module documentation

Mod-p completed-to-finite Fox stage projection

A finite p-group quotient of the presented group gives a canonical projection from the mod-p completed group algebra to the reflected finite Fox target. This module constructs the coefficient and coordinate projections, proves compatibility with the completed and finite Fox boundaries, and identifies projected presentation derivatives with the reflected finite-stage derivative on abstract free words.

Imports2
Imported by2

Declarations

def

presentationModPFiniteStageProjection

L42 ↗
ClassFieldTower.ProP.presentationModPFiniteStageProjection
Documentation

The selected quotient coordinate of the mod-p completed group algebra.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageProjection
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    ModPCompletedGroupAlgebra p G →+*
      CompletedGroupAlgebraStageInClass
        (FiniteGroupClass.pGroup p) (ZMod p) G (OrderDual.toDual ⟨U, hU⟩)
def

presentationModPFiniteStageQMapAtIndex

L52 ↗
ClassFieldTower.ProP.presentationModPFiniteStageQMapAtIndex
Documentation

The reflected comparison, typed at the selected completed-algebra quotient index.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageQMapAtIndex
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    FoxDifferential.CompletedGroupAlgebraQuotientInClass G (FiniteGroupClass.pGroup p)
        (OrderDual.toDual ⟨U, hU⟩) →*
      presentationModPFiniteStageTarget P U hU
def

presentationModPFiniteStageQMapAlgebra

L62 ↗
ClassFieldTower.ProP.presentationModPFiniteStageQMapAlgebra
Documentation

Change the quotient support from G/U to the reflected finite Fox target.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageQMapAlgebra
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    CompletedGroupAlgebraStageInClass
        (FiniteGroupClass.pGroup p) (ZMod p) G (OrderDual.toDual ⟨U, hU⟩) →+*
      foxAlgebraicStageTargetGroupAlgebra
        (presentationModPFiniteStageKernel P U hU) p
def

presentationModPFiniteStageCoefficientMap

L74 ↗
ClassFieldTower.ProP.presentationModPFiniteStageCoefficientMap
Documentation

The actual coefficient projection from the completed algebra to the reflected stage.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageCoefficientMap
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    ModPCompletedGroupAlgebra p G →+*
      foxAlgebraicStageTargetGroupAlgebra
        (presentationModPFiniteStageKernel P U hU) p
def

presentationModPFiniteStageCoordinateMap

L85 ↗
ClassFieldTower.ProP.presentationModPFiniteStageCoordinateMap
Documentation

Apply the coefficient projection in every Fox coordinate.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageCoordinateMap
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    PresentationModPFoxCoordinates (p := p) (d := d) (G := G) →+
      foxAlgebraicStageCoordinateVector
        (presentationModPFiniteStageKernel P U hU) p where
  toFun v i := presentationModPFiniteStageCoefficientMap P U hU (v i)
  map_zero' := by
    funext i
    exact map_zero _
  map_add' v w := by
    funext i
    exact map_add _ _ _
theorem

presentationModPFiniteStageCoordinateMap_apply

L101 ↗
ClassFieldTower.ProP.presentationModPFiniteStageCoordinateMap_apply
Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageCoordinateMap_apply
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G))
    (i : ULift.{u} (Fin d)) :
    presentationModPFiniteStageCoordinateMap P U hU v i =
      presentationModPFiniteStageCoefficientMap P U hU (v i)
theorem

presentationModPFiniteStageProjection_of

L113 ↗
ClassFieldTower.ProP.presentationModPFiniteStageProjection_of
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageProjection_of
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (g : G) :
    presentationModPFiniteStageProjection U hU
        (completedGroupAlgebraOfInClass
          (FiniteGroupClass.pGroup p) (ZMod p) G g) =
      MonoidAlgebra.of (ZMod p)
        (FoxDifferential.CompletedGroupAlgebraQuotientInClass G (FiniteGroupClass.pGroup p)
          (OrderDual.toDual ⟨U, hU⟩))
        (QuotientGroup.mk g)
theorem

presentationModPFiniteStageCoefficientMap_groupLike

L127 ↗
ClassFieldTower.ProP.presentationModPFiniteStageCoefficientMap_groupLike
Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageCoefficientMap_groupLike
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (g : G) :
    presentationModPFiniteStageCoefficientMap P U hU
        (completedGroupAlgebraOfInClass
          (FiniteGroupClass.pGroup p) (ZMod p) G g) =
      MonoidAlgebra.of (ZMod p)
        (presentationModPFiniteStageTarget P U hU)
        (presentationModPFiniteStageQMapAtIndex P U hU
          (QuotientGroup.mk g))
theorem

presentationModPFiniteStageQMapAtIndex_generator

L151 ↗
ClassFieldTower.ProP.presentationModPFiniteStageQMapAtIndex_generator
Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageQMapAtIndex_generator
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (i : ULift.{u} (Fin d)) :
    presentationModPFiniteStageQMapAtIndex P U hU
        (QuotientGroup.mk (P.quotient (presentationChosenGenerator P i))) =
      QuotientGroup.mk'
        (presentationModPFiniteStageKernel P U hU) (FreeGroup.of i)
theorem

presentationModPFiniteStageCoefficientMap_chosenGenerator

L162 ↗
ClassFieldTower.ProP.presentationModPFiniteStageCoefficientMap_chosenGenerator
Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageCoefficientMap_chosenGenerator
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (i : ULift.{u} (Fin d)) :
    presentationModPFiniteStageCoefficientMap P U hU
        (groupLikeDifference p G
          (P.quotient (presentationChosenGenerator P i))) =
      MonoidAlgebra.of (ZMod p)
          (presentationModPFiniteStageTarget P U hU)
          (QuotientGroup.mk'
            (presentationModPFiniteStageKernel P U hU) (FreeGroup.of i)) - 1
theorem

presentationModPFiniteStageFoxBoundary_coordinateMap

L179 ↗
ClassFieldTower.ProP.presentationModPFiniteStageFoxBoundary_coordinateMap
Documentation

The completed mod-p presentation boundary commutes with the reflected stage projection.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageFoxBoundary_coordinateMap
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (v : PresentationModPFoxCoordinates (p := p) (d := d) (G := G)) :
    foxAlgebraicStageFoxBoundary
        (presentationModPFiniteStageKernel P U hU) p
        (presentationModPFiniteStageCoordinateMap P U hU v) =
      presentationModPFiniteStageCoefficientMap P U hU
        (presentationModPFoxBoundary P v)
def

presentationZCFiniteStageCoefficientMap

L197 ↗
ClassFieldTower.ProP.presentationZCFiniteStageCoefficientMap
Documentation

The integral completed coefficient map attached to the same reflected stage.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationZCFiniteStageCoefficientMap
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G →+*
      foxAlgebraicStageTargetGroupAlgebra
        (presentationModPFiniteStageKernel P U hU) p
def

presentationModPFiniteStageRightMap

L210 ↗
ClassFieldTower.ProP.presentationModPFiniteStageRightMap
Documentation

The selected quotient followed by the reflected target comparison.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageRightMap
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G))) :
    G →* presentationModPFiniteStageTarget P U hU
theorem

presentationZCFiniteStageCoefficientMap_groupLike

L221 ↗
ClassFieldTower.ProP.presentationZCFiniteStageCoefficientMap_groupLike
Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationZCFiniteStageCoefficientMap_groupLike
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (g : G) :
    presentationZCFiniteStageCoefficientMap P U hU
        (zcGroupLike (FiniteGroupClass.pGroup p) G g) =
      MonoidAlgebra.of (ZMod p)
        (presentationModPFiniteStageTarget P U hU)
        (presentationModPFiniteStageRightMap P U hU g)
theorem

presentationModPFiniteStageProjection_reduction

L239 ↗
ClassFieldTower.ProP.presentationModPFiniteStageProjection_reduction
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageProjection_reduction
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (x : ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G) :
    presentationModPFiniteStageProjection U hU
        (modPCoefficientReduction p G x) =
      zcCompletedGroupAlgebraProjection
        (FiniteGroupClass.pGroup p) G
        (modPCoefficientIndex p, OrderDual.toDual ⟨U, hU⟩) x
theorem

presentationModPFiniteStageCoefficientMap_reduction

L253 ↗
ClassFieldTower.ProP.presentationModPFiniteStageCoefficientMap_reduction
Documentation

Reducing coefficients modulo p and then taking the selected stage is the same coefficient map as the integral completed stage with modulus p.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageCoefficientMap_reduction
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (x : ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G) :
    presentationModPFiniteStageCoefficientMap P U hU
        (modPCoefficientReduction p G x) =
      presentationZCFiniteStageCoefficientMap P U hU x
theorem

presentationModPFiniteStageRightMap_generator

L312 ↗
ClassFieldTower.ProP.presentationModPFiniteStageRightMap_generator
Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageRightMap_generator
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (i : ULift.{u} (Fin d)) :
    presentationModPFiniteStageRightMap P U hU
        (P.quotient (presentationChosenGenerator P i)) =
      QuotientGroup.mk'
        (presentationModPFiniteStageKernel P U hU) (FreeGroup.of i)
theorem

presentationZCFiniteStageDerivative_word

L324 ↗
ClassFieldTower.ProP.presentationZCFiniteStageDerivative_word
Documentation

Exact instantiation of the generic completed-to-finite derivative compatibility theorem.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationZCFiniteStageDerivative_word
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (w : FreeGroup (ULift.{u} (Fin d))) :
    zcFreeFoxCoordinatesStageMap
        (presentationModPFiniteStageKernel P U hU) p
        (presentationZCFiniteStageCoefficientMap P U hU)
        (zcFreeGroupFoxDerivativeVector (FiniteGroupClass.pGroup p)
          (FreeGroup.lift (fun i ↦
            P.quotient (presentationChosenGenerator P i))) w) =
      foxAlgebraicStageDerivativeVector
        (presentationModPFiniteStageKernel P U hU) p w := by
  exact zcFreeFoxCoordinatesStageMap_derivativeVector_of_generators
    (presentationModPFiniteStageKernel P U hU) p
    (fun i ↦ P.quotient (presentationChosenGenerator P i))
    (presentationZCFiniteStageCoefficientMap P U hU)
    (presentationModPFiniteStageRightMap P U hU)
    (presentationZCFiniteStageCoefficientMap_groupLike P U hU)
    (presentationModPFiniteStageRightMap_generator P U hU) w
theorem

presentationFoxDerivative_word

L347 ↗
ClassFieldTower.ProP.presentationFoxDerivative_word
Documentation

Restricting the completed presentation derivative to abstract words recovers the completed free-group derivative.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationFoxDerivative_word
    (P : FiniteProPPresentation p d r sourceData G)
    (w : FreeGroup (ULift.{u} (Fin d))) :
    presentationFoxDerivative P
        (FreeGroup.lift (presentationChosenGenerator P) w) =
      zcFreeGroupFoxDerivativeVector (FiniteGroupClass.pGroup p)
        (FreeGroup.lift (fun i ↦
          P.quotient (presentationChosenGenerator P i))) w := by
  let ι : ULift.{u} (Fin d) → sourceData.carrier :=
    presentationChosenGenerator P
  let ρ : sourceData.carrier →* G := P.quotient.toMonoidHom
  let D := presentationFoxDerivative P
  let δ : ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar
        (FiniteGroupClass.pGroup p) (ρ.comp (FreeGroup.lift ι)))
      (PresentationFoxCoordinates (p := p) (d := d) (G := G)) :=
    { toFun := fun w ↦ D (FreeGroup.lift ι w)
      map_mul' := by
        intro a b
        simp [ρ, D] }
  have hbasis : ∀ i : ULift.{u} (Fin d),
      δ (FreeGroup.of i) =
        Pi.single i (1 : PresentationFoxCoefficientRing (p := p) (G := G)) := by
    intro i
    change D (FreeGroup.lift ι (FreeGroup.of i)) = _
    rw [FreeGroup.lift_apply_of]
    exact presentationFoxDerivative_chosenGenerator P i
  have hδ : δ =
      zcFreeGroupFoxDerivativeVector
        (FiniteGroupClass.pGroup p) (ρ.comp (FreeGroup.lift ι)) :=
    zcFreeGroupFoxDerivativeVector_unique
      (FiniteGroupClass.pGroup p) (ρ.comp (FreeGroup.lift ι)) δ hbasis
  have hρlift : ρ.comp (FreeGroup.lift ι) =
      FreeGroup.lift (fun i ↦ P.quotient (presentationChosenGenerator P i)) := by
    ext i
    simp [ρ, ι]
  have hw := congrArg
    (fun E : ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar
        (FiniteGroupClass.pGroup p) (ρ.comp (FreeGroup.lift ι)))
      (PresentationFoxCoordinates (p := p) (d := d) (G := G)) ↦ E w) hδ
  change D (FreeGroup.lift ι w) =
    zcFreeGroupFoxDerivativeVector
      (FiniteGroupClass.pGroup p) (ρ.comp (FreeGroup.lift ι)) w at hw
  rw [← hρlift]
  simpa [D, ι] using hw
theorem

presentationZCFiniteStageDerivative_presentationWord

L395 ↗
ClassFieldTower.ProP.presentationZCFiniteStageDerivative_presentationWord
Documentation

The integral presentation derivative projects to the reflected finite derivative on words.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationZCFiniteStageDerivative_presentationWord
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (w : FreeGroup (ULift.{u} (Fin d))) :
    zcFreeFoxCoordinatesStageMap
        (presentationModPFiniteStageKernel P U hU) p
        (presentationZCFiniteStageCoefficientMap P U hU)
        (presentationFoxDerivative P
          (FreeGroup.lift (presentationChosenGenerator P) w)) =
      foxAlgebraicStageDerivativeVector
        (presentationModPFiniteStageKernel P U hU) p w
theorem

presentationModPFiniteStageDerivative_presentationWord

L412 ↗
ClassFieldTower.ProP.presentationModPFiniteStageDerivative_presentationWord
Documentation

The mod-p presentation derivative projects coordinatewise to the reflected finite-stage derivative on abstract words.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open CrowellExactSequence
open FoxDifferential
open ProCGroups
open ProCGroups.ProC
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 presentationModPFiniteStageDerivative_presentationWord
    (P : FiniteProPPresentation p d r sourceData G)
    (U : OpenNormalSubgroup G)
    (hU : FiniteGroupClass.pGroup p (G ⧸ (U : Subgroup G)))
    (w : FreeGroup (ULift.{u} (Fin d))) :
    presentationModPFiniteStageCoordinateMap P U hU
        (presentationModPFoxDerivative P
          (FreeGroup.lift (presentationChosenGenerator P) w)) =
      foxAlgebraicStageDerivativeVector
        (presentationModPFiniteStageKernel P U hU) p w

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