NYLL
Module

Augmentation.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation
6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: coefficient rings — mod-\(n\) completed group algebra — in class — augmentation

The principal declarations in this module are:

  • modNCompletedGroupAlgebraStageAugmentationInClass

The augmentation on one class-restricted residue-coefficient finite stage.

  • modNCompletedGroupAlgebraStageAugmentationInClass_of

The class-indexed finite-stage \(n\)-modular augmentation sends every group-like basis element to \(1\).

  • modNCompletedGroupAlgebraStageAugmentationInClass_single

The class-indexed finite-stage \(n\)-modular augmentation sends a singleton basis element to its coefficient.

  • modNCompletedGroupAlgebraStageAugmentationInClass_compatible

Class-indexed finite-stage \(n\)-modular augmentations are compatible with group-quotient transition maps.

Imports1
Imported by3

Declarations

def

modNCompletedGroupAlgebraStageAugmentationInClass

L40 ↗
FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass
Documentation

The augmentation on one class-restricted residue-coefficient finite stage.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def modNCompletedGroupAlgebraStageAugmentationInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    ModNCompletedGroupAlgebraStageInClass n G C U →+* ModNCompletedCoeff n
theorem

modNCompletedGroupAlgebraStageAugmentationInClass_of

L53 ↗
FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_of
Documentation

The class-indexed finite-stage \(n\)-modular augmentation sends every group-like basis element to \(1\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageAugmentationInClass_of
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (q : CompletedGroupAlgebraQuotientInClass G C U) :
    modNCompletedGroupAlgebraStageAugmentationInClass n G C U
        (MonoidAlgebra.of (ModNCompletedCoeff n) _ q) = 1
theorem

modNCompletedGroupAlgebraStageAugmentationInClass_single

L72 ↗
FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_single
Documentation

The class-indexed finite-stage \(n\)-modular augmentation sends a singleton basis element to its coefficient.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageAugmentationInClass_single
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (q : CompletedGroupAlgebraQuotientInClass G C U) (a : ModNCompletedCoeff n) :
    modNCompletedGroupAlgebraStageAugmentationInClass n G C U
        (MonoidAlgebra.single q a) = a
theorem

modNCompletedGroupAlgebraStageAugmentationInClass_compatible

L91 ↗
FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_compatible
Documentation

Class-indexed finite-stage \(n\)-modular augmentations are compatible with group-quotient transition maps.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageAugmentationInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
        (modNCompletedGroupAlgebraTransitionInClass n G C hUV) =
      modNCompletedGroupAlgebraStageAugmentationInClass n G C V
theorem

modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageMap

L118 ↗
FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageMap
Documentation

Composing the class-indexed finite-stage \(n\)-modular augmentation with the dense stage map gives the ordinary \(n\)-modular group-algebra augmentation.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageMap
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
        (modNCompletedGroupAlgebraStageMapInClass n G C U) =
      MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
        (1 : G →* ModNCompletedCoeff n)
theorem

modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMap

L147 ↗
FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMap
Documentation

Stage augmentations commute with coefficient reduction on class-restricted finite quotient stages.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMap
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    {m : ℕ} (hnm : n ∣ m) :
    (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
        (modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := n) (m := m) (G := G) C U hnm) =
      (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
        (modNCompletedGroupAlgebraStageAugmentationInClass m G C U)

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