ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Augmentation

2 Theorems | 1 Definition

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.

import

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module

Imported by

Definition FoxDifferential.primePowerCompletedGroupAlgebraAugmentation

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

omit [Fact (0 < ℓ)] in
@[simp]
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 Lean proof

Theorem FoxDifferential.primePowerCompletedGroupAlgebraStageAugmentation_eq_of_same_exponent

omit [Fact (0 < ℓ)] in
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 Lean proof

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Augmentation

Declarations