FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection
Fox Differential / Completed / Coefficient Rings / Prime-Power Completed Group Algebra / Within a Class / System / Ring / Projection.
Imported by
- FoxDifferential.Completed
- FoxDifferential.Completed.CoefficientRings
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Augmentation
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Map
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.GroupLike
theorem primePowerCompletedGroupAlgebraProjectionInClass_one
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i
(1 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) = 1The finite-stage projection sends \(1\) to \(1\).
Show proof
by
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 primePowerCompletedGroupAlgebraProjectionInClass_mul
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
(x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x * y) =
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x *
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i yThe finite-stage projection preserves multiplication.
Show proof
by
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 primePowerCompletedGroupAlgebraProjectionInClass_zero
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i
(0 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) = 0The finite-stage projection sends \(0\) to \(0\).
Show proof
by
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 primePowerCompletedGroupAlgebraProjectionInClass_add
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
(x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x + y) =
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x +
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i yThe prime-power finite-stage projection preserves addition.
Show proof
by
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 primePowerCompletedGroupAlgebraProjectionInClass_neg
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
(x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (-x) =
-primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i xThe prime-power finite-stage projection preserves negation.
Show proof
by
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 primePowerCompletedGroupAlgebraProjectionInClass_sub
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
(x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (x - y) =
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x -
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i yThe prime-power finite-stage projection preserves subtraction.
Show proof
by
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 primePowerCompletedGroupAlgebraProjectionInClass_nsmul
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
(m : ℕ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (m • x) =
m • primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i xThe finite-stage projection is compatible with natural-number scalar multiplication.
Show proof
by
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 primePowerCompletedGroupAlgebraProjectionInClass_zsmul
(C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
(m : ℤ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i (m • x) =
m • primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i xThe finite-stage projection is compatible with integer scalar multiplication.
Show proof
by
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.
□