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

ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.StageAugmentation

6 Theorems | 1 Definition

This file defines augmentation on each finite coefficient-and-group stage of the all-finite system and proves its formulas on basis elements and compatibility with transition, coefficient, and functorial stage maps.

import
Imported by

Declarations

Definition CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation 
def completedGroupAlgebraStageAugmentation (R : Type u) (G : Type v) [CommRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraStage R G U →+* R :=
  groupAlgebraAugmentation R (CompletedGroupAlgebraQuotient G U)

The augmentation map on a finite stage is the ring homomorphism \(R[G/U]\to R\) that sends every group-like basis element to \(1\).

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_of 
omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraStageAugmentation_of
    (U : CompletedGroupAlgebraIndex G) (q : CompletedGroupAlgebraQuotient G U) :
    completedGroupAlgebraStageAugmentation R G U (MonoidAlgebra.of R _ q) = 1

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

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_single 
omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraStageAugmentation_single
    (U : CompletedGroupAlgebraIndex G) (q : CompletedGroupAlgebraQuotient G U) (r : R) :
    completedGroupAlgebraStageAugmentation R G U (MonoidAlgebra.single q r) = r

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

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_compatible 
omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraStageAugmentation_compatible
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (completedGroupAlgebraStageAugmentation R G U).comp
        (completedGroupAlgebraTransition R G hUV) =
      completedGroupAlgebraStageAugmentation R G V

Finite-stage augmentations are compatible with transition maps.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_comp_stageMap 
omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraStageAugmentation_comp_stageMap
    (U : CompletedGroupAlgebraIndex G) :
    (completedGroupAlgebraStageAugmentation R G U).comp
        (completedGroupAlgebraStageMap R G U) =
      groupAlgebraAugmentation R G

Finite-stage augmentation after the stage map is the abstract group-algebra augmentation.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_comp_stageCoeffMap 
omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraStageAugmentation_comp_stageCoeffMap
    (S : Type w) [CommRing S] (f : R →+* S) (U : CompletedGroupAlgebraIndex G) :
    (completedGroupAlgebraStageAugmentation S G U).comp
        (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U) =
      f.comp (completedGroupAlgebraStageAugmentation R G U)

Finite-stage augmentation is natural in the coefficient ring.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_comp_functorialStageMap 
omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraStageAugmentation_comp_functorialStageMap
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) :
    (completedGroupAlgebraStageAugmentation R H V).comp
        (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ V) =
      completedGroupAlgebraStageAugmentation R G
        (completedGroupAlgebraComapIndex (G := G) φ hφ V)

Finite-stage augmentation is natural with respect to functorial finite-stage maps.

Show Lean proof