FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection
Fox Differential / Completed / Coefficient Rings / Prime-Power Completed Group Algebra / Coefficient / Projection.
Imported by
- FoxDifferential.Completed
- FoxDifferential.Completed.CoefficientRings
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module
theorem primePowerCompletedCoeffProjection_one
(i : PrimePowerCompletedGroupAlgebraIndex G) :
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
(1 : PrimePowerCompletedCoeff ℓ G) = 1The finite-stage projection sends \(1\) to \(1\).
Show proof
by
change (1 : ZMod (ℓ ^ i.1)) = 1
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 primePowerCompletedCoeffProjection_mul
(i : PrimePowerCompletedGroupAlgebraIndex G)
(x y : PrimePowerCompletedCoeff ℓ G) :
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (x * y) =
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x *
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i yThe finite-stage projection preserves multiplication.
Show proof
by
change (show ZMod (ℓ ^ i.1) from (x * y).1 i) =
(show ZMod (ℓ ^ i.1) from x.1 i) * (show ZMod (ℓ ^ i.1) from y.1 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 primePowerCompletedCoeffProjection_natCast
(i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℕ) :
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
(n : PrimePowerCompletedCoeff ℓ G) = nThe finite-stage projection preserves natural number casts.
Show proof
by
change (n : ZMod (ℓ ^ i.1)) = n
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 primePowerCompletedCoeffProjection_intCast
(i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℤ) :
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
(n : PrimePowerCompletedCoeff ℓ G) = nThe finite-stage projection preserves integer casts.
Show proof
by
change (n : ZMod (ℓ ^ i.1)) = n
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 primePowerCompletedCoeffProjection_zero
(i : PrimePowerCompletedGroupAlgebraIndex G) :
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
(0 : PrimePowerCompletedCoeff ℓ G) = 0The finite-stage projection sends \(0\) to \(0\).
Show proof
by
change (0 : ZMod (ℓ ^ i.1)) = 0
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 primePowerCompletedCoeffProjection_add
(i : PrimePowerCompletedGroupAlgebraIndex G)
(x y : PrimePowerCompletedCoeff ℓ G) :
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (x + y) =
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x +
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i yThe finite-stage projection evaluates a completed element by reading the corresponding inverse-limit coordinate.
Show proof
by
change (show ZMod (ℓ ^ i.1) from (x + y).1 i) =
(show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 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 primePowerCompletedCoeffProjection_neg
(i : PrimePowerCompletedGroupAlgebraIndex G)
(x : PrimePowerCompletedCoeff ℓ G) :
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (-x) =
-primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i xThe finite-stage projection evaluates a completed element by reading the corresponding inverse-limit coordinate.
Show proof
by
change (show ZMod (ℓ ^ i.1) from (-x).1 i) =
-(show ZMod (ℓ ^ i.1) from x.1 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 primePowerCompletedCoeffProjection_sub
(i : PrimePowerCompletedGroupAlgebraIndex G)
(x y : PrimePowerCompletedCoeff ℓ G) :
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (x - y) =
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x -
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i yThe finite-stage projection evaluates a completed element by reading the corresponding inverse-limit coordinate.
Show proof
by
change (show ZMod (ℓ ^ i.1) from (x - y).1 i) =
(show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 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 primePowerCompletedCoeffProjection_eq_of_same_exponent
(a : ℕ) (U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
(z : PrimePowerCompletedCoeff ℓ G) :
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, U) z =
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, V) zShow proof
by
let T : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G := _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G
let hTU : (a, T) ≤ (a, U) :=
⟨le_rfl, _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex_le (G := G) U⟩
let hTV : (a, T) ≤ (a, V) :=
⟨le_rfl, _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex_le (G := G) V⟩
have hTU_coeff :
modNCompletedCoeffMap
(n := ℓ ^ a) (m := ℓ ^ a)
(primePow_dvd_primePow (ℓ := ℓ) hTU.1) = RingHom.id _ := by
have hproof :
primePow_dvd_primePow (ℓ := ℓ) hTU.1 = (dvd_rfl : ℓ ^ a ∣ ℓ ^ a) :=
Subsingleton.elim _ _
rw [hproof]
exact modNCompletedCoeffMap_rfl (n := ℓ ^ a)
have hTV_coeff :
modNCompletedCoeffMap
(n := ℓ ^ a) (m := ℓ ^ a)
(primePow_dvd_primePow (ℓ := ℓ) hTV.1) = RingHom.id _ := by
have hproof :
primePow_dvd_primePow (ℓ := ℓ) hTV.1 = (dvd_rfl : ℓ ^ a ∣ ℓ ^ a) :=
Subsingleton.elim _ _
rw [hproof]
exact modNCompletedCoeffMap_rfl (n := ℓ ^ a)
have hU := z.2 (a, T) (a, U) hTU
have hV := z.2 (a, T) (a, V) hTV
have hU' :
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, U) z =
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, T) z := by
simpa [primePowerCompletedCoeffProjection, primePowerCompletedCoeffSystem, hTU_coeff] using
hU
have hV' :
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, V) z =
primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, T) z := by
simpa [primePowerCompletedCoeffProjection, primePowerCompletedCoeffSystem, hTV_coeff] using
hV
exact hU'.trans hV'.symmProof. 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.
□