CompletedGroupAlgebra.Basic.AllFinite.Ring
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.
instance instOneCompletedGroupAlgebra : One (Carrier R G) where
one := ⟨fun U => (1 : CompletedGroupAlgebraStage R G U), by
intro U V hUV
change completedGroupAlgebraTransition R G hUV
(1 : CompletedGroupAlgebraStage R G V) = 1
exact map_one (completedGroupAlgebraTransition R G hUV)⟩The unit of the completed group algebra is defined coordinatewise through the finite-stage units.
instance instMulCompletedGroupAlgebra : Mul (Carrier R G) where
mul 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_mul]
_ = (show CompletedGroupAlgebraStage R G U from x.1 U) *
(show CompletedGroupAlgebraStage R G U from y.1 U) := by
exact congrArg₂ HMul.hMul (x.2 U V hUV) (y.2 U V hUV)⟩Multiplication on the completed group algebra is defined coordinatewise through the finite-stage group-algebra products.
instance instNatCastCompletedGroupAlgebra : NatCast (Carrier R G) where
natCast n := ⟨fun U => (n : CompletedGroupAlgebraStage R G U), by
intro U V hUV
change completedGroupAlgebraTransition R G hUV
(n : CompletedGroupAlgebraStage R G V) = n
exact map_natCast (completedGroupAlgebraTransition R G hUV) n⟩Natural-number numerals in the completed group algebra are interpreted coordinatewise through the finite-stage ring structures.
instance instIntCastCompletedGroupAlgebra : IntCast (Carrier R G) where
intCast n := ⟨fun U => (n : CompletedGroupAlgebraStage R G U), by
intro U V hUV
change completedGroupAlgebraTransition R G hUV
(n : CompletedGroupAlgebraStage R G V) = n
exact map_intCast (completedGroupAlgebraTransition R G hUV) n⟩Integer numerals in the completed group algebra are interpreted coordinatewise through the finite-stage ring structures.
instance instRingCompletedGroupAlgebraStage
(U : CompletedGroupAlgebraIndex G) :
Ring ((completedGroupAlgebraSystem R G).X U) := by
dsimp [completedGroupAlgebraSystem, CompletedGroupAlgebraStage]
infer_instanceThe completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.
instance instRingCompletedGroupAlgebraFamily :
Ring ((U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) :=
inferInstanceThe completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.
instance instPowCompletedGroupAlgebra : Pow (Carrier R G) ℕ where
pow x n := ⟨fun U => (show CompletedGroupAlgebraStage R G U from x.1 U) ^ n, by
intro U V hUV
change completedGroupAlgebraTransition R G hUV
((show CompletedGroupAlgebraStage R G V from x.1 V) ^ n) =
(show CompletedGroupAlgebraStage R G U from x.1 U) ^ n
rw [map_pow]
exact congrArg (fun t => t ^ n) (x.2 U V hUV)⟩Powers in the completed group algebra are computed coordinatewise in the finite-stage group algebras.
theorem coe_one_completedGroupAlgebra :
((1 : Carrier R G) :
(U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) = 1The unit 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_mul_completedGroupAlgebra (x y : Carrier R G) :
((x * y : Carrier R G) :
(U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
x * yThe 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. 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_natCast_completedGroupAlgebra (n : ℕ) :
((n : Carrier R G) :
(U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
nNatural number casts are 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_intCast_completedGroupAlgebra (n : ℤ) :
((n : Carrier R G) :
(U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
nInteger casts are 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_pow_completedGroupAlgebra (x : Carrier R G) (n : ℕ) :
((x ^ n : Carrier R G) :
(U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
x ^ nThe pow 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.
□instance instRingCompletedGroupAlgebra : Ring (Carrier R G) :=
Function.Injective.ring
(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_one_completedGroupAlgebra (R := R) (G := G))
(coe_add_completedGroupAlgebra (R := R) (G := G))
(coe_mul_completedGroupAlgebra (R := R) (G := G))
(coe_neg_completedGroupAlgebra (R := R) (G := G))
(coe_sub_completedGroupAlgebra (R := R) (G := G))
(fun n x => coe_nsmul_completedGroupAlgebra (R := R) (G := G) n x)
(fun n x => coe_zsmul_completedGroupAlgebra (R := R) (G := G) n x)
(fun x n => coe_pow_completedGroupAlgebra (R := R) (G := G) x n)
(by intro n; exact coe_natCast_completedGroupAlgebra (R := R) (G := G) n)
(by intro n; exact coe_intCast_completedGroupAlgebra (R := R) (G := G) n)The completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.
def completedGroupAlgebraCoeffMap
(S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
(f : R →+* S) :
Carrier R G →+* Carrier S G where
toFun x := ⟨fun U => completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U (x.1 U), by
intro U V hUV
have hcompat := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageCoeffMap_compatible
(R := R) (G := G) S f hUV))
(x.1 V)
calc
completedGroupAlgebraTransition S G hUV
(completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f V (x.1 V))
=
completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U
(completedGroupAlgebraTransition R G hUV (x.1 V)) := hcompat.symm
_ =
completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U (x.1 U) := by
exact congrArg (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U)
(x.2 U V hUV)⟩
map_zero' := by
apply Subtype.ext
funext U
exact map_zero (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U)
map_one' := by
apply Subtype.ext
funext U
exact map_one (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U)
map_add' x y := by
apply Subtype.ext
funext U
exact map_add (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U) (x.1 U) (y.1 U)
map_mul' x y := by
apply Subtype.ext
funext U
exact map_mul (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U) (x.1 U) (y.1 U)
@[simp]The all-finite completed group-algebra coefficient-change map is defined stagewise.
theorem completedGroupAlgebraProjection_coeffMap
(S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
(f : R →+* S) (U : CompletedGroupAlgebraIndex G)
(x : Carrier R G) :
completedGroupAlgebraProjection S G U
(completedGroupAlgebraCoeffMap (R := R) (G := G) S f x) =
completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U
(completedGroupAlgebraProjection R G U x)Show proof
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, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. 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. 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem completedGroupAlgebraProjection_zero (U : CompletedGroupAlgebraIndex G) :
completedGroupAlgebraProjection R G U (0 : Carrier R G) = 0The projection from \(\widehat{R[G]}\) to \(R[G/U]\) sends \(0\) to \(0\).
Show proof
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, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra. 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 completedGroupAlgebraProjection_add (U : CompletedGroupAlgebraIndex G)
(x y : Carrier R G) :
completedGroupAlgebraProjection R G U (x + y) =
completedGroupAlgebraProjection R G U x + completedGroupAlgebraProjection R G U yThe finite-stage projection preserves addition.
Show proof
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, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem completedGroupAlgebraProjection_smul (U : CompletedGroupAlgebraIndex G)
(r : R) (x : Carrier R G) :
completedGroupAlgebraProjection R G U (r • x) =
r • completedGroupAlgebraProjection R G U xThe projection from \(\widehat{R[G]}\) to \(R[G/U]\) is compatible with scalar multiplication by elements of \(R\).
Show proof
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, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. 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 completedGroupAlgebraProjection_one (U : CompletedGroupAlgebraIndex G) :
completedGroupAlgebraProjection R G U (1 : Carrier R G) = 1The projection from \(\widehat{R[G]}\) to \(R[G/U]\) sends the unit of the completed group algebra to the unit of the finite-stage group algebra.
Show proof
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, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem completedGroupAlgebraProjection_mul (U : CompletedGroupAlgebraIndex G)
(x y : Carrier R G) :
completedGroupAlgebraProjection R G U (x * y) =
completedGroupAlgebraProjection R G U x * completedGroupAlgebraProjection R G U yThe projection from \(\widehat{R[G]}\) to a finite stage \(R[G/U]\) preserves multiplication.
Show proof
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, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem completedGroupAlgebraTransition_algebraMap
{U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (r : R) :
completedGroupAlgebraTransition R G hUV
(algebraMap R (CompletedGroupAlgebraStage R G V) r) =
algebraMap R (CompletedGroupAlgebraStage R G U) rTransition maps between finite group-algebra stages preserve scalar elements coming from the coefficient ring \(R\).
Show proof
by
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. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. 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 completedGroupAlgebraAlgebraMap (R : Type u) (G : Type v) [CommRing R]
[TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] : R →+* Carrier R G where
toFun r := ⟨fun U => algebraMap R (CompletedGroupAlgebraStage R G U) r, by
intro U V hUV
exact completedGroupAlgebraTransition_algebraMap (R := R) (G := G) hUV r⟩
map_zero' := by
apply (completedGroupAlgebraSystem R G).ext
intro U
change algebraMap R (CompletedGroupAlgebraStage R G U) (0 : R) = 0
exact map_zero (algebraMap R (CompletedGroupAlgebraStage R G U))
map_one' := by
apply (completedGroupAlgebraSystem R G).ext
intro U
change algebraMap R (CompletedGroupAlgebraStage R G U) (1 : R) = 1
exact map_one (algebraMap R (CompletedGroupAlgebraStage R G U))
map_add' r s := by
apply (completedGroupAlgebraSystem R G).ext
intro U
change algebraMap R (CompletedGroupAlgebraStage R G U) (r + s) =
algebraMap R (CompletedGroupAlgebraStage R G U) r +
algebraMap R (CompletedGroupAlgebraStage R G U) s
exact map_add (algebraMap R (CompletedGroupAlgebraStage R G U)) r s
map_mul' r s := by
apply (completedGroupAlgebraSystem R G).ext
intro U
change algebraMap R (CompletedGroupAlgebraStage R G U) (r * s) =
algebraMap R (CompletedGroupAlgebraStage R G U) r *
algebraMap R (CompletedGroupAlgebraStage R G U) s
exact map_mul (algebraMap R (CompletedGroupAlgebraStage R G U)) r sThe coefficient-ring map sends a coefficient to the corresponding constant element of the completed group algebra.
instance instAlgebraCompletedGroupAlgebra : Algebra R (Carrier R G) where
algebraMap := completedGroupAlgebraAlgebraMap R G
commutes' := by
intro r x
apply (completedGroupAlgebraSystem R G).ext
intro U
change algebraMap R (CompletedGroupAlgebraStage R G U) r *
completedGroupAlgebraProjection R G U x =
completedGroupAlgebraProjection R G U x *
algebraMap R (CompletedGroupAlgebraStage R G U) r
exact Algebra.commutes r (completedGroupAlgebraProjection R G U x)
smul_def' := by
intro r x
apply (completedGroupAlgebraSystem R G).ext
intro U
change completedGroupAlgebraProjection R G U (r • x) =
completedGroupAlgebraProjection R G U (completedGroupAlgebraAlgebraMap R G r * x)
rw [completedGroupAlgebraProjection_smul, completedGroupAlgebraProjection_mul]
change r • completedGroupAlgebraProjection R G U x =
algebraMap R (CompletedGroupAlgebraStage R G U) r *
completedGroupAlgebraProjection R G U x
rw [Algebra.smul_def]The completed group algebra is an algebra over the coefficient ring via the coordinatewise finite-stage algebra maps.