Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup
ProCGroups/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Coeff/AddCommGroup

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup

6 Theorems | 3 Definitions | 7 Instances

The principal declarations in this module are:

  • instAddCommGroupPrimePowerCompletedCoeffStage Each coefficient stage \(\mathbb{Z}/\ell^i\mathbb{Z}\) carries its standard additive group. - instAddCommGroupPrimePowerCompletedCoeffFamily The dependent family of prime-power coefficient stages carries the pointwise additive commutative group structure. - coe_zero_primePowerCompletedCoeff The inclusion of the prime-power completed coefficient ring preserves zero. - coe_add_primePowerCompletedCoeff The inclusion of the prime-power completed coefficient ring preserves addition.
import
Imported by

Declarations

Instance FoxDifferential.instZeroPrimePowerCompletedCoeff 
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 
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 
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]

Coordinatewise zero and addition on the prime-power completed coefficient ring satisfy the left and right zero laws.

Instance FoxDifferential.instNegPrimePowerCompletedCoeff 
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 
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 
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 
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.

Definition FoxDifferential.instAddCommGroupPrimePowerCompletedCoeffStage 
@[reducible] def instAddCommGroupPrimePowerCompletedCoeffStage
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    AddCommGroup ((primePowerCompletedCoeffSystem ℓ G).X i) := by
  dsimp [primePowerCompletedCoeffSystem]
  infer_instance

Each coefficient stage \(\mathbb{Z}/\ell^i\mathbb{Z}\) carries its standard additive group.

Definition FoxDifferential.instAddCommGroupPrimePowerCompletedCoeffFamily 
@[reducible] def instAddCommGroupPrimePowerCompletedCoeffFamily :
    AddCommGroup
      ((i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedCoeffSystem ℓ G).X i) :=
  inferInstance

The dependent family of prime-power coefficient stages carries the pointwise additive commutative group structure.

Theorem FoxDifferential.coe_zero_primePowerCompletedCoeff 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
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 Lean proof
Theorem FoxDifferential.coe_add_primePowerCompletedCoeff 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
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 Lean proof
Theorem FoxDifferential.coe_neg_primePowerCompletedCoeff 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
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 Lean proof
Theorem FoxDifferential.coe_sub_primePowerCompletedCoeff 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
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 Lean proof
Theorem FoxDifferential.coe_nsmul_primePowerCompletedCoeff 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
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 Lean proof
Theorem FoxDifferential.coe_zsmul_primePowerCompletedCoeff 
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
@[simp]
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 Lean proof
Definition FoxDifferential.instAddCommGroupPrimePowerCompletedCoeff 
@[reducible] def 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)

The prime-power completed coefficient ring inherits an additive commutative group structure from its injective inclusion into the family of coefficient stages.