ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Completed

10 Theorems | 4 Definitions

An algebraic augmentation compatible with the completion map extends uniquely to a continuous augmentation of the completed group algebra. This file constructs that map, its kernel ideal and short exact sequence, and the finite-group-algebra instance.

import

ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Abstract

Imported by

Definition CompletedGroupAlgebra.completedGroupAlgebraCoefficientMap

noncomputable def completedGroupAlgebraCoefficientMap
    (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
    (dense : RingHom (MonoidAlgebra R G) RG) : RingHom R RG :=
  dense.comp (algebraMap R (MonoidAlgebra R G))

The coefficient map \(R \to R[G]\) attached to a dense map from the abstract group algebra.

Theorem CompletedGroupAlgebra.completedGroupAlgebraCoefficientMap_apply

@[simp]
theorem completedGroupAlgebraCoefficientMap_apply
    (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
    (dense : RingHom (MonoidAlgebra R G) RG) (r : R) :
    completedGroupAlgebraCoefficientMap R G RG dense r =
      dense (algebraMap R (MonoidAlgebra R G) r)

The coefficient-change map is evaluated coordinatewise: the support in the finite quotient is unchanged and every coefficient is carried through the given ring homomorphism.

Show Lean proof

Definition CompletedGroupAlgebra.hasCompletedGroupAlgebraAugmentation

def hasCompletedGroupAlgebraAugmentation
    (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
    [Group G] [Ring RG] [TopologicalSpace RG]
    (dense : RingHom (MonoidAlgebra R G) RG) : Prop :=
  Exists fun ε : RingHom RG R =>
    And (ε.comp dense = groupAlgebraAugmentation R G) (Continuous ε)

A completed group algebra model has a continuous augmentation when its dense abstract group-algebra map admits a continuous extension of the abstract augmentation.

Definition CompletedGroupAlgebra.completedGroupAlgebraAugmentation

noncomputable def completedGroupAlgebraAugmentation
    (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
    [Group G] [Ring RG] [TopologicalSpace RG]
    {dense : RingHom (MonoidAlgebra R G) RG}
    (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) : RingHom RG R :=
  Classical.choose haug

The continuous augmentation extracted from completed group algebra augmentation data.

Theorem CompletedGroupAlgebra.completedGroupAlgebraAugmentation_comp_dense

theorem completedGroupAlgebraAugmentation_comp_dense
    (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
    [Group G] [Ring RG] [TopologicalSpace RG]
    {dense : RingHom (MonoidAlgebra R G) RG}
    (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
    (completedGroupAlgebraAugmentation R G RG haug).comp dense =
      groupAlgebraAugmentation R G

The completed augmentation extends the abstract augmentation along the dense algebraic map.

Show Lean proof

Theorem CompletedGroupAlgebra.continuous_completedGroupAlgebraAugmentation

theorem continuous_completedGroupAlgebraAugmentation
    (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
    [Group G] [Ring RG] [TopologicalSpace RG]
    {dense : RingHom (MonoidAlgebra R G) RG}
    (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
    Continuous (completedGroupAlgebraAugmentation R G RG haug)

The augmentation extracted from the completed augmentation package is continuous.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraAugmentation_comp_coefficientMap

theorem completedGroupAlgebraAugmentation_comp_coefficientMap
    (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
    [Group G] [Ring RG] [TopologicalSpace RG]
    {dense : RingHom (MonoidAlgebra R G) RG}
    (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
    (completedGroupAlgebraAugmentation R G RG haug).comp
        (completedGroupAlgebraCoefficientMap R G RG dense) = RingHom.id R

The coefficient map is a section of the completed augmentation.

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraAugmentationIdeal

noncomputable def completedGroupAlgebraAugmentationIdeal
    (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
    [Group G] [Ring RG] [TopologicalSpace RG]
    {dense : RingHom (MonoidAlgebra R G) RG}
    (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) : Ideal RG :=
  RingHom.ker (completedGroupAlgebraAugmentation R G RG haug)

The augmentation ideal of a completed group algebra model with augmentation data.

Theorem CompletedGroupAlgebra.mem_completedGroupAlgebraAugmentationIdeal_iff

@[simp]
theorem mem_completedGroupAlgebraAugmentationIdeal_iff
    {R : Type u} {G : Type v} {RG : Type w} [CommRing R] [TopologicalSpace R]
    [Group G] [Ring RG] [TopologicalSpace RG]
    {dense : RingHom (MonoidAlgebra R G) RG}
    {haug : hasCompletedGroupAlgebraAugmentation R G RG dense} {x : RG} :
    x ∈ completedGroupAlgebraAugmentationIdeal R G RG haug ↔
      completedGroupAlgebraAugmentation R G RG haug x = 0

A completed finite group-algebra element lies in the completed augmentation ideal iff its completed augmentation is zero.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraAugmentation_surjective

theorem completedGroupAlgebraAugmentation_surjective
    (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
    [Group G] [Ring RG] [TopologicalSpace RG]
    {dense : RingHom (MonoidAlgebra R G) RG}
    (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
    Function.Surjective (completedGroupAlgebraAugmentation R G RG haug)

The completed augmentation is split by the completed coefficient map.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraAugmentationIdeal_subtype_injective

theorem completedGroupAlgebraAugmentationIdeal_subtype_injective
    (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
    [Group G] [Ring RG] [TopologicalSpace RG]
    {dense : RingHom (MonoidAlgebra R G) RG}
    (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
    Function.Injective
      (fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG))

The inclusion of the completed augmentation ideal into the completed group algebra model is injective.

Show Lean proof

Theorem CompletedGroupAlgebra.exact_completedGroupAlgebraAugmentationIdeal_subtype

theorem exact_completedGroupAlgebraAugmentationIdeal_subtype
    (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
    [Group G] [Ring RG] [TopologicalSpace RG]
    {dense : RingHom (MonoidAlgebra R G) RG}
    (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
    Function.Exact
      (fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG))
      (completedGroupAlgebraAugmentation R G RG haug)

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

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraAugmentation_shortExact

theorem completedGroupAlgebraAugmentation_shortExact
    (R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
    [Group G] [Ring RG] [TopologicalSpace RG]
    {dense : RingHom (MonoidAlgebra R G) RG}
    (haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
    Function.Injective
        (fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG)) ∧
      Function.Exact
        (fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG))
        (completedGroupAlgebraAugmentation R G RG haug) ∧
      Function.Surjective (completedGroupAlgebraAugmentation R G RG haug)

For the completed augmentation data haug, the subtype inclusion of its augmentation ideal into \(RG\), followed by the completed augmentation, is a short exact sequence.

Show Lean proof

Theorem CompletedGroupAlgebra.finiteGroupAlgebra_hasCompletedGroupAlgebraAugmentation

theorem finiteGroupAlgebra_hasCompletedGroupAlgebraAugmentation
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [Finite G] :
    letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
    hasCompletedGroupAlgebraAugmentation R G (MonoidAlgebra R G)
      (RingHom.id (MonoidAlgebra R G))

In the finite-group case, the finite group algebra carries the completed augmentation data induced by the ordinary augmentation.

Show Lean proof

ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Completed

Declarations