FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup

6 Theorem | 10 Instance

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

Open this file on GitHub

import

FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.System

Imported by

Instance FoxDifferential.instZeroPrimePowerCompletedCoeff GitHub

instance instZeroPrimePowerCompletedCoeff : Zero (PrimePowerCompletedCoeff ℓ G) where
  zero := ⟨fun i => (0 : ZMod (ℓ ^ i.1)), by
    intro i j hij
    letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
    letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
    exact map_zero
      (modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1))⟩

The zero element of the prime-power completed coefficient ring is the compatible family of finite-stage zero elements.

Instance FoxDifferential.instAddPrimePowerCompletedCoeff GitHub

instance instAddPrimePowerCompletedCoeff : Add (PrimePowerCompletedCoeff ℓ G) where
  add x y := ⟨fun i =>
      (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i), by
    intro i j hij
    letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
    letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        ((show ZMod (ℓ ^ j.1) from x.1 j) + (show ZMod (ℓ ^ j.1) from y.1 j)) =
      (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i)
    rw [map_add]
    exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩

Addition in the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient additions.

Instance FoxDifferential.instAddZeroClassPrimePowerCompletedCoeff GitHub

instance instAddZeroClassPrimePowerCompletedCoeff :
    AddZeroClass (PrimePowerCompletedCoeff ℓ G) where
  zero := 0
  add := (· + ·)
  zero_add x := by
    apply Subtype.ext
    funext i
    change (0 : ZMod (ℓ ^ i.1)) + (show ZMod (ℓ ^ i.1) from x.1 i) =
      (show ZMod (ℓ ^ i.1) from x.1 i)
    simp only [zero_add]
  add_zero x := by
    apply Subtype.ext
    funext i
    change (show ZMod (ℓ ^ i.1) from x.1 i) + (0 : ZMod (ℓ ^ i.1)) =
      (show ZMod (ℓ ^ i.1) from x.1 i)
    simp only [add_zero]

Addition in the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient additions.

Instance FoxDifferential.instNegPrimePowerCompletedCoeff GitHub

instance instNegPrimePowerCompletedCoeff : Neg (PrimePowerCompletedCoeff ℓ G) where
  neg x := ⟨fun i => -(show ZMod (ℓ ^ i.1) from x.1 i), by
    intro i j hij
    letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
    letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        (-(show ZMod (ℓ ^ j.1) from x.1 j)) =
      -(show ZMod (ℓ ^ i.1) from x.1 i)
    rw [map_neg]
    exact congrArg Neg.neg (x.2 i j hij)⟩

Negation on the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient negations.

Instance FoxDifferential.instSubPrimePowerCompletedCoeff GitHub

instance instSubPrimePowerCompletedCoeff : Sub (PrimePowerCompletedCoeff ℓ G) where
  sub x y := ⟨fun i =>
      (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i), by
    intro i j hij
    letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
    letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        ((show ZMod (ℓ ^ j.1) from x.1 j) - (show ZMod (ℓ ^ j.1) from y.1 j)) =
      (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i)
    rw [map_sub]
    exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩

Subtraction in the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient-ring subtractions.

Instance FoxDifferential.instSMulNatPrimePowerCompletedCoeff GitHub

instance instSMulNatPrimePowerCompletedCoeff : SMul ℕ (PrimePowerCompletedCoeff ℓ G) where
  smul m x := ⟨fun i => m • (show ZMod (ℓ ^ i.1) from x.1 i), by
    intro i j hij
    letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
    letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        (m • (show ZMod (ℓ ^ j.1) from x.1 j)) =
      m • (show ZMod (ℓ ^ i.1) from x.1 i)
    rw [map_nsmul]
    exact congrArg (m • ·) (x.2 i j hij)⟩

The prime-power completed coefficient ring carries natural-number scalar multiplication coordinatewise at every finite coefficient stage.

Instance FoxDifferential.instSMulIntPrimePowerCompletedCoeff GitHub

