FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Projection
Fox Differential / Completed / Coefficient Rings / Prime-Power Completed Group Algebra / System / Ring / Projection.
import
Imported by
- FoxDifferential.Completed
- FoxDifferential.Completed.CoefficientRings
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.System
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring
theorem primePowerCompletedGroupAlgebraProjection_natCast
(i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℕ) :
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
(n : PrimePowerCompletedGroupAlgebra ℓ G) = nThe finite-stage projection preserves natural number casts.
Show proof
by
change (n : PrimePowerCompletedGroupAlgebraStage ℓ G i) = n
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem primePowerCompletedGroupAlgebraProjection_intCast
(i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℤ) :
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
(n : PrimePowerCompletedGroupAlgebra ℓ G) = nThe finite-stage projection preserves integer casts.
Show proof
by
change (n : PrimePowerCompletedGroupAlgebraStage ℓ G i) = n
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem primePowerCompletedGroupAlgebraProjection_zero
(i : PrimePowerCompletedGroupAlgebraIndex G) :
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
(0 : PrimePowerCompletedGroupAlgebra ℓ G) = 0The finite-stage projection sends \(0\) to \(0\).
Show proof
by
change (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) = 0
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem primePowerCompletedGroupAlgebraProjection_add
(i : PrimePowerCompletedGroupAlgebraIndex G)
(x y : PrimePowerCompletedGroupAlgebra ℓ G) :
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x + y) =
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x +
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i yThe prime-power finite-stage projection preserves addition.
Show proof
by
change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from (x + y).1 i) =
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i)
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem primePowerCompletedGroupAlgebraProjection_neg
(i : PrimePowerCompletedGroupAlgebraIndex G)
(x : PrimePowerCompletedGroupAlgebra ℓ G) :
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (-x) =
-primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i xThe prime-power finite-stage projection preserves negation.
Show proof
by
change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from (-x).1 i) =
-(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem primePowerCompletedGroupAlgebraProjection_sub
(i : PrimePowerCompletedGroupAlgebraIndex G)
(x y : PrimePowerCompletedGroupAlgebra ℓ G) :
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x - y) =
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x -
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i yThe prime-power finite-stage projection preserves subtraction.
Show proof
by
change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from (x - y).1 i) =
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) -
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i)
rflProof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□theorem primePowerCompletedGroupAlgebraStageAugmentation_comp_transition
{i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
(modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2).comp
(primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij) =
(modNCompletedCoeffMap
(n := ℓ ^ i.1) (m := ℓ ^ j.1)
(primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
(modNCompletedGroupAlgebraStageAugmentation (ℓ ^ j.1) G j.2)Finite-stage prime-power augmentation is compatible with transition maps and coefficient reduction.
Show proof
by
rw [primePowerCompletedGroupAlgebraTransition_eq]
rw [← RingHom.comp_assoc]
rw [modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap]
rw [RingHom.comp_assoc]
rw [modNCompletedGroupAlgebraStageAugmentation_compatible]Proof. Unfold the prime-power completed group algebra as the inverse limit over prime-power coefficient stages and finite group quotients. Projections, transition maps, augmentation, multiplication, scalar actions, and coefficient reduction are computed coordinatewise at finite group-algebra stages. The formulas are checked on singleton group-like basis elements and then extended by finite support and linearity; inverse-limit extensionality and transition compatibility assemble the completed statements.
□