FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation

6 Theorem | 3 Definition

This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.

Open this file on GitHub

import

FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap

Imported by

Definition FoxDifferential.modNCompletedGroupAlgebraStageAugmentation GitHub

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 GitHub

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 proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentation_compatible GitHub

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 proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentation_comp_stageMap GitHub

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 proof

Definition FoxDifferential.modNCompletedGroupAlgebraAugmentationAt GitHub

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 GitHub

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 proof

Definition FoxDifferential.modNCompletedGroupAlgebraAugmentation GitHub

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 GitHub

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 proof

Theorem FoxDifferential.modNCompletedGroupAlgebraAugmentation_toCompleted GitHub

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 proof

FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation

Declarations