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

ProCGroups.CompletedGroupAlgebra.Augmentation.AugmentationIdeal

5 Theorems | 1 Definition

This file defines the kernel of the canonical augmentation on the in-class completed group algebra, establishes the associated short exact sequence, and identifies the ideal through the canonical map from the algebraic group algebra.

import
Imported by

Declarations

Definition CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdealInClass 
def completedGroupAlgebraCanonicalAugmentationIdealInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    Ideal (CompletedGroupAlgebraInClass C R G) :=
  RingHom.ker (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C )

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

Theorem CompletedGroupAlgebra.mem_completedGroupAlgebraCanonicalAugmentationIdealInClass_iff 
@[simp]
theorem mem_completedGroupAlgebraCanonicalAugmentationIdealInClass_iff
    {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {C : ProCGroups.FiniteGroupClass.{v}}
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    {x : CompletedGroupAlgebraInClass C R G} :
    x ∈ completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ↔
      completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C x = 0

An in-class completed group-algebra element lies in the canonical augmentation ideal iff the in-class canonical augmentation sends it to zero.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdealInClass_subtype_injective 
theorem completedGroupAlgebraCanonicalAugmentationIdealInClass_subtype_injective
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    Function.Injective
      (fun x : completedGroupAlgebraCanonicalAugmentationIdealInClass
          (R := R) (G := G) C => (x : CompletedGroupAlgebraInClass C R G))

The inclusion of the \(C\)-indexed canonical augmentation ideal is injective.

Show Lean proof
Theorem CompletedGroupAlgebra.exact_completedGroupAlgebraCanonicalAugmentationIdealInClass_subtype 
theorem exact_completedGroupAlgebraCanonicalAugmentationIdealInClass_subtype
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    Function.Exact
      (fun x : completedGroupAlgebraCanonicalAugmentationIdealInClass
          (R := R) (G := G) C => (x : CompletedGroupAlgebraInClass C R G))
      (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C )

The \(C\)-indexed canonical augmentation ideal is exactly the kernel of the canonical augmentation.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_shortExact 
theorem completedGroupAlgebraCanonicalAugmentationInClass_shortExact
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    Function.Injective
        (fun x : completedGroupAlgebraCanonicalAugmentationIdealInClass
          (R := R) (G := G) C => (x : CompletedGroupAlgebraInClass C R G)) ∧
      Function.Exact
        (fun x : completedGroupAlgebraCanonicalAugmentationIdealInClass
          (R := R) (G := G) C => (x : CompletedGroupAlgebraInClass C R G))
        (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C ) ∧
      Function.Surjective
        (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C )

The canonical augmentation sequence with augmentation ideal as kernel is short exact: the inclusion is injective, its image is the kernel of augmentation, and the augmentation is surjective.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_of 
@[simp]
theorem completedGroupAlgebraCanonicalAugmentationInClass_of
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] (g : G) :
    completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
        (completedGroupAlgebraOfInClass C R G g) = 1

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

Show Lean proof