FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation

5 Theorem | 1 Definition

Fox Differential / Completed / Coefficient Rings / Completed Group Algebra Mod N / Within a Class / Augmentation.

import

FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap

Imported by

Definition FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass GitHub

def modNCompletedGroupAlgebraStageAugmentationInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    ModNCompletedGroupAlgebraStageInClass n G C U →+* ModNCompletedCoeff n :=
  MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)
    (CompletedGroupAlgebraQuotientInClass G C U)
    (1 : CompletedGroupAlgebraQuotientInClass G C U →* ModNCompletedCoeff n)

The augmentation on one class-restricted residue-coefficient finite stage.

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_of GitHub

theorem modNCompletedGroupAlgebraStageAugmentationInClass_of
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (q : CompletedGroupAlgebraQuotientInClass G C U) :
    modNCompletedGroupAlgebraStageAugmentationInClass n G C U
        (MonoidAlgebra.of (ModNCompletedCoeff n) _ q) = 1

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

Show proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_single GitHub

theorem modNCompletedGroupAlgebraStageAugmentationInClass_single
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (q : CompletedGroupAlgebraQuotientInClass G C U) (a : ModNCompletedCoeff n) :
    modNCompletedGroupAlgebraStageAugmentationInClass n G C U
        (MonoidAlgebra.single q a) = a

The class-indexed finite-stage \(n\)-modular augmentation sends a singleton basis element to its coefficient.

Show proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_compatible GitHub

theorem modNCompletedGroupAlgebraStageAugmentationInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
        (modNCompletedGroupAlgebraTransitionInClass n G C hUV) =
      modNCompletedGroupAlgebraStageAugmentationInClass n G C V

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

Show proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageMap GitHub

theorem modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageMap
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
        (modNCompletedGroupAlgebraStageMapInClass n G C U) =
      MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
        (1 : G →* ModNCompletedCoeff n)

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

Show proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMap GitHub

theorem modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMap
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    {m : ℕ} [Fact (0 < m)] (hnm : n ∣ m) :
    (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
        (modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := n) (m := m) (G := G) C U hnm) =
      (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
        (modNCompletedGroupAlgebraStageAugmentationInClass m G C U)

Stage augmentations commute with coefficient reduction on class-restricted finite quotient stages.

Show proof

FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation

Declarations