FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.AddCommGroup
Fox Differential / Completed / Coefficient Rings / Completed Group Algebra Mod N / Within a Class / Additive Commutative Group.
instance instZeroModNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
Zero (ModNCompletedGroupAlgebraInClass n G C) where
zero := ⟨fun U => (0 : ModNCompletedGroupAlgebraStageInClass n G C U), by
intro U V hUV
change modNCompletedGroupAlgebraTransitionInClass n G C hUV
(0 : ModNCompletedGroupAlgebraStageInClass n G C V) = 0
exact map_zero _⟩The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.
instance instAddModNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
Add (ModNCompletedGroupAlgebraInClass n G C) where
add x y := ⟨fun U =>
(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
(show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U), by
intro U V hUV
calc
modNCompletedGroupAlgebraTransitionInClass n G C hUV
((show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) +
(show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V))
=
modNCompletedGroupAlgebraTransitionInClass n G C hUV
(show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) +
modNCompletedGroupAlgebraTransitionInClass n G C hUV
(show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V) := by
rw [map_add]
_ =
(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
(show ModNCompletedGroupAlgebraStageInClass n G C 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 instAddZeroClassModNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
AddZeroClass (ModNCompletedGroupAlgebraInClass n G C) where
zero := 0
add := (· + ·)
zero_add x := by
apply Subtype.ext
funext U
change (0 : ModNCompletedGroupAlgebraStageInClass n G C U) +
(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) =
(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
simp only [zero_add]
add_zero x := by
apply Subtype.ext
funext U
change (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
(0 : ModNCompletedGroupAlgebraStageInClass n G C U) =
(show ModNCompletedGroupAlgebraStageInClass n G C 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 instNegModNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
Neg (ModNCompletedGroupAlgebraInClass n G C) where
neg x := ⟨fun U => -(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
intro U V hUV
change modNCompletedGroupAlgebraTransitionInClass n G C hUV
(-(show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
-(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
rw [map_neg]
exact congrArg Neg.neg (x.2 U V hUV)⟩Negation on the \(C\)-indexed mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra negations.
instance instSubModNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
Sub (ModNCompletedGroupAlgebraInClass n G C) where
sub x y := ⟨fun U =>
(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) -
(show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U), by
intro U V hUV
change modNCompletedGroupAlgebraTransitionInClass n G C hUV
((show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) -
(show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V)) =
(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) -
(show ModNCompletedGroupAlgebraStageInClass n G C 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 instSMulNatModNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
SMul ℕ (ModNCompletedGroupAlgebraInClass n G C) where
smul m x := ⟨fun U =>
m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
intro U V hUV
change modNCompletedGroupAlgebraTransitionInClass n G C hUV
(m • (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
m • (show ModNCompletedGroupAlgebraStageInClass n G C 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 instSMulIntModNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
SMul ℤ (ModNCompletedGroupAlgebraInClass n G C) where
smul m x := ⟨fun U =>
m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
intro U V hUV
change modNCompletedGroupAlgebraTransitionInClass n G C hUV
(m • (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
m • (show ModNCompletedGroupAlgebraStageInClass n G C 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.
theorem coe_zero_modNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
((0 : ModNCompletedGroupAlgebraInClass n G C) :
(U : CompletedGroupAlgebraIndexInClass G C) →
ModNCompletedGroupAlgebraStageInClass n G C U) = 0The inclusion of the \(C\)-indexed 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_modNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u})
(x y : ModNCompletedGroupAlgebraInClass n G C) :
((x + y : ModNCompletedGroupAlgebraInClass n G C) :
(U : CompletedGroupAlgebraIndexInClass G C) →
ModNCompletedGroupAlgebraStageInClass n G C U) = x + yThe inclusion of the \(C\)-indexed 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_modNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u})
(x : ModNCompletedGroupAlgebraInClass n G C) :
((-x : ModNCompletedGroupAlgebraInClass n G C) :
(U : CompletedGroupAlgebraIndexInClass G C) →
ModNCompletedGroupAlgebraStageInClass n G C U) = -xThe inclusion of the \(C\)-indexed 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_modNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u})
(x y : ModNCompletedGroupAlgebraInClass n G C) :
((x - y : ModNCompletedGroupAlgebraInClass n G C) :
(U : CompletedGroupAlgebraIndexInClass G C) →
ModNCompletedGroupAlgebraStageInClass n G C U) = x - yThe inclusion of the \(C\)-indexed 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_modNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u})
(m : ℕ) (x : ModNCompletedGroupAlgebraInClass n G C) :
((m • x : ModNCompletedGroupAlgebraInClass n G C) :
(U : CompletedGroupAlgebraIndexInClass G C) →
ModNCompletedGroupAlgebraStageInClass n G C U) = m • xThe inclusion of the \(C\)-indexed 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_modNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u})
(m : ℤ) (x : ModNCompletedGroupAlgebraInClass n G C) :
((m • x : ModNCompletedGroupAlgebraInClass n G C) :
(U : CompletedGroupAlgebraIndexInClass G C) →
ModNCompletedGroupAlgebraStageInClass n G C U) = m • xThe inclusion of the \(C\)-indexed 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 instAddCommGroupModNCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
AddCommGroup (ModNCompletedGroupAlgebraInClass n G C) :=
Function.Injective.addCommGroup
(fun x : ModNCompletedGroupAlgebraInClass n G C =>
(x :
(U : CompletedGroupAlgebraIndexInClass G C) →
ModNCompletedGroupAlgebraStageInClass n G C U))
Subtype.val_injective
(coe_zero_modNCompletedGroupAlgebraInClass (n := n) (G := G) C)
(coe_add_modNCompletedGroupAlgebraInClass (n := n) (G := G) C)
(coe_neg_modNCompletedGroupAlgebraInClass (n := n) (G := G) C)
(coe_sub_modNCompletedGroupAlgebraInClass (n := n) (G := G) C)
(fun x m => coe_nsmul_modNCompletedGroupAlgebraInClass (n := n) (G := G) C m x)
(fun x m => coe_zsmul_modNCompletedGroupAlgebraInClass (n := n) (G := G) C m x)Addition in the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra additions.
theorem modNCompletedGroupAlgebraProjectionInClass_zero
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
modNCompletedGroupAlgebraProjectionInClass n G C U
(0 : ModNCompletedGroupAlgebraInClass n G C) = 0The finite-stage projection sends \(0\) to \(0\).
Show proof
by
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 modNCompletedGroupAlgebraProjectionInClass_add
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
(x y : ModNCompletedGroupAlgebraInClass n G C) :
modNCompletedGroupAlgebraProjectionInClass n G C U (x + y) =
modNCompletedGroupAlgebraProjectionInClass n G C U x +
modNCompletedGroupAlgebraProjectionInClass n G C U yThe mod-\(n\) finite-stage projection preserves addition.
Show proof
by
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 modNCompletedGroupAlgebraProjectionInClass_neg
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
(x : ModNCompletedGroupAlgebraInClass n G C) :
modNCompletedGroupAlgebraProjectionInClass n G C U (-x) =
-modNCompletedGroupAlgebraProjectionInClass n G C U xThe mod-\(n\) finite-stage projection preserves negation.
Show proof
by
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 modNCompletedGroupAlgebraProjectionInClass_sub
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
(x y : ModNCompletedGroupAlgebraInClass n G C) :
modNCompletedGroupAlgebraProjectionInClass n G C U (x - y) =
modNCompletedGroupAlgebraProjectionInClass n G C U x -
modNCompletedGroupAlgebraProjectionInClass n G C U yThe mod-\(n\) finite-stage projection preserves subtraction.
Show proof
by
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 modNCompletedGroupAlgebraProjectionInClass_nsmul
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
(m : ℕ) (x : ModNCompletedGroupAlgebraInClass n G C) :
modNCompletedGroupAlgebraProjectionInClass n G C U (m • x) =
m • modNCompletedGroupAlgebraProjectionInClass n G C U xThe finite-stage projection is compatible with natural-number scalar multiplication.
Show proof
by
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 modNCompletedGroupAlgebraProjectionInClass_zsmul
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
(m : ℤ) (x : ModNCompletedGroupAlgebraInClass n G C) :
modNCompletedGroupAlgebraProjectionInClass n G C U (m • x) =
m • modNCompletedGroupAlgebraProjectionInClass n G C U xThe finite-stage projection is compatible with integer scalar multiplication.
Show proof
by
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.
□