Module

Augmentation.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Augmentation

3 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — coefficient rings — prime-power completed group algebra —

augmentation

The principal declarations in this module are:

primePowerCompletedGroupAlgebraAugmentation

The prime-power completed group algebra carries a canonical augmentation to the corresponding coefficient inverse limit.

primePowerCompletedCoeffProjection_augmentation

Projecting the prime-power completed augmentation to a coefficient stage agrees with the corresponding finite-stage augmentation.

primePowerCompletedGroupAlgebraStageAugmentation_eq_of_same_exponent

Stagewise augmentations of a completed group-algebra element are independent of the finite-quotient component once the prime-power exponent is fixed.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module

Imported by2

def

primePowerCompletedGroupAlgebraAugmentation

L42 ↗

FoxDifferential.primePowerCompletedGroupAlgebraAugmentation

Documentation

The prime-power completed group algebra carries a canonical augmentation to the corresponding coefficient inverse limit.

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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def primePowerCompletedGroupAlgebraAugmentation :
    PrimePowerCompletedGroupAlgebra ℓ G → PrimePowerCompletedCoeff ℓ G

theorem

primePowerCompletedCoeffProjection_augmentation

L74 ↗

FoxDifferential.primePowerCompletedCoeffProjection_augmentation

Documentation

Projecting the prime-power completed augmentation to a coefficient stage agrees with the corresponding finite-stage 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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem primePowerCompletedCoeffProjection_augmentation
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (x : PrimePowerCompletedGroupAlgebra ℓ G) :
    primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x) =
      modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x)

theorem

primePowerCompletedGroupAlgebraStageAugmentation_eq_of_same_exponent

L87 ↗

FoxDifferential.primePowerCompletedGroupAlgebraStageAugmentation_eq_of_same_exponent

Documentation

Stagewise augmentations of a completed group-algebra element are independent of the finite-quotient component once the prime-power exponent is fixed.

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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem primePowerCompletedGroupAlgebraStageAugmentation_eq_of_same_exponent
    (a : ℕ) (U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
    (x : PrimePowerCompletedGroupAlgebra ℓ G) :
    modNCompletedGroupAlgebraStageAugmentation (ℓ ^ a) G U
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) (a, U) x) =
      modNCompletedGroupAlgebraStageAugmentation (ℓ ^ a) G V
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) (a, V) x)

Module documentation

Fox differential: completed — coefficient rings — prime-power completed group algebra —

Declarations

primePowerCompletedGroupAlgebraAugmentation

primePowerCompletedCoeffProjection_augmentation

primePowerCompletedGroupAlgebraStageAugmentation_eq_of_same_exponent