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

ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.CanonicalAugmentation

11 Theorems | 2 Definitions

This module defines the all-finite canonical augmentation as the composition of a terminal finite-stage augmentation with the canonical bundled projection, and proves that it can be computed at every finite stage.

import
Imported by

Declarations

Definition CompletedGroupAlgebra.completedGroupAlgebraAugmentationAt 
def completedGroupAlgebraAugmentationAt (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraCarrier R G → R :=
  fun x => completedGroupAlgebraStageAugmentation R G U (completedGroupAlgebraProjection R G U x)

The completed augmentation evaluated at a finite stage.

Theorem CompletedGroupAlgebra.completedGroupAlgebraAugmentationAt_eq_of_le 
@[simp]
theorem completedGroupAlgebraAugmentationAt_eq_of_le
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraAugmentationAt R G U x =
      completedGroupAlgebraAugmentationAt R G V x

The coordinate defining the completed augmentation is independent of the chosen sufficiently terminal index.

Show Lean proof
Definition CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation 
def completedGroupAlgebraCanonicalAugmentation (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] :
    CompletedGroupAlgebraCarrier R G →+* R :=
  (completedGroupAlgebraStageAugmentation R G
    (terminalCompletedGroupAlgebraIndex G)).comp
      (completedGroupAlgebraProjection R G
        (terminalCompletedGroupAlgebraIndex G))

The canonical augmentation \(\varepsilon:\widehat{R[G]}\to R\) is the ring homomorphism obtained by applying the finite-stage augmentation to any sufficiently terminal coordinate.

Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_eq_at 
@[simp]
theorem completedGroupAlgebraCanonicalAugmentation_eq_at
    (U : CompletedGroupAlgebraIndex G) (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraCanonicalAugmentation R G x =
      completedGroupAlgebraAugmentationAt R G U x

The canonical completed augmentation is computed at any finite stage.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_comp_projection 
@[simp]
theorem completedGroupAlgebraStageAugmentation_comp_projection
    (U : CompletedGroupAlgebraIndex G) :
    (completedGroupAlgebraStageAugmentation R G U).comp
        (completedGroupAlgebraProjection R G U) =
      completedGroupAlgebraCanonicalAugmentation R G

For every finite quotient stage \(U\), projecting \(\widehat{R[G]}\) to \(R[G/U]\) and then applying the finite-stage augmentation gives the canonical augmentation on \(\widehat{R[G]}\).

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra 
@[simp]
theorem completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra
    (x : MonoidAlgebra R G) :
    completedGroupAlgebraCanonicalAugmentation R G (toCompletedGroupAlgebra R G x) =
      groupAlgebraAugmentation R G x

The canonical augmentation extends the abstract group-algebra augmentation through the dense algebraic map.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_comp_toCompletedGroupAlgebra 
@[simp]
theorem completedGroupAlgebraCanonicalAugmentation_comp_toCompletedGroupAlgebra :
    (completedGroupAlgebraCanonicalAugmentation R G).comp
        (toCompletedGroupAlgebraRingHom R G) =
      groupAlgebraAugmentation R G

Composing the canonical augmentation with the dense map gives the abstract augmentation.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_comp_coeffMap 
@[simp]
theorem completedGroupAlgebraCanonicalAugmentation_comp_coeffMap
    (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
    (f : R →+* S) :
    (completedGroupAlgebraCanonicalAugmentation S G).comp
        (completedGroupAlgebraCoeffMap (R := R) (G := G) S f) =
      f.comp (completedGroupAlgebraCanonicalAugmentation R G)

Canonical augmentation is natural in the coefficient ring.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_map 
@[simp 900]
theorem completedGroupAlgebraCanonicalAugmentation_map
    (φ : G →* H) (hφ : Continuous φ)
    (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraCanonicalAugmentation R H
        (completedGroupAlgebraMap (G := G) (H := H) R φ hφ x) =
      completedGroupAlgebraCanonicalAugmentation R G x

Canonical augmentation is natural with respect to functorial completed group-algebra maps.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_comp_map 
@[simp]
theorem completedGroupAlgebraCanonicalAugmentation_comp_map
    (φ : G →* H) (hφ : Continuous φ) :
    (completedGroupAlgebraCanonicalAugmentation R H).comp
        (completedGroupAlgebraMap (G := G) (H := H) R φ hφ) =
      completedGroupAlgebraCanonicalAugmentation R G

Canonical augmentation after the functorial completed map agrees with canonical augmentation.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_of 
@[simp]
theorem completedGroupAlgebraCanonicalAugmentation_of (g : G) :
    completedGroupAlgebraCanonicalAugmentation R G (completedGroupAlgebraOf R G g) = 1

The canonical augmentation sends every completed group-like element to one.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_surjective 
theorem completedGroupAlgebraCanonicalAugmentation_surjective :
    Function.Surjective (completedGroupAlgebraCanonicalAugmentation R G)

The canonical augmentation \(\varepsilon:\widehat{R[G]}\to R\) is surjective.

Show Lean proof
Theorem CompletedGroupAlgebra.continuous_completedGroupAlgebraCanonicalAugmentation 
theorem continuous_completedGroupAlgebraCanonicalAugmentation :
    Continuous (completedGroupAlgebraCanonicalAugmentation R G)

The canonical augmentation \(\varepsilon:\widehat{R[G]}\to R\) is continuous for the inverse-limit topology on \(\widehat{R[G]}\).

Show Lean proof