ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation

5 Theorems | 1 Definition

The principal declarations in this module are:

modNCompletedGroupAlgebraStageAugmentationInClass The augmentation on one class-restricted residue-coefficient finite stage. - modNCompletedGroupAlgebraStageAugmentationInClass_of The class-indexed finite-stage \(n\)-modular augmentation sends every group-like basis element to \(1\). - modNCompletedGroupAlgebraStageAugmentationInClass_single The class-indexed finite-stage \(n\)-modular augmentation sends a singleton basis element to its coefficient. - modNCompletedGroupAlgebraStageAugmentationInClass_compatible Class-indexed finite-stage \(n\)-modular augmentations are compatible with group-quotient transition maps.

import

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap

Imported by

Definition FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass

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

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

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_single

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

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_compatible

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

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageMap

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

Theorem FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMap

omit [Fact (0 < n)] in
@[simp 900]
theorem modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMap
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    {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 Lean proof

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation

Declarations