FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Augmentation

2 Theorem | 1 Definition

Fox Differential / Completed / Coefficient Rings / Prime-Power Completed Group Algebra / Augmentation.

import

FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module

Imported by

Definition FoxDifferential.primePowerCompletedGroupAlgebraAugmentation GitHub

def primePowerCompletedGroupAlgebraAugmentation :
    PrimePowerCompletedGroupAlgebra ℓ G → PrimePowerCompletedCoeff ℓ G := by
  intro x
  refine ⟨fun i => ?_, ?_⟩
  · letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
    exact modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2 (x.1 i)
  · intro i j hij
    letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
    letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
    calc
      modNCompletedCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1)
          (primePow_dvd_primePow (ℓ := ℓ) hij.1)
          (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ j.1) G j.2 (x.1 j))
        =
      modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
        (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij (x.1 j)) := by
          symm
          exact congrFun
            (congrArg DFunLike.coe
              (primePowerCompletedGroupAlgebraStageAugmentation_comp_transition
                (ℓ := ℓ) (G := G) hij)) (x.1 j)
      _ =
      modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2 (x.1 i) := by
          have hx :
              primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij (x.1 j) = x.1 i :=
            x.2 i j hij
          exact congrArg (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2) hx

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

Theorem FoxDifferential.primePowerCompletedCoeffProjection_augmentation GitHub

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)

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

Show proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraStageAugmentation_eq_of_same_exponent GitHub

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)

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

Show proof

FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Augmentation

Declarations