FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.AddCommGroup
Fox Differential / Completed / Coefficient Rings / Prime-Power Completed Group Algebra / Within a Class / System / Ring / Additive Commutative Group.
import
Imported by
- FoxDifferential.Completed
- FoxDifferential.Completed.CoefficientRings
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Multiplicative
instance instZeroPrimePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
Zero (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
zero := ⟨fun i => (0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
(0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) = 0
exact map_zero _⟩The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.
instance instAddPrimePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
Add (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
add x y := ⟨fun i =>
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) +
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i), by
intro i j hij
calc
primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
((show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) +
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j))
=
primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) +
primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j) := by
rw [map_add]
_ =
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) +
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i) := by
exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩Addition in the prime-power completed group algebra is defined coordinatewise through finite-stage group-algebra additions.
instance instAddZeroClassPrimePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
AddZeroClass (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
zero := 0
add := (· + ·)
zero_add x := by
apply Subtype.ext
funext i
change (0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) +
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) =
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
simp only [zero_add]
add_zero x := by
apply Subtype.ext
funext i
change (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) +
(0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
simp only [add_zero]Addition in the prime-power completed group algebra is defined coordinatewise through finite-stage group-algebra additions.
instance instNegPrimePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
Neg (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
neg x := ⟨fun i => -(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
(-(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j)) =
-(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
rw [map_neg]
exact congrArg Neg.neg (x.2 i j hij)⟩Negation on the \(C\)-indexed prime-power completed group algebra is defined coordinatewise through finite-stage group-algebra negations.
instance instSubPrimePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
Sub (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
sub x y := ⟨fun i =>
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) -
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
((show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) -
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j)) =
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) -
(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i)
rw [map_sub]
exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩Subtraction on the completed group algebra is defined coordinatewise through the finite-stage group-algebra subtractions.
instance instSMulNatPrimePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
SMul ℕ (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
smul m x := ⟨fun i =>
m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
(m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j)) =
m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
rw [map_nsmul]
exact congrArg (m • ·) (x.2 i j hij)⟩The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.
instance instSMulIntPrimePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
SMul ℤ (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
smul m x := ⟨fun i =>
m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
(m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j)) =
m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
rw [map_zsmul]
exact congrArg (m • ·) (x.2 i j hij)⟩The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.
theorem coe_zero_primePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
((0 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
(i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = 0The inclusion of the class-indexed prime-power completed group algebra preserves zero.
Show proof
by
funext 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 coe_add_primePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u})
(x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
((x + y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
(i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = x + yThe inclusion of the class-indexed prime-power completed group algebra preserves addition.
Show proof
by
funext 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 coe_neg_primePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u})
(x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
((-x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
(i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = -xThe inclusion of the class-indexed prime-power completed group algebra preserves negation.
Show proof
by
funext 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 coe_sub_primePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u})
(x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
((x - y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
(i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = x - ySubtraction in the \(C\)-indexed prime-power completed group algebra is computed coordinatewise.
Show proof
by
funext 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 coe_nsmul_primePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u})
(m : ℕ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
((m • x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
(i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = m • xThe inclusion of the class-indexed prime-power completed group algebra preserves natural-number scalar multiplication.
Show proof
by
funext 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 coe_zsmul_primePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u})
(m : ℤ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
((m • x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
(i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = m • xThe inclusion of the class-indexed prime-power completed group algebra preserves integer scalar multiplication.
Show proof
by
funext 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.
□instance instAddCommGroupPrimePowerCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
AddCommGroup (PrimePowerCompletedGroupAlgebraInClass ℓ G C) :=
Function.Injective.addCommGroup
(fun x : PrimePowerCompletedGroupAlgebraInClass ℓ G C =>
(x :
(i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i))
Subtype.val_injective
(coe_zero_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
(coe_add_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
(coe_neg_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
(coe_sub_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
(fun x m => coe_nsmul_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C m x)
(fun x m => coe_zsmul_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C m x)Addition in the prime-power completed group algebra is defined coordinatewise through finite-stage group-algebra additions.