NYLL
Module

CoefficientReduction.lean

Nyll.ProCGroups.ProP.Fox.CoefficientReduction
10 declarations indexed from sourceView source ↗

Module documentation

Continuous reduction of completed pro-p group algebras modulo p

The pro-p integral completed group algebra has both a coefficient index and a finite group-quotient index. Fixing the coefficient index at p ^ 1 leaves a compatible family over the group quotients. Its inverse-limit lift is the canonical continuous reduction map to the completed group algebra over ZMod p.

Imports3
Imported by2

Declarations

def

modPCoefficientIndex

L40 ↗
ClassFieldTower.ProP.modPCoefficientIndex
Documentation

The coefficient coordinate supplied by pGroupPower p 1, with modulus definitionally normalized to p.

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
open ProCGroups.Completion
open ProCGroups.InverseSystems
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def modPCoefficientIndex :
    ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}) where
  modulus := p
  positive := (Fact.out : Nat.Prime p).pos
  cyclic_mem := by
    have h := (ProCIntegerIndex.pGroupPower p 1).cyclic_mem
    change (FiniteGroupClass.pGroup p).MemAcrossUniverses
      (Multiplicative (ZMod (p ^ 1))) at h
    have hp : p ^ 1 = p := Nat.pow_one p
    rw [hp] at h
    exact h
theorem

modPCoefficientIndex_modulus

L53 ↗
ClassFieldTower.ProP.modPCoefficientIndex_modulus
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
open ProCGroups.Completion
open ProCGroups.InverseSystems
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem modPCoefficientIndex_modulus :
    (modPCoefficientIndex p :
      ProCIntegerIndex
        (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})).modulus = p
def

modPCoefficientReductionStageRingHom

L61 ↗
ClassFieldTower.ProP.modPCoefficientReductionStageRingHom
Documentation

Reduction to the fixed p ^ 1 coefficient coordinate at one finite group quotient stage.

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
open ProCGroups.Completion
open ProCGroups.InverseSystems
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def modPCoefficientReductionStageRingHom
    (U : CompletedGroupAlgebra.CompletedGroupAlgebraIndexInClass G
      (FiniteGroupClass.pGroup p)) :
    ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G →+*
      CompletedGroupAlgebraStageInClass
        (FiniteGroupClass.pGroup p) (ZMod p) G U
theorem

modPCoefficientReductionStage_compatible

L72 ↗
ClassFieldTower.ProP.modPCoefficientReductionStage_compatible
Documentation

