FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.AddCommGroup
Fox Differential / Completed / Coefficient Rings / Completed Group Algebra Mod N / System / Additive Commutative Group.
instance instZeroModNCompletedGroupAlgebra : Zero (ModNCompletedGroupAlgebra n G) where
zero := ⟨fun U => (0 : ModNCompletedGroupAlgebraStage n G U), by
intro U V hUV
change modNCompletedGroupAlgebraTransition n G hUV
(0 : ModNCompletedGroupAlgebraStage n G V) = 0
exact map_zero (modNCompletedGroupAlgebraTransition n G hUV)⟩The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.
instance instAddModNCompletedGroupAlgebra : Add (ModNCompletedGroupAlgebra n G) where
add x y := ⟨fun U =>
(show ModNCompletedGroupAlgebraStage n G U from x.1 U) +
(show ModNCompletedGroupAlgebraStage n G U from y.1 U), by
intro U V hUV
calc
modNCompletedGroupAlgebraTransition n G hUV
((show ModNCompletedGroupAlgebraStage n G V from x.1 V) +
(show ModNCompletedGroupAlgebraStage n G V from y.1 V))
=
modNCompletedGroupAlgebraTransition n G hUV
(show ModNCompletedGroupAlgebraStage n G V from x.1 V) +
modNCompletedGroupAlgebraTransition n G hUV
(show ModNCompletedGroupAlgebraStage n G V from y.1 V) := by
rw [map_add]
_ =
(show ModNCompletedGroupAlgebraStage n G U from x.1 U) +
(show ModNCompletedGroupAlgebraStage n G U from y.1 U) := by
exact congrArg₂ HAdd.hAdd (x.2 U V hUV) (y.2 U V hUV)⟩Addition in the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra additions.
instance instAddZeroClassModNCompletedGroupAlgebra :
AddZeroClass (ModNCompletedGroupAlgebra n G) where
zero := 0
add := (· + ·)
zero_add x := by
apply Subtype.ext
funext U
change (0 : ModNCompletedGroupAlgebraStage n G U) +
(show ModNCompletedGroupAlgebraStage n G U from x.1 U) =
(show ModNCompletedGroupAlgebraStage n G U from x.1 U)
simp only [zero_add]
add_zero x := by
apply Subtype.ext
funext U
change (show ModNCompletedGroupAlgebraStage n G U from x.1 U) +
(0 : ModNCompletedGroupAlgebraStage n G U) =
(show ModNCompletedGroupAlgebraStage n G U from x.1 U)
simp only [add_zero]Addition in the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra additions.
instance instNegModNCompletedGroupAlgebra : Neg (ModNCompletedGroupAlgebra n G) where
neg x := ⟨fun U => -(show ModNCompletedGroupAlgebraStage n G U from x.1 U), by
intro U V hUV
change modNCompletedGroupAlgebraTransition n G hUV
(-(show ModNCompletedGroupAlgebraStage n G V from x.1 V)) =
-(show ModNCompletedGroupAlgebraStage n G U from x.1 U)
rw [map_neg]
exact congrArg Neg.neg (x.2 U V hUV)⟩Negation on the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra negations.
instance instSubModNCompletedGroupAlgebra : Sub (ModNCompletedGroupAlgebra n G) where
sub x y := ⟨fun U =>
(show ModNCompletedGroupAlgebraStage n G U from x.1 U) -
(show ModNCompletedGroupAlgebraStage n G U from y.1 U), by
intro U V hUV
change modNCompletedGroupAlgebraTransition n G hUV
((show ModNCompletedGroupAlgebraStage n G V from x.1 V) -
(show ModNCompletedGroupAlgebraStage n G V from y.1 V)) =
(show ModNCompletedGroupAlgebraStage n G U from x.1 U) -
(show ModNCompletedGroupAlgebraStage n G U from y.1 U)
rw [map_sub]
exact congrArg₂ HSub.hSub (x.2 U V hUV) (y.2 U V hUV)⟩Subtraction on the completed group algebra is defined coordinatewise through the finite-stage group-algebra subtractions.
instance instSMulNatModNCompletedGroupAlgebra : SMul ℕ (ModNCompletedGroupAlgebra n G) where
smul m x := ⟨fun U => m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U), by
intro U V hUV
change modNCompletedGroupAlgebraTransition n G hUV
(m • (show ModNCompletedGroupAlgebraStage n G V from x.1 V)) =
m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U)
rw [map_nsmul]
exact congrArg (m • ·) (x.2 U V hUV)⟩The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.
instance instSMulIntModNCompletedGroupAlgebra : SMul ℤ (ModNCompletedGroupAlgebra n G) where
smul m x := ⟨fun U => m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U), by
intro U V hUV
change modNCompletedGroupAlgebraTransition n G hUV
(m • (show ModNCompletedGroupAlgebraStage n G V from x.1 V)) =
m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U)
rw [map_zsmul]
exact congrArg (m • ·) (x.2 U V hUV)⟩The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.
instance instAddCommGroupModNCompletedGroupAlgebraStage (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
AddCommGroup ((modNCompletedGroupAlgebraSystem n G).X U) := by
dsimp [modNCompletedGroupAlgebraSystem, ModNCompletedGroupAlgebraStage]
infer_instanceAddition in the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra additions.
instance instAddCommGroupModNCompletedGroupAlgebraFamily :
AddCommGroup ((i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) :=
inferInstanceAddition in the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra additions.
theorem coe_zero_modNCompletedGroupAlgebra :
((0 : ModNCompletedGroupAlgebra n G) :
(i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) = 0The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves zero.
Show proof
by
funext U
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□theorem coe_add_modNCompletedGroupAlgebra
(x y : ModNCompletedGroupAlgebra n G) :
((x + y : ModNCompletedGroupAlgebra n G) :
(i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) =
x + yThe inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves addition.
Show proof
by
funext U
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□theorem coe_neg_modNCompletedGroupAlgebra
(x : ModNCompletedGroupAlgebra n G) :
((-x : ModNCompletedGroupAlgebra n G) :
(i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) =
-xThe inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves negation.
Show proof
by
funext U
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□theorem coe_sub_modNCompletedGroupAlgebra
(x y : ModNCompletedGroupAlgebra n G) :
((x - y : ModNCompletedGroupAlgebra n G) :
(i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) =
x - yThe inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves subtraction.
Show proof
by
funext U
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□theorem coe_nsmul_modNCompletedGroupAlgebra
(m : ℕ) (x : ModNCompletedGroupAlgebra n G) :
((m • x : ModNCompletedGroupAlgebra n G) :
(i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) =
m • xThe inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves natural-number scalar multiplication.
Show proof
by
funext U
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□theorem coe_zsmul_modNCompletedGroupAlgebra
(m : ℤ) (x : ModNCompletedGroupAlgebra n G) :
((m • x : ModNCompletedGroupAlgebra n G) :
(i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) =
m • xThe inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra preserves integer scalar multiplication.
Show proof
by
funext U
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□instance instAddCommGroupModNCompletedGroupAlgebra :
AddCommGroup (ModNCompletedGroupAlgebra n G) :=
Function.Injective.addCommGroup
(fun x : ModNCompletedGroupAlgebra n G =>
(x : (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i))
Subtype.val_injective
(coe_zero_modNCompletedGroupAlgebra (n := n) (G := G))
(coe_add_modNCompletedGroupAlgebra (n := n) (G := G))
(coe_neg_modNCompletedGroupAlgebra (n := n) (G := G))
(coe_sub_modNCompletedGroupAlgebra (n := n) (G := G))
(fun x m => coe_nsmul_modNCompletedGroupAlgebra (n := n) (G := G) m x)
(fun x m => coe_zsmul_modNCompletedGroupAlgebra (n := n) (G := G) m x)Addition in the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra additions.
theorem modNCompletedGroupAlgebraProjection_zero (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
modNCompletedGroupAlgebraProjection n G U (0 : ModNCompletedGroupAlgebra n G) = 0The finite-stage projection sends \(0\) to \(0\).
Show proof
by
change (0 : ModNCompletedGroupAlgebraStage n G U) = 0
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□theorem modNCompletedGroupAlgebraProjection_add (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
(x y : ModNCompletedGroupAlgebra n G) :
modNCompletedGroupAlgebraProjection n G U (x + y) =
modNCompletedGroupAlgebraProjection n G U x +
modNCompletedGroupAlgebraProjection n G U yThe mod-\(n\) finite-stage projection preserves addition.
Show proof
by
change (show ModNCompletedGroupAlgebraStage n G U from (x + y).1 U) =
(show ModNCompletedGroupAlgebraStage n G U from x.1 U) +
(show ModNCompletedGroupAlgebraStage n G U from y.1 U)
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□theorem modNCompletedGroupAlgebraProjection_neg (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
(x : ModNCompletedGroupAlgebra n G) :
modNCompletedGroupAlgebraProjection n G U (-x) =
-modNCompletedGroupAlgebraProjection n G U xThe mod-\(n\) finite-stage projection preserves negation.
Show proof
by
change (show ModNCompletedGroupAlgebraStage n G U from (-x).1 U) =
-(show ModNCompletedGroupAlgebraStage n G U from x.1 U)
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□theorem modNCompletedGroupAlgebraProjection_sub (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
(x y : ModNCompletedGroupAlgebra n G) :
modNCompletedGroupAlgebraProjection n G U (x - y) =
modNCompletedGroupAlgebraProjection n G U x -
modNCompletedGroupAlgebraProjection n G U yThe mod-\(n\) finite-stage projection preserves subtraction.
Show proof
by
change (show ModNCompletedGroupAlgebraStage n G U from (x - y).1 U) =
(show ModNCompletedGroupAlgebraStage n G U from x.1 U) -
(show ModNCompletedGroupAlgebraStage n G U from y.1 U)
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□