FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Module

2 Theorem | 5 Instance

Fox Differential / Completed / Coefficient Rings / Prime-Power Augmentation Ideal / Module.

import

FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Additive

Imported by

Theorem FoxDifferential.primePowerCompletedGroupAlgebraStageAugmentationIdealTransition_smul GitHub

theorem primePowerCompletedGroupAlgebraStageAugmentationIdealTransition_smul
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
    (a : ZMod (ℓ ^ j.1))
    (x : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) :
    primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
        (ℓ := ℓ) (G := G) hij (a • x) =
      (modNCompletedCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1)
          (primePow_dvd_primePow (ℓ := ℓ) hij.1) a) •
        primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
          (ℓ := ℓ) (G := G) hij x

The transition map between finite-stage augmentation ideals is compatible with scalar multiplication.

Show proof

Instance FoxDifferential.instCommRingPrimePowerCompletedCoeffAugmentationIdealLocal GitHub

instance instCommRingPrimePowerCompletedCoeffAugmentationIdealLocal :
    CommRing (PrimePowerCompletedCoeff ℓ G) := by
  infer_instance

The constructed object has powers computed at every finite-stage coordinate.

Instance FoxDifferential.instSMulPrimePowerCompletedCoeffPrimePowerCompletedGAAugmentationIdealFamily GitHub

instance instSMulPrimePowerCompletedCoeffPrimePowerCompletedGAAugmentationIdealFamily :
    SMul (PrimePowerCompletedCoeff ℓ G)
      ((i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) where
  smul a x := fun i =>
    (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
      (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x i)

The family-level prime-power completed group-algebra augmentation ideal carries scalar multiplication by the prime-power completed coefficient ring.

Instance FoxDifferential.instModulePpCoeffPpGAAugIdealFamily GitHub

instance instModulePpCoeffPpGAAugIdealFamily :
    Module (PrimePowerCompletedCoeff ℓ G)
      ((i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) where
  one_smul x := by
    funext i
    change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (1 : PrimePowerCompletedCoeff ℓ G)) •
        (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
          (ℓ := ℓ) (G := G) i from x i) =
      (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
        (ℓ := ℓ) (G := G) i from x i)
    rw [primePowerCompletedCoeffProjection_one, one_smul]
  mul_smul a b x := by
    funext i
    change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a * b)) •
        (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
          (ℓ := ℓ) (G := G) i from x i) =
      (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        ((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
          (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
            (ℓ := ℓ) (G := G) i from x i))
    rw [primePowerCompletedCoeffProjection_mul, mul_smul]
  smul_zero a := by
    funext i
    change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        (0 : primePowerCompletedGroupAlgebraStageAugmentationIdeal
          (ℓ := ℓ) (G := G) i) = 0
    rw [smul_zero]
  smul_add a x y := by
    funext i
    change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal
          (ℓ := ℓ) (G := G) i from x i) +
          (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
            (ℓ := ℓ) (G := G) i from y i)) =
      (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
          (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
            (ℓ := ℓ) (G := G) i from x i) +
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
          (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
            (ℓ := ℓ) (G := G) i from y i)
    rw [smul_add]
  add_smul a b x := by
    funext i
    change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a + b)) •
        (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
          (ℓ := ℓ) (G := G) i from x i) =
      (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
          (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
            (ℓ := ℓ) (G := G) i from x i) +
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
          (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
            (ℓ := ℓ) (G := G) i from x i)
    rw [primePowerCompletedCoeffProjection_add, add_smul]
  zero_smul x := by
    funext i
    change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (0 : PrimePowerCompletedCoeff ℓ G)) •
        (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
          (ℓ := ℓ) (G := G) i from x i) = 0
    rw [primePowerCompletedCoeffProjection_zero, zero_smul]

The prime-power completed augmentation-ideal family is a module over the completed coefficient ring.

Instance FoxDifferential.instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraAugmentationIdeal GitHub

instance instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraAugmentationIdeal :
    SMul (PrimePowerCompletedCoeff ℓ G)
      (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
  smul a x := ⟨fun i =>
      (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
          (ℓ := ℓ) (G := G) i from x.1 i), by
    intro i j hij
    calc
      primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
          (ℓ := ℓ) (G := G) hij
          ((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a) •
            (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
              from x.1 j)) =
      (modNCompletedCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1)
          (primePow_dvd_primePow (ℓ := ℓ) hij.1)
          (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)) •
        primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
          (ℓ := ℓ) (G := G) hij
          (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
            from x.1 j) := by
            exact
              primePowerCompletedGroupAlgebraStageAugmentationIdealTransition_smul
                (ℓ := ℓ) (G := G) hij
                (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)
                (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
                  (ℓ := ℓ) (G := G) j from x.1 j)
      _ =
      (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        (show primePowerCompletedGroupAlgebraStageAugmentationIdeal
          (ℓ := ℓ) (G := G) i from x.1 i) := by
            exact congrArg₂ HSMul.hSMul (a.2 i j hij) (x.2 i j hij)⟩

The prime-power completed group-algebra augmentation ideal carries scalar multiplication by the prime-power completed coefficient ring.

Theorem FoxDifferential.coe_smul_primePowerCompletedGroupAlgebraAugmentationIdeal GitHub

theorem coe_smul_primePowerCompletedGroupAlgebraAugmentationIdeal
    (a : PrimePowerCompletedCoeff ℓ G)
    (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
    letI

The inclusion of the completed augmentation ideal preserves scalar multiplication.

Show proof

Instance FoxDifferential.instModulePpCoeffPpGAAugIdeal GitHub

instance instModulePpCoeffPpGAAugIdeal :
    Module (PrimePowerCompletedCoeff ℓ G)
      (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :=
  Function.Injective.module (PrimePowerCompletedCoeff ℓ G)
    { toFun := Subtype.val
      map_zero' := rfl
      map_add' := fun _ _ => rfl }
    Subtype.val_injective
    (coe_smul_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))

The prime-power completed augmentation ideal is a module over the completed coefficient ring.

FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Module

Declarations