The fixed-coefficient stage maps commute with refinement of finite p-group quotients.

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
open ProCGroups.Completion
open ProCGroups.InverseSystems
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
theorem modPCoefficientReductionStage_compatible :
    (completedGroupAlgebraSystemInClass
      (FiniteGroupClass.pGroup p) (ZMod p) G).CompatibleMaps
      (fun U => modPCoefficientReductionStageRingHom p G U) := by
  intro U V hUV
  funext x
  have hx := x.2
    (modPCoefficientIndex p, U)
    (modPCoefficientIndex p, V)
    ⟨le_rfl, hUV⟩
  have hsame := zcCompletedGroupAlgebraTransition_sameCoeff
    (FiniteGroupClass.pGroup p) G (modPCoefficientIndex p)
    (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV
  have hsx := congrFun (congrArg DFunLike.coe hsame)
    (zcCompletedGroupAlgebraProjection
      (FiniteGroupClass.pGroup p) G (modPCoefficientIndex p, V) x)
  exact hsx.symm.trans hx
def

modPCoefficientReductionAddMonoidHom

L91 ↗
ClassFieldTower.ProP.modPCoefficientReductionAddMonoidHom
Documentation

The additive inverse-limit lift of the fixed mod-p stage family.

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
open ProCGroups.Completion
open ProCGroups.InverseSystems
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def modPCoefficientReductionAddMonoidHom :
    ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G →+
      ModPCompletedGroupAlgebra p G where
  toFun :=
    (completedGroupAlgebraSystemInClass
      (FiniteGroupClass.pGroup p) (ZMod p) G).inverseLimitLift
      (fun U => modPCoefficientReductionStageRingHom p G U)
      (modPCoefficientReductionStage_compatible p G)
  map_zero' := by
    apply completedGroupAlgebraInClass_ext
      (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p)
    intro U
    exact map_zero (modPCoefficientReductionStageRingHom p G U)
  map_add' x y := by
    apply completedGroupAlgebraInClass_ext
      (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p)
    intro U
    exact map_add (modPCoefficientReductionStageRingHom p G U) x y
theorem

completedGroupAlgebraProjectionInClass_modPCoefficientReductionAddMonoidHom

L113 ↗
ClassFieldTower.ProP.completedGroupAlgebraProjectionInClass_modPCoefficientReductionAddMonoidHom
Documentation

Projection of the additive reduction lift is the chosen fixed-coefficient stage 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
open ProCGroups.Completion
open ProCGroups.InverseSystems
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem completedGroupAlgebraProjectionInClass_modPCoefficientReductionAddMonoidHom
    (U : CompletedGroupAlgebra.CompletedGroupAlgebraIndexInClass G
      (FiniteGroupClass.pGroup p))
    (x : ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G) :
    completedGroupAlgebraProjectionInClass
        (FiniteGroupClass.pGroup p) (ZMod p) G U
        (modPCoefficientReductionAddMonoidHom p G x) =
      modPCoefficientReductionStageRingHom p G U x
theorem

continuous_modPCoefficientReductionAddMonoidHom

L125 ↗
ClassFieldTower.ProP.continuous_modPCoefficientReductionAddMonoidHom
Documentation

The additive reduction lift is continuous for the two inverse-limit topologies.

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
open ProCGroups.Completion
open ProCGroups.InverseSystems
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem continuous_modPCoefficientReductionAddMonoidHom :
    Continuous (modPCoefficientReductionAddMonoidHom p G)
def

modPCoefficientReduction

L191 ↗
ClassFieldTower.ProP.modPCoefficientReduction
Documentation

The canonical continuous ring homomorphism reducing completed pro-p integer coefficients modulo p.

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
open ProCGroups.Completion
open ProCGroups.InverseSystems
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def modPCoefficientReduction :
    ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G →+*
      ModPCompletedGroupAlgebra p G where
  toFun := modPCoefficientReductionAddMonoidHom p G
  map_zero' := map_zero (modPCoefficientReductionAddMonoidHom p G)
  map_one' := by
    apply completedGroupAlgebraInClass_ext
      (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p)
    intro U
    exact map_one (modPCoefficientReductionStageRingHom p G U)
  map_add' := map_add (modPCoefficientReductionAddMonoidHom p G)
  map_mul' := by
    intro x y
    apply completedGroupAlgebraInClass_ext
      (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p)
    intro U
    exact map_mul (modPCoefficientReductionStageRingHom p G U) x y
theorem

completedGroupAlgebraProjectionInClass_modPCoefficientReduction

L212 ↗
ClassFieldTower.ProP.completedGroupAlgebraProjectionInClass_modPCoefficientReduction
Documentation

Projection of coefficient reduction is the fixed p ^ 1 source projection.

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
open ProCGroups.Completion
open ProCGroups.InverseSystems
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem completedGroupAlgebraProjectionInClass_modPCoefficientReduction
    (U : CompletedGroupAlgebra.CompletedGroupAlgebraIndexInClass G
      (FiniteGroupClass.pGroup p))
    (x : ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G) :
    completedGroupAlgebraProjectionInClass
        (FiniteGroupClass.pGroup p) (ZMod p) G U
        (modPCoefficientReduction p G x) =
      modPCoefficientReductionStageRingHom p G U x
theorem

continuous_modPCoefficientReduction

L223 ↗
ClassFieldTower.ProP.continuous_modPCoefficientReduction
Documentation

Coefficient reduction 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
open ProCGroups.Completion
open ProCGroups.InverseSystems
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem continuous_modPCoefficientReduction :
    Continuous (modPCoefficientReduction p G)

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