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

ProCGroups.CompletedGroupAlgebra.Augmentation.CanonicalAugmentation

10 Theorems | 2 Definitions

Compatible finite-stage augmentations assemble into the canonical augmentation of the in-class completed group algebra. This file proves its projection, coefficient-map, continuity, and surjectivity properties.

import
Imported by

Declarations

Definition CompletedGroupAlgebra.completedGroupAlgebraAugmentationAtInClass 
def completedGroupAlgebraAugmentationAtInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    CompletedGroupAlgebraInClass C R G → R :=
  fun x => completedGroupAlgebraStageAugmentationInClass C R G U
    (completedGroupAlgebraProjectionInClass C R G U x)

The \(C\)-indexed completed augmentation evaluated at a finite stage.

Theorem CompletedGroupAlgebra.completedGroupAlgebraAugmentationAtInClass_eq_of_le 
@[simp 900]
theorem completedGroupAlgebraAugmentationAtInClass_eq_of_le
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
    (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraAugmentationAtInClass C R G  U x =
      completedGroupAlgebraAugmentationAtInClass C R G  V x

The augmentation value read at a finer in-class stage agrees after transition.

Show Lean proof
Definition CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass 
def completedGroupAlgebraCanonicalAugmentationInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    CompletedGroupAlgebraInClass C R G →+* R :=
  (completedGroupAlgebraStageAugmentationInClass C R G
    (terminalCompletedGroupAlgebraIndexInClass (G := G) C)).comp
      (completedGroupAlgebraProjectionInClass C R G
        (terminalCompletedGroupAlgebraIndexInClass (G := G) C))

The canonical augmentation on the \(C\)-indexed completed group algebra.

Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_eq_at 
@[simp]
theorem completedGroupAlgebraCanonicalAugmentationInClass_eq_at
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C x =
      completedGroupAlgebraAugmentationAtInClass C R G  U x

The in-class canonical augmentation can be computed at any in-class stage.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_comp_projectionInClass 
@[simp]
theorem completedGroupAlgebraStageAugmentationInClass_comp_projectionInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    (completedGroupAlgebraStageAugmentationInClass C R G U).comp
        (completedGroupAlgebraProjectionInClass C R G U) =
      completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C

Stage augmentation after projection is the in-class canonical augmentation.

Show Lean proof
Theorem CompletedGroupAlgebra.canonicalAugmentationInClass_toCompleted 
@[simp]
theorem canonicalAugmentationInClass_toCompleted
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] (x : MonoidAlgebra R G) :
    completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
        (toCompletedGroupAlgebraInClass C R G x) =
      groupAlgebraAugmentation R G x

The in-class canonical augmentation extends the abstract augmentation on the dense algebraic map.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGACanonicalAugmentationInClass_comp_toCompletedGAInClass 
@[simp]
theorem completedGACanonicalAugmentationInClass_comp_toCompletedGAInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C ).comp
        (toCompletedGroupAlgebraInClassRingHom C R G) =
      groupAlgebraAugmentation R G

Composing the dense in-class map with canonical augmentation gives abstract augmentation.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_comp_coeffMapInClass 
@[simp 900]
theorem completedGroupAlgebraCanonicalAugmentationInClass_comp_coeffMapInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
    (f : R →+* S) :
    (completedGroupAlgebraCanonicalAugmentationInClass (R := S) (G := G) C ).comp
        (completedGroupAlgebraCoeffMapInClass (R := R) (G := G) C S f) =
      f.comp (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C )

In-class canonical augmentation is natural in the coefficient ring.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_algebraMap 
@[simp 900]
theorem completedGroupAlgebraCanonicalAugmentationInClass_algebraMap
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] (r : R) :
    completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
        (algebraMap R (CompletedGroupAlgebraInClass C R G) r) = r

The in-class canonical augmentation sends scalar algebra-map elements to their scalar.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_surjective 
theorem completedGroupAlgebraCanonicalAugmentationInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    Function.Surjective
      (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C )

The \(C\)-indexed canonical augmentation \(\varepsilon_C:\widehat{R[G]}_C\to R\) is surjective.

Show Lean proof
Theorem CompletedGroupAlgebra.continuous_completedGroupAlgebraCanonicalAugmentationInClass 
theorem continuous_completedGroupAlgebraCanonicalAugmentationInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    Continuous (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C )

The \(C\)-indexed canonical augmentation is continuous for the inverse-limit topology on \(\widehat{R[G]}_C\).

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraInClass_hasCompletedGroupAlgebraAugmentation 
theorem completedGroupAlgebraInClass_hasCompletedGroupAlgebraAugmentation
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    hasCompletedGroupAlgebraAugmentation R G (CompletedGroupAlgebraInClass C R G)
      (toCompletedGroupAlgebraInClassRingHom C R G)

The \(C\)-indexed completed group algebra carries the standard model-independent augmentation package.

Show Lean proof