ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation

6 Theorems | 3 Definitions

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.

import

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap

Imported by

Definition FoxDifferential.modNCompletedGroupAlgebraStageAugmentation

def modNCompletedGroupAlgebraStageAugmentation (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    ModNCompletedGroupAlgebraStage n G U →+* ModNCompletedCoeff n :=
  MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)
    (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)
    (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →* ModNCompletedCoeff n)

The augmentation on one residue-coefficient finite stage.

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentation_of

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraStageAugmentation_of
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (q :
        _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) :
    modNCompletedGroupAlgebraStageAugmentation n G U
        (MonoidAlgebra.of (ModNCompletedCoeff n) _ q) = 1

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

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentation_compatible

omit [Fact (0 < n)] in
@[simp 900]
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

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

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentation_comp_stageMap

omit [Fact (0 < n)] in
@[simp 900]
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)

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

Show Lean proof

Definition FoxDifferential.modNCompletedGroupAlgebraAugmentationAt

def modNCompletedGroupAlgebraAugmentationAt (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    ModNCompletedGroupAlgebra n G → ModNCompletedCoeff n :=
  fun x => modNCompletedGroupAlgebraStageAugmentation n G U
    (modNCompletedGroupAlgebraProjection n G U x)

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

Theorem FoxDifferential.modNCompletedGroupAlgebraAugmentationAt_eq_of_le

omit [Fact (0 < n)] in
@[simp 900]
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

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

Show Lean proof

Definition FoxDifferential.modNCompletedGroupAlgebraAugmentation

def modNCompletedGroupAlgebraAugmentation :
    ModNCompletedGroupAlgebra n G → ModNCompletedCoeff n :=
  modNCompletedGroupAlgebraAugmentationAt n G
      (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)

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

Theorem FoxDifferential.modNCompletedGroupAlgebraAugmentation_eq_at

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraAugmentation_eq_at
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (x :
        ModNCompletedGroupAlgebra n G) :
    modNCompletedGroupAlgebraAugmentation n G x =
      modNCompletedGroupAlgebraAugmentationAt n G U x

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

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraAugmentation_toCompleted

omit [Fact (0 < n)] in
@[simp]
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

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

Show Lean proof

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation

Declarations