Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.Augmentation.StageAugmentation
ProCGroups/CompletedGroupAlgebra/Augmentation/StageAugmentation

ProCGroups.CompletedGroupAlgebra.Augmentation.StageAugmentation

6 Theorems | 1 Definition

This file defines augmentation on each in-class finite stage and proves its values on basis elements and compatibility with transition, coefficient-change, and functorial stage maps.

import
Imported by

Declarations

Definition CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass 
def completedGroupAlgebraStageAugmentationInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    CompletedGroupAlgebraStageInClass C R G U →+* R :=
  groupAlgebraAugmentation R (CompletedGroupAlgebraQuotientInClass G C U)

The augmentation map on one \(C\)-indexed finite stage.

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_of 
@[simp]
theorem completedGroupAlgebraStageAugmentationInClass_of
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (q : CompletedGroupAlgebraQuotientInClass G C U) :
    completedGroupAlgebraStageAugmentationInClass C R G U (MonoidAlgebra.of R _ q) = 1

The in-class finite-stage augmentation sends every group-like basis element to one.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_single 
@[simp]
theorem completedGroupAlgebraStageAugmentationInClass_single
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (q : CompletedGroupAlgebraQuotientInClass G C U) (r : R) :
    completedGroupAlgebraStageAugmentationInClass C R G U (MonoidAlgebra.single q r) = r

The in-class finite-stage augmentation sends a singleton to its coefficient.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_compatible 
@[simp]
theorem completedGroupAlgebraStageAugmentationInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    (completedGroupAlgebraStageAugmentationInClass C R G U).comp
        (completedGroupAlgebraTransitionInClass C R G hUV) =
      completedGroupAlgebraStageAugmentationInClass C R G V

In-class finite-stage augmentations are compatible with transition maps.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_comp_stageMapInClass 
@[simp]
theorem completedGroupAlgebraStageAugmentationInClass_comp_stageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
    (completedGroupAlgebraStageAugmentationInClass C R G U).comp
        (completedGroupAlgebraStageMapInClass C R G U) =
      groupAlgebraAugmentation R G

Composing the in-class finite-stage augmentation with the stage map gives the abstract augmentation.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMapInClass 
@[simp]
theorem completedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S]
    (f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C) :
    (completedGroupAlgebraStageAugmentationInClass C S G U).comp
        (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U) =
      f.comp (completedGroupAlgebraStageAugmentationInClass C R G U)

In-class finite-stage augmentation is natural in the coefficient ring.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_comp_functorialStageMapInClass 
@[simp]
theorem completedGroupAlgebraStageAugmentationInClass_comp_functorialStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
    (completedGroupAlgebraStageAugmentationInClass C R H V).comp
        (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := R) φ hφ V) =
      completedGroupAlgebraStageAugmentationInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)

In-class finite-stage augmentation is natural for functorial finite-stage maps.

Show Lean proof