NYLL
Module

StageAugmentation.lean

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

Module documentation

Augmentation at in-class quotient stages

This file defines augmentation on each in-class finite stage and proves its values on basis elements and compatibility with transition, coefficient-change, and functorial stage maps.

Imports1
Imported by2

Declarations

def

completedGroupAlgebraStageAugmentationInClass

L34 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass
Documentation

The augmentation map on one \(C\)-indexed 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]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def completedGroupAlgebraStageAugmentationInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    CompletedGroupAlgebraStageInClass C R G U →+* R
theorem

completedGroupAlgebraStageAugmentationInClass_of

L43 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_of
Documentation

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

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]
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_of
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (q : CompletedGroupAlgebraQuotientInClass G C U) :
    completedGroupAlgebraStageAugmentationInClass C R G U (MonoidAlgebra.of R _ q) = 1
theorem

completedGroupAlgebraStageAugmentationInClass_single

L52 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_single
Documentation

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

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]
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_single
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (q : CompletedGroupAlgebraQuotientInClass G C U) (r : R) :
    completedGroupAlgebraStageAugmentationInClass C R G U (MonoidAlgebra.single q r) = r
theorem

completedGroupAlgebraStageAugmentationInClass_compatible

L60 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_compatible
Documentation

In-class finite-stage augmentations are compatible with transition maps.

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]
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_compatible
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    (completedGroupAlgebraStageAugmentationInClass C R G U).comp
        (completedGroupAlgebraTransitionInClass C R G hUV) =
      completedGroupAlgebraStageAugmentationInClass C R G V
theorem

completedGroupAlgebraStageAugmentationInClass_comp_stageMapInClass

L79 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_comp_stageMapInClass
Documentation

Composing the in-class finite-stage augmentation with the stage map gives the 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]
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_stageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
    (completedGroupAlgebraStageAugmentationInClass C R G U).comp
        (completedGroupAlgebraStageMapInClass C R G U) =
      groupAlgebraAugmentation R G
theorem

completedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMapInClass

L92 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMapInClass
Documentation

In-class finite-stage 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]
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_stageCoeffMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S]
    (f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C) :
    (completedGroupAlgebraStageAugmentationInClass C S G U).comp
        (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U) =
      f.comp (completedGroupAlgebraStageAugmentationInClass C R G U)
theorem

completedGroupAlgebraStageAugmentationInClass_comp_functorialStageMapInClass

L105 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentationInClass_comp_functorialStageMapInClass
Documentation

In-class finite-stage augmentation is natural for functorial finite-stage maps.

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]
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_functorialStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
    (completedGroupAlgebraStageAugmentationInClass C R H V).comp
        (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := R) φ hφ V) =
      completedGroupAlgebraStageAugmentationInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)

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