ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.AugmentationIdeal

13 Theorems | 1 Definition

This file defines the kernel of the canonical augmentation on the all-finite completed group algebra, packages its short exact sequence, and proves comparison and functoriality formulas for the ideal.

imports

Imported by

ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation

Definition CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdeal

def completedGroupAlgebraCanonicalAugmentationIdeal (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] : Ideal (CompletedGroupAlgebraCarrier R G) :=
  RingHom.ker (completedGroupAlgebraCanonicalAugmentation R G)

The canonical augmentation ideal \(I_G\subseteq \widehat{R[G]}\) is the kernel of the completed augmentation \(\varepsilon:\widehat{R[G]}\to R\).

Theorem CompletedGroupAlgebra.mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff

@[simp]
theorem mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff
    {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {x : CompletedGroupAlgebraCarrier R G} :
    x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R G ↔
      completedGroupAlgebraCanonicalAugmentation R G x = 0

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

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdeal_subtype_injective

theorem completedGroupAlgebraCanonicalAugmentationIdeal_subtype_injective :
    Function.Injective
      (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
        (x : CompletedGroupAlgebraCarrier R G))

The inclusion of the canonical completed augmentation ideal is injective.

Show Lean proof

Theorem CompletedGroupAlgebra.exact_completedGroupAlgebraCanonicalAugmentationIdeal_subtype

theorem exact_completedGroupAlgebraCanonicalAugmentationIdeal_subtype :
    Function.Exact
      (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
        (x : CompletedGroupAlgebraCarrier R G))
      (completedGroupAlgebraCanonicalAugmentation R G)

The canonical completed augmentation ideal is exactly the kernel of the canonical augmentation.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_shortExact

theorem completedGroupAlgebraCanonicalAugmentation_shortExact :
    Function.Injective
        (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
          (x : CompletedGroupAlgebraCarrier R G)) ∧
      Function.Exact
        (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
          (x : CompletedGroupAlgebraCarrier R G))
        (completedGroupAlgebraCanonicalAugmentation R G) ∧
      Function.Surjective (completedGroupAlgebraCanonicalAugmentation R G)

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.completedGroupAlgebraCanonicalAugmentationIdeal_comap_fromInClass

@[simp]
theorem completedGroupAlgebraCanonicalAugmentationIdeal_comap_fromInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Ideal.comap (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)
        (completedGroupAlgebraCanonicalAugmentationIdeal R G) =
      completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C

The all-finite augmentation ideal pulls back along the from-in-class comparison map to the class-indexed augmentation ideal.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdealInClass_map_fromInClass

@[simp]
theorem completedGroupAlgebraCanonicalAugmentationIdealInClass_map_fromInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Ideal.map (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)
        (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ) =
      completedGroupAlgebraCanonicalAugmentationIdeal R G

The from-in-class comparison map sends the class-indexed augmentation ideal into the all-finite augmentation ideal.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraToInClass_mem_canonicalAugmentationIdeal_iff

@[simp]
theorem completedGroupAlgebraToInClass_mem_canonicalAugmentationIdeal_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 : CompletedGroupAlgebraCarrier R G} :
    completedGroupAlgebraToInClassRingHom (R := R) (G := G) C x ∈
        completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ↔
      x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R G

The all-finite-to-in-class comparison map preserves and reflects membership in the canonical augmentation ideal.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_toInClass

@[simp]
theorem completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_toInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    Ideal.comap (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )
        (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ) =
      completedGroupAlgebraCanonicalAugmentationIdeal R G

The class-indexed augmentation ideal pulls back along the to-in-class comparison map to the all-finite augmentation ideal.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdeal_map_toInClass

@[simp]
theorem completedGroupAlgebraCanonicalAugmentationIdeal_map_toInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Ideal.map (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )
        (completedGroupAlgebraCanonicalAugmentationIdeal R G) =
      completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C

The to-in-class comparison map sends the all-finite augmentation ideal into the class-indexed augmentation ideal.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraMap_sub_one_of

@[simp]
theorem completedGroupAlgebraMap_sub_one_of
    (φ : G →* H) (hφ : Continuous φ) (g : G) :
    completedGroupAlgebraMap (G := G) (H := H) R φ hφ
        (completedGroupAlgebraOf R G g - 1) =
      completedGroupAlgebraOf R H (φ g) - 1

A functorial all-finite completed group-algebra map sends augmentation generators to their images.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraMap_mem_canonicalAugmentationIdeal_iff

@[simp]
theorem completedGroupAlgebraMap_mem_canonicalAugmentationIdeal_iff
    {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (φ : G →* H) (hφ : Continuous φ)
    {x : CompletedGroupAlgebraCarrier R G} :
    completedGroupAlgebraMap (G := G) (H := H) R φ hφ x ∈
        completedGroupAlgebraCanonicalAugmentationIdeal R H ↔
      x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R G

A functorial all-finite completed group-algebra map preserves and reflects membership in the canonical augmentation ideal.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdeal_comap_map

@[simp]
theorem completedGroupAlgebraCanonicalAugmentationIdeal_comap_map
    (φ : G →* H) (hφ : Continuous φ) :
    Ideal.comap (completedGroupAlgebraMap (G := G) (H := H) R φ hφ)
        (completedGroupAlgebraCanonicalAugmentationIdeal R H) =
      completedGroupAlgebraCanonicalAugmentationIdeal R G

Pulling back the target canonical augmentation ideal along a completed group-algebra map gives the source canonical augmentation ideal.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdeal_map_functorial_of_surjective

theorem completedGroupAlgebraCanonicalAugmentationIdeal_map_functorial_of_surjective
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (φ : G →* H) (hφ : Continuous φ)
    (hφsurj : Function.Surjective φ) :
    Ideal.map (completedGroupAlgebraMap (G := G) (H := H) R φ hφ)
        (completedGroupAlgebraCanonicalAugmentationIdeal R G) =
      completedGroupAlgebraCanonicalAugmentationIdeal R H

A surjective functorial map sends the canonical completed augmentation ideal onto the target canonical augmentation ideal.

Show Lean proof

ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.AugmentationIdeal

Declarations