CompletedGroupAlgebra.Basic.InClass.LimitAlgebra
Completed Group Algebra / Basic / Within a Class / Limit Algebra.
abbrev CompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
Type (max u v) :=
(completedGroupAlgebraSystemInClass C hC R G).inverseLimitThe \(C\)-indexed completed group algebra as an inverse limit of finite-stage group algebras.
instance instRingCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
Ring (CompletedGroupAlgebraInClass C hC R G) := by
change Ring (completedGroupAlgebraSystemInClass C hC R G).inverseLimit
infer_instanceThe completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.
def completedGroupAlgebraCoeffMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
(f : R →+* S) :
CompletedGroupAlgebraInClass C hC R G →+* CompletedGroupAlgebraInClass C hC S G where
toFun x := ⟨fun U =>
completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U (x.1 U), by
intro U V hUV
have hcompat := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageCoeffMapInClass_compatible
(R := R) (G := G) C S f hUV))
(x.1 V)
calc
completedGroupAlgebraTransitionInClass C S G hUV
(completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f V (x.1 V))
=
completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U
(completedGroupAlgebraTransitionInClass C R G hUV (x.1 V)) := hcompat.symm
_ =
completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U (x.1 U) := by
exact congrArg (completedGroupAlgebraStageCoeffMapInClass
(R := R) (G := G) C S f U) (x.2 U V hUV)⟩
map_zero' := by
apply Subtype.ext
funext U
exact map_zero (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)
map_one' := by
apply Subtype.ext
funext U
exact map_one (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)
map_add' x y := by
apply Subtype.ext
funext U
exact map_add (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)
(x.1 U) (y.1 U)
map_mul' x y := by
apply Subtype.ext
funext U
exact map_mul (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)
(x.1 U) (y.1 U)The \(C\)-indexed completed group-algebra coefficient-change map is defined stagewise.
instance instSMulCoeffCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
SMul R (CompletedGroupAlgebraInClass C hC R G) where
smul r x := ⟨fun U =>
r • (show CompletedGroupAlgebraStageInClass C R G U from x.1 U), by
intro U V hUV
change completedGroupAlgebraTransitionInClass C R G hUV
(r • (show CompletedGroupAlgebraStageInClass C R G V from x.1 V)) =
r • (show CompletedGroupAlgebraStageInClass C R G U from x.1 U)
rw [completedGroupAlgebraTransitionInClass_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_completedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(r : R) (x : CompletedGroupAlgebraInClass C hC R G) :
((r • x : CompletedGroupAlgebraInClass C hC R G) :
(U : CompletedGroupAlgebraIndexInClass G C) →
(completedGroupAlgebraSystemInClass C hC R G).X U) =
fun U => r • (show CompletedGroupAlgebraStageInClass C R G U from x.1 U)Scalar multiplication in the inverse-limit algebra is computed stagewise.
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. 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 completedGroupAlgebraInClassValAddMonoidHom
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
CompletedGroupAlgebraInClass C hC R G →+
((U : CompletedGroupAlgebraIndexInClass G C) →
CompletedGroupAlgebraStageInClass C R G U) where
toFun x := fun U => (show CompletedGroupAlgebraStageInClass C R G U from x.1 U)
map_zero' := by
funext U
rfl
map_add' x y := by
funext U
rflEvaluation of a \(C\)-indexed completed group-algebra element as a compatible family is bundled as an additive monoid homomorphism.
instance instModuleCoeffCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
Module R (CompletedGroupAlgebraInClass C hC R G) :=
Function.Injective.module R
(completedGroupAlgebraInClassValAddMonoidHom (R := R) (G := G) C hC)
(fun x y h => by
apply Subtype.ext
funext U
exact congrFun h U)
(fun r x => by
funext U
rfl)The \(C\)-indexed completed group algebra is a module over the coefficient ring by coordinatewise finite-stage module structures.
def completedGroupAlgebraAlgebraMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
R →+* CompletedGroupAlgebraInClass C hC R G where
toFun r := ⟨fun U => algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r, by
intro U V hUV
exact completedGroupAlgebraTransitionInClass_algebraMap (R := R) (G := G) C hUV r⟩
map_zero' := by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
exact map_zero (algebraMap R (CompletedGroupAlgebraStageInClass C R G U))
map_one' := by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
exact map_one (algebraMap R (CompletedGroupAlgebraStageInClass C R G U))
map_add' r s := by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
exact map_add (algebraMap R (CompletedGroupAlgebraStageInClass C R G U)) r s
map_mul' r s := by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
exact map_mul (algebraMap R (CompletedGroupAlgebraStageInClass C R G U)) r sThe coefficient-ring map sends a coefficient to the corresponding constant element of the \(C\)-indexed completed group algebra.
instance instAlgebraCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
Algebra R (CompletedGroupAlgebraInClass C hC R G) where
algebraMap := completedGroupAlgebraAlgebraMapInClass (R := R) (G := G) C hC
commutes' := by
intro r x
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
change algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r *
(show CompletedGroupAlgebraStageInClass C R G U from x.1 U) =
(show CompletedGroupAlgebraStageInClass C R G U from x.1 U) *
algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r
exact Algebra.commutes r (show CompletedGroupAlgebraStageInClass C R G U from x.1 U)
smul_def' := by
intro r x
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
change r • (show CompletedGroupAlgebraStageInClass C R G U from x.1 U) =
algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r *
(show CompletedGroupAlgebraStageInClass C R G U from x.1 U)
rw [Algebra.smul_def]The completed group algebra is an algebra over the coefficient ring via the coordinatewise finite-stage algebra maps.