NYLL
Module

Augmentation.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation
9 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — coefficient rings — mod-\(n\) completed group algebra — augmentation

The principal declarations in this module are:

  • modNCompletedGroupAlgebraStageAugmentation

The augmentation on one residue-coefficient finite stage.

  • modNCompletedGroupAlgebraAugmentationAt

The augmentation value of a residue-coefficient completed point, read at one finite stage.

  • modNCompletedGroupAlgebraStageAugmentation_of

The finite-stage \(n\)-modular augmentation sends every group-like basis element to \(1\).

  • modNCompletedGroupAlgebraStageAugmentation_compatible

Finite-stage \(n\)-modular augmentations are compatible with group-quotient transition maps.

Imports1
Imported by2

Declarations

def

modNCompletedGroupAlgebraStageAugmentation

L38 ↗
FoxDifferential.modNCompletedGroupAlgebraStageAugmentation
Documentation

The augmentation on one residue-coefficient finite stage.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def modNCompletedGroupAlgebraStageAugmentation (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    ModNCompletedGroupAlgebraStage n G U →+* ModNCompletedCoeff n
theorem

modNCompletedGroupAlgebraStageAugmentation_of

L48 ↗
FoxDifferential.modNCompletedGroupAlgebraStageAugmentation_of
Documentation

The finite-stage \(n\)-modular augmentation sends every group-like basis element to \(1\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageAugmentation_of
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (q :
        _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) :
    modNCompletedGroupAlgebraStageAugmentation n G U
        (MonoidAlgebra.of (ModNCompletedCoeff n) _ q) = 1
theorem

modNCompletedGroupAlgebraStageAugmentation_compatible

L65 ↗
FoxDifferential.modNCompletedGroupAlgebraStageAugmentation_compatible
Documentation

Finite-stage \(n\)-modular augmentations are compatible with group-quotient transition maps.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageAugmentation_compatible
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (modNCompletedGroupAlgebraStageAugmentation n G U).comp
        (modNCompletedGroupAlgebraTransition n G hUV) =
      modNCompletedGroupAlgebraStageAugmentation n G V
theorem

modNCompletedGroupAlgebraStageAugmentation_comp_stageMap

L140 ↗
FoxDifferential.modNCompletedGroupAlgebraStageAugmentation_comp_stageMap
Documentation

Composing the finite-stage \(n\)-modular augmentation with the dense stage map gives the ordinary \(n\)-modular group-algebra augmentation.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageAugmentation_comp_stageMap
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    (modNCompletedGroupAlgebraStageAugmentation n G U).comp
        (modNCompletedGroupAlgebraStageMap n G U) =
      MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
        (1 : G →* ModNCompletedCoeff n)
def

modNCompletedGroupAlgebraAugmentationAt

L244 ↗
FoxDifferential.modNCompletedGroupAlgebraAugmentationAt
Documentation

The augmentation value of a residue-coefficient completed point, read at one finite stage.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def modNCompletedGroupAlgebraAugmentationAt (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    ModNCompletedGroupAlgebra n G → ModNCompletedCoeff n
theorem

modNCompletedGroupAlgebraAugmentationAt_eq_of_le

L256 ↗
FoxDifferential.modNCompletedGroupAlgebraAugmentationAt_eq_of_le
Documentation

The finite coordinate used to compute the \(n\)-modular completed augmentation is independent of passing to a finer quotient stage.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraAugmentationAt_eq_of_le
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (x :
        ModNCompletedGroupAlgebra n G) :
    modNCompletedGroupAlgebraAugmentationAt n G U x =
      modNCompletedGroupAlgebraAugmentationAt n G V x
def

modNCompletedGroupAlgebraAugmentation

L285 ↗
FoxDifferential.modNCompletedGroupAlgebraAugmentation
Documentation

The canonical augmentation on the residue-coefficient completed group algebra.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def modNCompletedGroupAlgebraAugmentation :
    ModNCompletedGroupAlgebra n G → ModNCompletedCoeff n
theorem

modNCompletedGroupAlgebraAugmentation_eq_at

L293 ↗
FoxDifferential.modNCompletedGroupAlgebraAugmentation_eq_at
Documentation

The \(n\)-modular completed augmentation is computed at any finite quotient stage.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraAugmentation_eq_at
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (x :
        ModNCompletedGroupAlgebra n G) :
    modNCompletedGroupAlgebraAugmentation n G x =
      modNCompletedGroupAlgebraAugmentationAt n G U x
theorem

modNCompletedGroupAlgebraAugmentation_toCompleted

L309 ↗
FoxDifferential.modNCompletedGroupAlgebraAugmentation_toCompleted
Documentation

The \(n\)-modular completed augmentation extends the abstract \(n\)-modular group-algebra augmentation through the dense map.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraAugmentation_toCompleted
    (x : ModNCompletedGroupRing n G) :
    modNCompletedGroupAlgebraAugmentation n G (toModNCompletedGroupAlgebra n G x) =
      MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
        (1 : G →* ModNCompletedCoeff n) x

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