instance instSMulIntPrimePowerCompletedCoeff : SMul ℤ (PrimePowerCompletedCoeff ℓ G) where
  smul m x := ⟨fun i => m • (show ZMod (ℓ ^ i.1) from x.1 i), by
    intro i j hij
    letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
    letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        (m • (show ZMod (ℓ ^ j.1) from x.1 j)) =
      m • (show ZMod (ℓ ^ i.1) from x.1 i)
    rw [map_zsmul]
    exact congrArg (m • ·) (x.2 i j hij)⟩

The prime-power completed coefficient ring carries integer scalar multiplication coordinatewise at every finite coefficient stage.

Instance FoxDifferential.instAddCommGroupPrimePowerCompletedCoeffStage GitHub

instance instAddCommGroupPrimePowerCompletedCoeffStage
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    AddCommGroup ((primePowerCompletedCoeffSystem ℓ G).X i) := by
  dsimp [primePowerCompletedCoeffSystem]
  infer_instance

Addition in the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient additions.

Instance FoxDifferential.instAddCommGroupPrimePowerCompletedCoeffFamily GitHub

instance instAddCommGroupPrimePowerCompletedCoeffFamily :
    AddCommGroup
      ((i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) :=
  inferInstance

Addition in the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient additions.

Theorem FoxDifferential.coe_zero_primePowerCompletedCoeff GitHub

theorem coe_zero_primePowerCompletedCoeff :
    ((0 : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) = 0

The inclusion of the prime-power completed coefficient ring preserves zero.

Show proof

Theorem FoxDifferential.coe_add_primePowerCompletedCoeff GitHub

theorem coe_add_primePowerCompletedCoeff
    (x y : PrimePowerCompletedCoeff ℓ G) :
    ((x + y : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) = x + y

The inclusion of the prime-power completed coefficient ring preserves addition.

Show proof

Theorem FoxDifferential.coe_neg_primePowerCompletedCoeff GitHub

theorem coe_neg_primePowerCompletedCoeff
    (x : PrimePowerCompletedCoeff ℓ G) :
    ((-x : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) = -x

The inclusion of the prime-power completed coefficient ring preserves negation.

Show proof

Theorem FoxDifferential.coe_sub_primePowerCompletedCoeff GitHub

theorem coe_sub_primePowerCompletedCoeff
    (x y : PrimePowerCompletedCoeff ℓ G) :
    ((x - y : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) = x - y

The inclusion of the prime-power completed coefficient ring preserves subtraction.

Show proof

Theorem FoxDifferential.coe_nsmul_primePowerCompletedCoeff GitHub

theorem coe_nsmul_primePowerCompletedCoeff
    (m : ℕ) (x : PrimePowerCompletedCoeff ℓ G) :
    ((m • x : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) = m • x

The inclusion of the prime-power completed coefficient ring preserves natural-number scalar multiplication.

Show proof

Theorem FoxDifferential.coe_zsmul_primePowerCompletedCoeff GitHub

theorem coe_zsmul_primePowerCompletedCoeff
    (m : ℤ) (x : PrimePowerCompletedCoeff ℓ G) :
    ((m • x : PrimePowerCompletedCoeff ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) = m • x

The inclusion of the prime-power completed coefficient ring preserves integer scalar multiplication.

Show proof

Instance FoxDifferential.instAddCommGroupPrimePowerCompletedCoeff GitHub

instance instAddCommGroupPrimePowerCompletedCoeff :
    AddCommGroup (PrimePowerCompletedCoeff ℓ G) :=
  Function.Injective.addCommGroup
    (fun x : PrimePowerCompletedCoeff ℓ G =>
      (x :
        (i : PrimePowerCompletedGroupAlgebraIndex G) →
          (primePowerCompletedCoeffSystem ℓ G).X i))
    Subtype.val_injective
    (coe_zero_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
    (coe_add_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
    (coe_neg_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
    (coe_sub_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
    (fun x m => coe_nsmul_primePowerCompletedCoeff (ℓ := ℓ) (G := G) m x)
    (fun x m => coe_zsmul_primePowerCompletedCoeff (ℓ := ℓ) (G := G) m x)

Addition in the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient additions.

FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup

Declarations