NYLL
Module

CanonicalAugmentation.lean

Nyll.ProCGroups.CompletedGroupAlgebra.Augmentation.CanonicalAugmentation
12 declarations indexed from sourceView source ↗

Module documentation

Canonical augmentation of the in-class completion

Compatible finite-stage augmentations assemble into the canonical augmentation of the in-class completed group algebra. This file proves its projection, coefficient-map, continuity, and surjectivity properties.

Imports1
Imported by3

Declarations

def

completedGroupAlgebraAugmentationAtInClass

L35 ↗
CompletedGroupAlgebra.completedGroupAlgebraAugmentationAtInClass
Documentation

The \(C\)-indexed completed augmentation evaluated at a finite stage.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def completedGroupAlgebraAugmentationAtInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    CompletedGroupAlgebraInClass C R G → R
theorem

completedGroupAlgebraAugmentationAtInClass_eq_of_le

L46 ↗
CompletedGroupAlgebra.completedGroupAlgebraAugmentationAtInClass_eq_of_le
Documentation

The augmentation value read at a finer in-class stage agrees after transition.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraAugmentationAtInClass_eq_of_le
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
    (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraAugmentationAtInClass C R G  U x =
      completedGroupAlgebraAugmentationAtInClass C R G  V x
def

completedGroupAlgebraCanonicalAugmentationInClass

L72 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass
Documentation

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

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def completedGroupAlgebraCanonicalAugmentationInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    CompletedGroupAlgebraInClass C R G →+* R
theorem

completedGroupAlgebraCanonicalAugmentationInClass_eq_at

L83 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_eq_at
Documentation

The in-class canonical augmentation can be computed at any in-class stage.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraCanonicalAugmentationInClass_eq_at
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C x =
      completedGroupAlgebraAugmentationAtInClass C R G  U x
theorem

completedGroupAlgebraStageAugmentationInClass_comp_projectionInClass

L95 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_comp_projectionInClass
Documentation

Stage augmentation after projection is the in-class canonical augmentation.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraStageAugmentationInClass_comp_projectionInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    (completedGroupAlgebraStageAugmentationInClass C R G U).comp
        (completedGroupAlgebraProjectionInClass C R G U) =
      completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
theorem

canonicalAugmentationInClass_toCompleted

L112 ↗
CompletedGroupAlgebra.canonicalAugmentationInClass_toCompleted
Documentation

The in-class canonical augmentation extends the abstract augmentation on the dense algebraic map.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem canonicalAugmentationInClass_toCompleted
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] (x : MonoidAlgebra R G) :
    completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
        (toCompletedGroupAlgebraInClass C R G x) =
      groupAlgebraAugmentation R G x
theorem

completedGACanonicalAugmentationInClass_comp_toCompletedGAInClass

L133 ↗
CompletedGroupAlgebra.completedGACanonicalAugmentationInClass_comp_toCompletedGAInClass
Documentation

Composing the dense in-class map with canonical augmentation gives abstract augmentation.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGACanonicalAugmentationInClass_comp_toCompletedGAInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C ).comp
        (toCompletedGroupAlgebraInClassRingHom C R G) =
      groupAlgebraAugmentation R G
theorem

completedGroupAlgebraCanonicalAugmentationInClass_comp_coeffMapInClass

L146 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_comp_coeffMapInClass
Documentation

In-class canonical augmentation is natural in the coefficient ring.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraCanonicalAugmentationInClass_comp_coeffMapInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
    (f : R →+* S) :
    (completedGroupAlgebraCanonicalAugmentationInClass (R := S) (G := G) C ).comp
        (completedGroupAlgebraCoeffMapInClass (R := R) (G := G) C S f) =
      f.comp (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C )
theorem

completedGroupAlgebraCanonicalAugmentationInClass_algebraMap

L172 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_algebraMap
Documentation

The in-class canonical augmentation sends scalar algebra-map elements to their scalar.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraCanonicalAugmentationInClass_algebraMap
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] (r : R) :
    completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
        (algebraMap R (CompletedGroupAlgebraInClass C R G) r) = r
theorem

completedGroupAlgebraCanonicalAugmentationInClass_surjective

L204 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_surjective
Documentation

The \(C\)-indexed canonical augmentation \(\varepsilon_C:\widehat{R[G]}_C\to R\) is surjective.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraCanonicalAugmentationInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    Function.Surjective
      (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C )
theorem

continuous_completedGroupAlgebraCanonicalAugmentationInClass

L217 ↗
CompletedGroupAlgebra.continuous_completedGroupAlgebraCanonicalAugmentationInClass
Documentation

The \(C\)-indexed canonical augmentation is continuous for the inverse-limit topology on \(\widehat{R[G]}_C\).

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem continuous_completedGroupAlgebraCanonicalAugmentationInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    Continuous (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C )
theorem

completedGroupAlgebraInClass_hasCompletedGroupAlgebraAugmentation

L237 ↗
CompletedGroupAlgebra.completedGroupAlgebraInClass_hasCompletedGroupAlgebraAugmentation
Documentation

The \(C\)-indexed completed group algebra carries the standard model-independent augmentation package.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraInClass_hasCompletedGroupAlgebraAugmentation
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    hasCompletedGroupAlgebraAugmentation R G (CompletedGroupAlgebraInClass C R G)
      (toCompletedGroupAlgebraInClassRingHom C R G)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.