FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.AddCommGroup
Fox Differential / Completed / Coefficient Rings / Prime-Power Completed Group Algebra / System / Ring / Additive Commutative Group.
Imported by
- FoxDifferential.Completed
- FoxDifferential.Completed.CoefficientRings
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Multiplicative
instance instZeroPrimePowerCompletedGroupAlgebra : Zero (PrimePowerCompletedGroupAlgebra ℓ G) where
zero := ⟨fun i => (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(0 : PrimePowerCompletedGroupAlgebraStage ℓ G j) = 0
exact map_zero _⟩The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.
instance instAddPrimePowerCompletedGroupAlgebra : Add (PrimePowerCompletedGroupAlgebra ℓ G) where
add x y := ⟨fun i =>
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i), by
intro i j hij
calc
primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) +
(show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j))
=
primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) +
primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j) := by
rw [map_add]
_ =
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +
(show PrimePowerCompletedGroupAlgebraStage ℓ G 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 instAddZeroClassPrimePowerCompletedGroupAlgebra :
AddZeroClass (PrimePowerCompletedGroupAlgebra ℓ G) where
zero := 0
add := (· + ·)
zero_add x := by
apply Subtype.ext
funext i
change (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) +
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) =
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
simp only [zero_add]
add_zero x := by
apply Subtype.ext
funext i
change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +
(0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) =
(show PrimePowerCompletedGroupAlgebraStage ℓ G 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 instNegPrimePowerCompletedGroupAlgebra : Neg (PrimePowerCompletedGroupAlgebra ℓ G) where
neg x := ⟨fun i => -(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(-(show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
-(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
rw [map_neg]
exact congrArg Neg.neg (x.2 i j hij)⟩Negation on the prime-power completed group algebra is defined coordinatewise through finite-stage group-algebra negations.
instance instSubPrimePowerCompletedGroupAlgebra : Sub (PrimePowerCompletedGroupAlgebra ℓ G) where
sub x y := ⟨fun i =>
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) -
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) -
(show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j)) =
(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) -
(show PrimePowerCompletedGroupAlgebraStage ℓ G 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 instSMulNatPrimePowerCompletedGroupAlgebra :
SMul ℕ (PrimePowerCompletedGroupAlgebra ℓ G) where
smul m x := ⟨fun i => m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(m • (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
m • (show PrimePowerCompletedGroupAlgebraStage ℓ G 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 instSMulIntPrimePowerCompletedGroupAlgebra :
SMul ℤ (PrimePowerCompletedGroupAlgebra ℓ G) where
smul m x := ⟨fun i => m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
intro i j hij
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
(m • (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
m • (show PrimePowerCompletedGroupAlgebraStage ℓ G 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.
instance instAddCommGroupPrimePowerCompletedGroupAlgebraStage
(i : PrimePowerCompletedGroupAlgebraIndex G) :
AddCommGroup ((primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
dsimp [primePowerCompletedGroupAlgebraSystem, PrimePowerCompletedGroupAlgebraStage]
infer_instanceAddition in the prime-power completed group algebra is defined coordinatewise through finite-stage group-algebra additions.
instance instAddCommGroupPrimePowerCompletedGroupAlgebraFamily :
AddCommGroup
((i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) :=
inferInstanceAddition in the prime-power completed group algebra is defined coordinatewise through finite-stage group-algebra additions.
theorem coe_zero_primePowerCompletedGroupAlgebra :
((0 : PrimePowerCompletedGroupAlgebra ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) = 0The inclusion of the 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_primePowerCompletedGroupAlgebra
(x y : PrimePowerCompletedGroupAlgebra ℓ G) :
((x + y : PrimePowerCompletedGroupAlgebra ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) = x + yThe inclusion of the 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_primePowerCompletedGroupAlgebra
(x : PrimePowerCompletedGroupAlgebra ℓ G) :
((-x : PrimePowerCompletedGroupAlgebra ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) = -xThe inclusion of the 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_primePowerCompletedGroupAlgebra
(x y : PrimePowerCompletedGroupAlgebra ℓ G) :
((x - y : PrimePowerCompletedGroupAlgebra ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) = x - yThe inclusion of the prime-power completed group algebra preserves subtraction.
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_primePowerCompletedGroupAlgebra
(m : ℕ) (x : PrimePowerCompletedGroupAlgebra ℓ G) :
((m • x : PrimePowerCompletedGroupAlgebra ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) = m • xThe inclusion of the 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_primePowerCompletedGroupAlgebra
(m : ℤ) (x : PrimePowerCompletedGroupAlgebra ℓ G) :
((m • x : PrimePowerCompletedGroupAlgebra ℓ G) :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i) = m • xThe inclusion of the 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 instAddCommGroupPrimePowerCompletedGroupAlgebra :
AddCommGroup (PrimePowerCompletedGroupAlgebra ℓ G) :=
Function.Injective.addCommGroup
(fun x : PrimePowerCompletedGroupAlgebra ℓ G =>
(x :
(i : PrimePowerCompletedGroupAlgebraIndex G) →
(primePowerCompletedGroupAlgebraSystem ℓ G).X i))
Subtype.val_injective
(coe_zero_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
(coe_add_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
(coe_neg_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
(coe_sub_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
(fun x m => coe_nsmul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) m x)
(fun x m => coe_zsmul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) m x)Addition in the prime-power completed group algebra is defined coordinatewise through finite-stage group-algebra additions.