Module

Completed.lean

Nyll.ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Completed

14 declarations indexed from sourceView source ↗

Module documentation

Augmentation after completion

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.

Imports1

Nyll.ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Abstract

Imported by2

def

completedGroupAlgebraCoefficientMap

L25 ↗

CompletedGroupAlgebra.completedGroupAlgebraCoefficientMap

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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

theorem

completedGroupAlgebraCoefficientMap_apply

L35 ↗

CompletedGroupAlgebra.completedGroupAlgebraCoefficientMap_apply

Documentation

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.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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)

def

hasCompletedGroupAlgebraAugmentation

L46 ↗

CompletedGroupAlgebra.hasCompletedGroupAlgebraAugmentation

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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

def

completedGroupAlgebraAugmentation

L54 ↗

CompletedGroupAlgebra.completedGroupAlgebraAugmentation

Documentation

The continuous augmentation extracted from completed group algebra augmentation data.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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

theorem

completedGroupAlgebraAugmentation_comp_dense

L62 ↗

CompletedGroupAlgebra.completedGroupAlgebraAugmentation_comp_dense

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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

theorem

continuous_completedGroupAlgebraAugmentation

L72 ↗

CompletedGroupAlgebra.continuous_completedGroupAlgebraAugmentation

Documentation

The augmentation extracted from the completed augmentation package is continuous.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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)

theorem

completedGroupAlgebraAugmentation_comp_coefficientMap

L81 ↗

CompletedGroupAlgebra.completedGroupAlgebraAugmentation_comp_coefficientMap

Documentation

The coefficient map is a section of the completed augmentation.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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

def

completedGroupAlgebraAugmentationIdeal

L95 ↗

CompletedGroupAlgebra.completedGroupAlgebraAugmentationIdeal

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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

theorem

mem_completedGroupAlgebraAugmentationIdeal_iff

L107 ↗

CompletedGroupAlgebra.mem_completedGroupAlgebraAugmentationIdeal_iff

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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

theorem

completedGroupAlgebraAugmentation_surjective

L117 ↗

CompletedGroupAlgebra.completedGroupAlgebraAugmentation_surjective

Documentation

The completed augmentation is split by the completed coefficient map.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · statement

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)

theorem

completedGroupAlgebraAugmentationIdeal_subtype_injective

L133 ↗

CompletedGroupAlgebra.completedGroupAlgebraAugmentationIdeal_subtype_injective

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · full declaration

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)) := by
  intro x y hxy
  exact Subtype.ext hxy

theorem

exact_completedGroupAlgebraAugmentationIdeal_subtype

L144 ↗

CompletedGroupAlgebra.exact_completedGroupAlgebraAugmentationIdeal_subtype

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · full declaration

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) := by
  intro x
  constructor
  · intro hx
    exact ⟨⟨x, hx⟩, rfl⟩
  · rintro ⟨y, rfl⟩
    exact y.2

theorem

completedGroupAlgebraAugmentation_shortExact

L163 ↗

CompletedGroupAlgebra.completedGroupAlgebraAugmentation_shortExact

Documentation

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.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · full declaration

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) := by
  exact ⟨completedGroupAlgebraAugmentationIdeal_subtype_injective R G RG haug,
    exact_completedGroupAlgebraAugmentationIdeal_subtype R G RG haug,
    completedGroupAlgebraAugmentation_surjective R G RG haug⟩

theorem

finiteGroupAlgebra_hasCompletedGroupAlgebraAugmentation

L182 ↗

CompletedGroupAlgebra.finiteGroupAlgebra_hasCompletedGroupAlgebraAugmentation

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
open ProCGroups
namespace CompletedGroupAlgebra
universe u v w z

Lean source · full declaration

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)) := by
  let : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
  refine Exists.intro (groupAlgebraAugmentation R G) ?_
  exact And.intro (RingHom.comp_id (groupAlgebraAugmentation R G))
    (finiteGroupAlgebra_augmentation_continuous R G)

Module documentation

Augmentation after completion

Declarations