NYLL
Module

StageAugmentation.lean

Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.StageAugmentation
7 declarations indexed from sourceView source ↗

Module documentation

Augmentation at all-finite quotient stages

This file defines augmentation on each finite coefficient-and-group stage of the all-finite system and proves its formulas on basis elements and compatibility with transition, coefficient, and functorial stage maps.

Imports1
Imported by2

Declarations

def

completedGroupAlgebraStageAugmentation

L38 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation
Documentation

The augmentation map on a finite stage is the ring homomorphism \(R[G/U]\to R\) that sends every group-like basis element to \(1\).

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 completedGroupAlgebraStageAugmentation (R : Type u) (G : Type v) [CommRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraStage R G U →+* R
theorem

completedGroupAlgebraStageAugmentation_of

L47 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_of
Documentation

The finite-stage augmentation sends every group-like basis element to one.

Source context 12 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]
omit [TopologicalSpace R] [IsTopologicalRing R] in
Lean source · statement
theorem completedGroupAlgebraStageAugmentation_of
    (U : CompletedGroupAlgebraIndex G) (q : CompletedGroupAlgebraQuotient G U) :
    completedGroupAlgebraStageAugmentation R G U (MonoidAlgebra.of R _ q) = 1
theorem

completedGroupAlgebraStageAugmentation_single

L56 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_single
Documentation

The finite-stage augmentation sends a singleton to its coefficient.

Source context 12 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]
omit [TopologicalSpace R] [IsTopologicalRing R] in
Lean source · statement
theorem completedGroupAlgebraStageAugmentation_single
    (U : CompletedGroupAlgebraIndex G) (q : CompletedGroupAlgebraQuotient G U) (r : R) :
    completedGroupAlgebraStageAugmentation R G U (MonoidAlgebra.single q r) = r
theorem

completedGroupAlgebraStageAugmentation_compatible

L64 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_compatible
Documentation

Finite-stage augmentations are compatible with transition maps.

Source context 12 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]
omit [TopologicalSpace R] [IsTopologicalRing R] in
Lean source · statement
theorem completedGroupAlgebraStageAugmentation_compatible
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (completedGroupAlgebraStageAugmentation R G U).comp
        (completedGroupAlgebraTransition R G hUV) =
      completedGroupAlgebraStageAugmentation R G V
theorem

completedGroupAlgebraStageAugmentation_comp_stageMap

L80 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_comp_stageMap
Documentation

Finite-stage augmentation after the stage map is the abstract group-algebra augmentation.

Source context 12 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]
omit [TopologicalSpace R] [IsTopologicalRing R] in
Lean source · statement
theorem completedGroupAlgebraStageAugmentation_comp_stageMap
    (U : CompletedGroupAlgebraIndex G) :
    (completedGroupAlgebraStageAugmentation R G U).comp
        (completedGroupAlgebraStageMap R G U) =
      groupAlgebraAugmentation R G
theorem

completedGroupAlgebraStageAugmentation_comp_stageCoeffMap

L94 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_comp_stageCoeffMap
Documentation

Finite-stage augmentation is natural in the coefficient ring.

Source context 12 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]
omit [TopologicalSpace R] [IsTopologicalRing R] in
Lean source · statement
theorem completedGroupAlgebraStageAugmentation_comp_stageCoeffMap
    (S : Type w) [CommRing S] (f : R →+* S) (U : CompletedGroupAlgebraIndex G) :
    (completedGroupAlgebraStageAugmentation S G U).comp
        (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U) =
      f.comp (completedGroupAlgebraStageAugmentation R G U)
theorem

completedGroupAlgebraStageAugmentation_comp_functorialStageMap

L107 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_comp_functorialStageMap
Documentation

Finite-stage augmentation is natural with respect to functorial finite-stage maps.

Source context 12 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]
omit [TopologicalSpace R] [IsTopologicalRing R] in
Lean source · statement
theorem completedGroupAlgebraStageAugmentation_comp_functorialStageMap
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) :
    (completedGroupAlgebraStageAugmentation R H V).comp
        (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ V) =
      completedGroupAlgebraStageAugmentation R G
        (completedGroupAlgebraComapIndex (G := G) φ hφ V)

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