Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Comparison
ProCGroups/CompletedGroupAlgebra/InClassFunctoriality/Comparison

ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.Comparison

8 Theorems

This file computes the canonical maps between all-finite and in-class completed group algebras on group-like elements and their differences from one. It also records the corresponding formulas for functorial maps and restricted scalar actions.

imports
Imported by

Declarations

Theorem CompletedGroupAlgebra.completedGroupAlgebraToInClass_of 
@[simp]
theorem completedGroupAlgebraToInClass_of
    (C : ProCGroups.FiniteGroupClass.{v})
    (g : G) :
    completedGroupAlgebraToInClassRingHom (R := R) (G := G) C
        (completedGroupAlgebraOf R G g) =
      completedGroupAlgebraOfInClass C R G g

The all-finite completed group algebra comparison sends group-like elements to the \(C\)-indexed group-like elements.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraToInClass_of_sub_one 
@[simp]
theorem completedGroupAlgebraToInClass_of_sub_one
    (C : ProCGroups.FiniteGroupClass.{v})
    (g : G) :
    completedGroupAlgebraToInClassRingHom (R := R) (G := G) C
        (completedGroupAlgebraOf R G g - 1) =
      completedGroupAlgebraOfInClass C R G g - 1

The comparison map to a class-indexed completion sends all-finite augmentation generators to class-indexed generators.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraToInClass_restrictScalars_sub_one_smul 
@[simp]
theorem completedGroupAlgebraToInClass_restrictScalars_sub_one_smul
    (C : ProCGroups.FiniteGroupClass.{v})
    (A : Type w) [AddCommGroup A] [Module (CompletedGroupAlgebraInClass C R G) A]
    (g : G) (a : A) :
    letI : Module (CompletedGroupAlgebraCarrier R G) A :=
      Module.compHom A (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )
    (completedGroupAlgebraOf R G g - 1) • a =
      (completedGroupAlgebraOfInClass C R G g - 1) • a

After restricting scalars along \(\widehat{R[G]} \to \widehat{R[G]}_C\), the all-finite augmentation generator acts as the matching \(C\)-indexed generator.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraFromInClass_of 
@[simp]
theorem completedGroupAlgebraFromInClass_of
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (g : G) :
    completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
        (completedGroupAlgebraOfInClass C R G g) =
      completedGroupAlgebraOf R G g

The comparison map from a class-indexed completion sends class-indexed group-like elements to all-finite group-like elements.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraFromInClass_of_sub_one 
@[simp]
theorem completedGroupAlgebraFromInClass_of_sub_one
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (g : G) :
    completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG
        (completedGroupAlgebraOfInClass C R G g - 1) =
      completedGroupAlgebraOf R G g - 1

The comparison map from a class-indexed completion sends class-indexed augmentation generators to all-finite generators.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraFromInClass_restrictScalars_sub_one_smul 
@[simp]
theorem completedGroupAlgebraFromInClass_restrictScalars_sub_one_smul
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G)
    (A : Type w) [AddCommGroup A] [Module (CompletedGroupAlgebraCarrier R G) A]
    (g : G) (a : A) :
    letI : Module (CompletedGroupAlgebraInClass C R G) A :=
      Module.compHom A (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)
    (completedGroupAlgebraOfInClass C R G g - 1) • a =
      (completedGroupAlgebraOf R G g - 1) • a

After restricting scalars along \(\widehat{R[G]}_C \to \widehat{R[G]}\), the \(C\)-indexed augmentation generator acts as the matching all-finite generator.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraMapInClass_of 
@[simp]
theorem completedGroupAlgebraMapInClass_of
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (g : G) :
    completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
        (completedGroupAlgebraOfInClass C R G g) =
      completedGroupAlgebraOfInClass C R H (φ g)

The class-indexed completed group-algebra map sends the completed group-like element of \(g\) to the completed group-like element of its image.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraMapInClass_of_sub_one 
@[simp]
theorem completedGroupAlgebraMapInClass_of_sub_one
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (g : G) :
    completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
        (completedGroupAlgebraOfInClass C R G g - 1) =
      completedGroupAlgebraOfInClass C R H (φ g) - 1

The class-indexed functorial map sends group-like augmentation generators to their images.

Show Lean proof