CompletedGroupAlgebra.Basic.AllFinite.Additive
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
abbrev Carrier (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
[IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
Type (max u v) :=
(completedGroupAlgebraSystem R G).inverseLimitThe carrier of the completed group algebra is the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\) over the open-normal finite quotients of \(G\).
abbrev completedGroupAlgebraProjection (R : Type u) (G : Type v) [CommRing R]
[TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G]
(U : CompletedGroupAlgebraIndex G) :
Carrier R G → CompletedGroupAlgebraStage R G U :=
(completedGroupAlgebraSystem R G).projection Uinstance instZeroCompletedGroupAlgebra : Zero (Carrier R G) where
zero := ⟨fun U => (0 : CompletedGroupAlgebraStage R G U), by
intro U V hUV
change completedGroupAlgebraTransition R G hUV
(0 : CompletedGroupAlgebraStage R G V) = 0
exact map_zero (completedGroupAlgebraTransition R G hUV)⟩The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.
instance instAddCompletedGroupAlgebra : Add (Carrier R G) where
add x y := ⟨fun U =>
(show CompletedGroupAlgebraStage R G U from x.1 U) +
(show CompletedGroupAlgebraStage R G U from y.1 U), by
intro U V hUV
calc
completedGroupAlgebraTransition R G hUV
((show CompletedGroupAlgebraStage R G V from x.1 V) +
(show CompletedGroupAlgebraStage R G V from y.1 V))
=
completedGroupAlgebraTransition R G hUV
(show CompletedGroupAlgebraStage R G V from x.1 V) +
completedGroupAlgebraTransition R G hUV
(show CompletedGroupAlgebraStage R G V from y.1 V) := by
rw [map_add]
_ = (show CompletedGroupAlgebraStage R G U from x.1 U) +
(show CompletedGroupAlgebraStage R G U from y.1 U) := by
exact congrArg₂ HAdd.hAdd (x.2 U V hUV) (y.2 U V hUV)⟩The additive structure of the completed group algebra is inherited coordinatewise from its finite group-algebra stages.
instance instAddZeroClassCompletedGroupAlgebra : AddZeroClass (Carrier R G) where
zero := 0
add := (· + ·)
zero_add x := by
apply Subtype.ext
funext U
change (0 : CompletedGroupAlgebraStage R G U) +
(show CompletedGroupAlgebraStage R G U from x.1 U) =
(show CompletedGroupAlgebraStage R G U from x.1 U)
simp only [zero_add]
add_zero x := by
apply Subtype.ext
funext U
change (show CompletedGroupAlgebraStage R G U from x.1 U) +
(0 : CompletedGroupAlgebraStage R G U) =
(show CompletedGroupAlgebraStage R G U from x.1 U)
simp only [add_zero]The additive structure of the completed group algebra is inherited coordinatewise from its finite group-algebra stages.
instance instNegCompletedGroupAlgebra : Neg (Carrier R G) where
neg x := ⟨fun U => -(show CompletedGroupAlgebraStage R G U from x.1 U), by
intro U V hUV
change completedGroupAlgebraTransition R G hUV
(-(show CompletedGroupAlgebraStage R G V from x.1 V)) =
-(show CompletedGroupAlgebraStage R G U from x.1 U)
rw [map_neg]
exact congrArg Neg.neg (x.2 U V hUV)⟩instance instSubCompletedGroupAlgebra : Sub (Carrier R G) where
sub x y := ⟨fun U =>
(show CompletedGroupAlgebraStage R G U from x.1 U) -
(show CompletedGroupAlgebraStage R G U from y.1 U), by
intro U V hUV
change completedGroupAlgebraTransition R G hUV
((show CompletedGroupAlgebraStage R G V from x.1 V) -
(show CompletedGroupAlgebraStage R G V from y.1 V)) =
(show CompletedGroupAlgebraStage R G U from x.1 U) -
(show CompletedGroupAlgebraStage R 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 instSMulNatCompletedGroupAlgebra : SMul ℕ (Carrier R G) where
smul n x := ⟨fun U => n • (show CompletedGroupAlgebraStage R G U from x.1 U), by
intro U V hUV
change completedGroupAlgebraTransition R G hUV
(n • (show CompletedGroupAlgebraStage R G V from x.1 V)) =
n • (show CompletedGroupAlgebraStage R G U from x.1 U)
rw [map_nsmul]
exact congrArg (n • ·) (x.2 U V hUV)⟩The all-finite completed group algebra carries natural-number scalar multiplication coordinatewise.
instance instSMulIntCompletedGroupAlgebra : SMul ℤ (Carrier R G) where
smul n x := ⟨fun U => n • (show CompletedGroupAlgebraStage R G U from x.1 U), by
intro U V hUV
change completedGroupAlgebraTransition R G hUV
(n • (show CompletedGroupAlgebraStage R G V from x.1 V)) =
n • (show CompletedGroupAlgebraStage R G U from x.1 U)
rw [map_zsmul]
exact congrArg (n • ·) (x.2 U V hUV)⟩The all-finite completed group algebra carries integer scalar multiplication coordinatewise.
instance instAddCommGroupCompletedGroupAlgebraStage
(U : CompletedGroupAlgebraIndex G) :
AddCommGroup ((completedGroupAlgebraSystem R G).X U) := by
dsimp [completedGroupAlgebraSystem, CompletedGroupAlgebraStage]
infer_instanceAddition at each finite group-algebra stage is the usual stagewise addition.
instance instAddCommGroupCompletedGroupAlgebraFamily :
AddCommGroup
((U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) :=
inferInstanceAddition in the completed group-algebra family is defined coordinatewise across finite stages.
theorem coe_zero_completedGroupAlgebra :
((0 : Carrier R G) :
(U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) = 0The zero operation is computed coordinatewise in the inverse-limit completed group algebra.
Show proof
by
funext U
rflProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem coe_add_completedGroupAlgebra (x y : Carrier R G) :
((x + y : Carrier R G) :
(U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
x + yThe addition operation is computed coordinatewise in the inverse-limit completed group algebra.
Show proof
by
funext U
rflProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem coe_neg_completedGroupAlgebra (x : Carrier R G) :
((-x : Carrier R G) :
(U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
-xThe negation operation is computed coordinatewise in the inverse-limit completed group algebra.
Show proof
by
funext U
rflProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem coe_sub_completedGroupAlgebra (x y : Carrier R G) :
((x - y : Carrier R G) :
(U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
x - yThe subtraction operation is computed coordinatewise in the inverse-limit completed group algebra.
Show proof
by
funext U
rflProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem coe_nsmul_completedGroupAlgebra (n : ℕ) (x : Carrier R G) :
((n • x : Carrier R G) :
(U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
n • xThe natural-number scalar multiplication operation is computed coordinatewise in the inverse-limit completed group algebra.
Show proof
by
funext U
rflProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums.
□theorem coe_zsmul_completedGroupAlgebra (n : ℤ) (x : Carrier R G) :
((n • x : Carrier R G) :
(U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
n • xThe integer scalar multiplication operation is computed coordinatewise in the inverse-limit completed group algebra.
Show proof
by
funext U
rflProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums.
□instance instAddCommGroupCompletedGroupAlgebra : AddCommGroup (Carrier R G) :=
Function.Injective.addCommGroup
(fun x : Carrier R G =>
(x : (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U))
Subtype.val_injective
(coe_zero_completedGroupAlgebra (R := R) (G := G))
(coe_add_completedGroupAlgebra (R := R) (G := G))
(coe_neg_completedGroupAlgebra (R := R) (G := G))
(coe_sub_completedGroupAlgebra (R := R) (G := G))
(fun x n => coe_nsmul_completedGroupAlgebra (R := R) (G := G) n x)
(fun x n => coe_zsmul_completedGroupAlgebra (R := R) (G := G) n x)The additive structure of the completed group algebra is inherited coordinatewise from its finite group-algebra stages.
theorem completedGroupAlgebraTransition_smul
{U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
(r : R) (x : CompletedGroupAlgebraStage R G V) :
completedGroupAlgebraTransition R G hUV (r • x) =
r • completedGroupAlgebraTransition R G hUV xTransition maps commute with coefficient scalar multiplication.
Show proof
by
rw [Algebra.smul_def, Algebra.smul_def, map_mul]
congr 1
simp only [completedGroupAlgebraTransition, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
RingHom.coe_id, Function.comp_apply, id_eq, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one]Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums.
□instance instSMulCoeffCompletedGroupAlgebra : SMul R (Carrier R G) where
smul r x := ⟨fun U => r • (show CompletedGroupAlgebraStage R G U from x.1 U), by
intro U V hUV
change completedGroupAlgebraTransition R G hUV
(r • (show CompletedGroupAlgebraStage R G V from x.1 V)) =
r • (show CompletedGroupAlgebraStage R G U from x.1 U)
rw [completedGroupAlgebraTransition_smul]
exact congrArg (r • ·) (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_smul_completedGroupAlgebra (r : R) (x : Carrier R G) :
((r • x : Carrier R G) :
(U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
fun U => r • (show CompletedGroupAlgebraStage R G U from x.1 U)The scalar multiplication operation is computed coordinatewise in the inverse-limit completed group algebra.
Show proof
by
funext U
rflProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums.
□def completedGroupAlgebraValAddMonoidHom :
Carrier R G →+
((U : CompletedGroupAlgebraIndex G) → CompletedGroupAlgebraStage R G U) where
toFun x := fun U => (show CompletedGroupAlgebraStage R G U from x.1 U)
map_zero' := by
funext U
rfl
map_add' x y := by
funext U
rflThe coordinatewise additive monoid homomorphism from the completed group algebra.
instance instModuleCoeffCompletedGroupAlgebra : Module R (Carrier R G) :=
Function.Injective.module R
(completedGroupAlgebraValAddMonoidHom (R := R) (G := G))
(fun x y h => by
apply Subtype.ext
funext U
exact congrFun h U)
(fun r x => by
funext U
change (show CompletedGroupAlgebraStage R G U from (r • x).1 U) =
r • (show CompletedGroupAlgebraStage R G U from x.1 U)
rfl)