NYLL
Module

CoefficientReductionCompatibility.lean

Nyll.ProCGroups.ProP.Fox.CoefficientReductionCompatibility
7 declarations indexed from sourceView source ↗

Module documentation

Compatibility of mod-p coefficient reduction

The continuous coefficient-reduction homomorphism preserves group-like elements, commutes with augmentation, and carries the algebraic and closed augmentation filtrations to their mod-p counterparts.

Imports2
Imported by3

Declarations

theorem

modPCoefficientReduction_groupLike

L37 ↗
ClassFieldTower.ProP.modPCoefficientReduction_groupLike
Documentation

Coefficient reduction carries an integral completed group-like element to the corresponding mod-p completed group-like element.

Source context 10 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
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem modPCoefficientReduction_groupLike (g : G) :
    modPCoefficientReduction p G
        (zcGroupLike (FiniteGroupClass.pGroup p) G g) =
      completedGroupAlgebraOfInClass
        (FiniteGroupClass.pGroup p) (ZMod p) G g
theorem

modPCoefficientReduction_groupLike_sub_one

L62 ↗
ClassFieldTower.ProP.modPCoefficientReduction_groupLike_sub_one
Documentation

Coefficient reduction carries [g] - 1 to the mod-p group-like difference.

Source context 10 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
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem modPCoefficientReduction_groupLike_sub_one (g : G) :
    modPCoefficientReduction p G
        (zcGroupLike (FiniteGroupClass.pGroup p) G g - 1) =
      groupLikeDifference p G g
theorem

modPCoefficientReduction_augmentation

L71 ↗
ClassFieldTower.ProP.modPCoefficientReduction_augmentation
Documentation

Coefficient reduction commutes with augmentation after projecting the pro-p integer coefficient to its distinguished mod-p coordinate.

Source context 10 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
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem modPCoefficientReduction_augmentation
    (x : ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G) :
    completedGroupAlgebraCanonicalAugmentationInClass
        (R := ZMod p) (G := G) (FiniteGroupClass.pGroup p)
        (modPCoefficientReduction p G x) =
      proCIntegerProj
        (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))
        (modPCoefficientIndex p)
        (zcCompletedGroupAlgebraAugmentation
          (FiniteGroupClass.pGroup p) G x)
theorem

modPCoefficientReduction_mem_augmentationIdeal

L98 ↗
ClassFieldTower.ProP.modPCoefficientReduction_mem_augmentationIdeal
Documentation

Coefficient reduction sends the source augmentation ideal into the mod-p augmentation ideal.

Source context 10 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
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem modPCoefficientReduction_mem_augmentationIdeal
    {x : ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G}
    (hx : x ∈ zcCompletedGroupAlgebraAugmentationIdeal
      (FiniteGroupClass.pGroup p) G) :
    modPCoefficientReduction p G x ∈ modPAugmentationIdeal p G
theorem

modPCoefficientReduction_mem_augmentationIdeal_pow

L112 ↗
ClassFieldTower.ProP.modPCoefficientReduction_mem_augmentationIdeal_pow
Documentation

Coefficient reduction sends each algebraic source augmentation-ideal power into the corresponding mod-p ideal power.

Source context 10 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
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem modPCoefficientReduction_mem_augmentationIdeal_pow
    (n : ℕ)
    {x : ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G}
    (hx : x ∈
      (zcCompletedGroupAlgebraAugmentationIdeal
        (FiniteGroupClass.pGroup p) G) ^ n) :
    modPCoefficientReduction p G x ∈ (modPAugmentationIdeal p G) ^ n
def

zcClosedAugmentationPower

L125 ↗
ClassFieldTower.ProP.zcClosedAugmentationPower
Documentation

The closure of the n-th source augmentation-ideal power.

Source context 10 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
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def zcClosedAugmentationPower (n : ℕ) :
    Ideal (ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G)
theorem

modPCoefficientReduction_mem_closedAugmentationPower

L132 ↗
ClassFieldTower.ProP.modPCoefficientReduction_mem_closedAugmentationPower
Documentation

Continuous coefficient reduction sends closed source augmentation powers into the corresponding closed mod-p augmentation powers.

Source context 10 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
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem modPCoefficientReduction_mem_closedAugmentationPower
    (n : ℕ)
    {x : ZCCompletedGroupAlgebra (FiniteGroupClass.pGroup p) G}
    (hx : x ∈ zcClosedAugmentationPower p G n) :
    modPCoefficientReduction p G x ∈ 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.