FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Ring
Fox Differential / Completed / Coefficient Rings / Prime-Power Completed Group Algebra / Coefficient / Ring.
Imported by
- FoxDifferential.Completed
- FoxDifferential.Completed.CoefficientRings
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection
instance instOnePrimePowerCompletedCoeff : One (PrimePowerCompletedCoeff ℓ G) where
one := ⟨fun i => (1 : 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_one
(modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1))⟩The unit of the prime-power completed coefficient ring is the compatible family of finite-stage units.
instance instMulPrimePowerCompletedCoeff : Mul (PrimePowerCompletedCoeff ℓ G) where
mul 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_mul]
exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩Multiplication on the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient rings.
instance instNatCastPrimePowerCompletedCoeff : NatCast (PrimePowerCompletedCoeff ℓ G) where
natCast n := ⟨fun i => (n : 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_natCast
(modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1)) n⟩Natural number casts in the prime-power completed coefficient ring are computed coordinatewise from finite-stage natural number casts.
instance instIntCastPrimePowerCompletedCoeff : IntCast (PrimePowerCompletedCoeff ℓ G) where
intCast n := ⟨fun i => (n : 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_intCast
(modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1)) n⟩Integer casts in the prime-power completed coefficient ring are computed coordinatewise from finite-stage integer casts.
instance instCommRingPrimePowerCompletedCoeffStage
(i : PrimePowerCompletedGroupAlgebraIndex G) :
CommRing ((primePowerCompletedCoeffSystem ℓ G).X i) := by
dsimp [primePowerCompletedCoeffSystem]
infer_instanceEach finite prime-power coefficient stage is a commutative ring.
instance instCommRingPrimePowerCompletedCoeffFamily :
CommRing
((i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedCoeffSystem ℓ G).X i) :=
inferInstanceThe family-level prime-power completed coefficient object is a commutative ring with operations computed coordinatewise.
instance instPowPrimePowerCompletedCoeff : Pow (PrimePowerCompletedCoeff ℓ G) ℕ where
pow x n := ⟨fun i => (show ZMod (ℓ ^ i.1) from x.1 i) ^ n, 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) ^ n) =
(show ZMod (ℓ ^ i.1) from x.1 i) ^ n
rw [map_pow]
exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩Powers in the prime-power completed coefficient ring are computed at every finite coefficient stage.
theorem coe_one_primePowerCompletedCoeff :
((1 : PrimePowerCompletedCoeff ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedCoeffSystem ℓ G).X i) =
(1 :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedCoeffSystem ℓ G).X i)The multiplicative identity in the prime-power completed coefficient ring is computed coordinatewise.
Show proof
by
funext i
rflProof. Unfold the prime-power completed coefficient ring as the inverse limit over its finite prime-power coefficient stages. Projections, transition maps, arithmetic operations, scalar actions, and coefficient reductions are computed coordinatewise. The finite-stage identities are the corresponding identities in the coefficient rings, and inverse-limit extensionality together with transition compatibility assembles the completed statements.
□theorem coe_mul_primePowerCompletedCoeff
(x y : PrimePowerCompletedCoeff ℓ G) :
((x * y : PrimePowerCompletedCoeff ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedCoeffSystem ℓ G).X i) =
(x * y :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedCoeffSystem ℓ G).X i)Multiplication in the prime-power completed coefficient ring is computed coordinatewise.
Show proof
by
funext i
rflProof. Unfold the prime-power completed coefficient ring as the inverse limit over its finite prime-power coefficient stages. Projections, transition maps, arithmetic operations, scalar actions, and coefficient reductions are computed coordinatewise. The finite-stage identities are the corresponding identities in the coefficient rings, and inverse-limit extensionality together with transition compatibility assembles the completed statements.
□theorem coe_natCast_primePowerCompletedCoeff
(n : ℕ) :
((n : PrimePowerCompletedCoeff ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedCoeffSystem ℓ G).X i) =
(n :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedCoeffSystem ℓ G).X i)Natural number casts in the prime-power completed coefficient ring are computed coordinatewise.
Show proof
by
funext i
rflProof. Unfold the prime-power completed coefficient ring as the inverse limit over its finite prime-power coefficient stages. Projections, transition maps, arithmetic operations, scalar actions, and coefficient reductions are computed coordinatewise. The finite-stage identities are the corresponding identities in the coefficient rings, and inverse-limit extensionality together with transition compatibility assembles the completed statements.
□theorem coe_intCast_primePowerCompletedCoeff
(n : ℤ) :
((n : PrimePowerCompletedCoeff ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedCoeffSystem ℓ G).X i) =
(n :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedCoeffSystem ℓ G).X i)Integer casts in the prime-power completed coefficient ring are computed coordinatewise.
Show proof
by
funext i
rflProof. Unfold the prime-power completed coefficient ring as the inverse limit over its finite prime-power coefficient stages. Projections, transition maps, arithmetic operations, scalar actions, and coefficient reductions are computed coordinatewise. The finite-stage identities are the corresponding identities in the coefficient rings, and inverse-limit extensionality together with transition compatibility assembles the completed statements.
□theorem coe_pow_primePowerCompletedCoeff
(x : PrimePowerCompletedCoeff ℓ G) (n : ℕ) :
((x ^ n : PrimePowerCompletedCoeff ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedCoeffSystem ℓ G).X i) =
(x ^ n :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedCoeffSystem ℓ G).X i)Powers in the prime-power completed coefficient ring are computed coordinatewise.
Show proof
by
funext i
rflProof. Unfold the prime-power completed coefficient ring as the inverse limit over its finite prime-power coefficient stages. Projections, transition maps, arithmetic operations, scalar actions, and coefficient reductions are computed coordinatewise. The finite-stage identities are the corresponding identities in the coefficient rings, and inverse-limit extensionality together with transition compatibility assembles the completed statements.
□instance instCommRingPrimePowerCompletedCoeff :
CommRing (PrimePowerCompletedCoeff ℓ G) :=
Function.Injective.commRing
(fun x : PrimePowerCompletedCoeff ℓ G =>
(x :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedCoeffSystem ℓ G).X i))
Subtype.val_injective
(coe_zero_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
(coe_one_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
(coe_add_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
(coe_mul_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
(coe_neg_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
(coe_sub_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
(fun n x => coe_nsmul_primePowerCompletedCoeff (ℓ := ℓ) (G := G) n x)
(fun n x => coe_zsmul_primePowerCompletedCoeff (ℓ := ℓ) (G := G) n x)
(fun x n => coe_pow_primePowerCompletedCoeff (ℓ := ℓ) (G := G) x n)
(by
intro n
exact coe_natCast_primePowerCompletedCoeff (ℓ := ℓ) (G := G) n)
(by
intro z
exact coe_intCast_primePowerCompletedCoeff (ℓ := ℓ) (G := G) z)The prime-power completed coefficient object is a commutative ring with operations computed coordinatewise.