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

ProCGroups.CompletedGroupAlgebra.Augmentation.Functoriality

5 Theorems

Maps of in-class completed group algebras commute with canonical augmentation. This file derives the corresponding comap and image formulas for augmentation ideals, including the surjective case.

import
Imported by

Declarations

Theorem CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_map 
@[simp 900]
theorem completedGroupAlgebraCanonicalAugmentationInClass_map
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := H) C
        (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x) =
      completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C x

The in-class canonical augmentation is natural under functorial completed maps.

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

Composing an in-class completed map with augmentation gives the source augmentation.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraMapInClass_mem_canonicalAugmentationIdeal_iff 
@[simp]
theorem completedGroupAlgebraMapInClass_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]
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ)
    {x : CompletedGroupAlgebraInClass C R G} :
    completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x ∈
        completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C ↔
      x ∈ completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C

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

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

The \(C\)-indexed canonical augmentation ideal is pulled back to itself by functorial maps.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGACanonicalAugmentationIdealInClass_map_functorial_of_surj 
theorem completedGACanonicalAugmentationIdealInClass_map_functorial_of_surj
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hH : HasOpenNormalBasisInClass C H)
    (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ) :
    Ideal.map (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ)
        (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ) =
      completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C

A surjective functorial map sends the \(C\)-indexed canonical augmentation ideal onto the target canonical augmentation ideal.

Show Lean proof