CompletedGroupAlgebra.Basic.InClass.Stage
Completed Group Algebra / Basic / Within a Class / Stage.
abbrev CompletedGroupAlgebraStageInClass (C : ProCGroups.FiniteGroupClass.{v})
(R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] (U : CompletedGroupAlgebraIndexInClass G C) :
Type (max u v) :=
MonoidAlgebra R (CompletedGroupAlgebraQuotientInClass G C U)A \(C\)-indexed quotient \(G/U\) determines the finite-stage group algebra \(R[G/U]\).
def completedGroupAlgebraStageCoeffMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S]
(f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C) :
CompletedGroupAlgebraStageInClass C R G U →+*
CompletedGroupAlgebraStageInClass C S G U :=
MonoidAlgebra.mapRangeRingHom (CompletedGroupAlgebraQuotientInClass G C U) f
@[simp]The coefficient-change map on one \(C\)-indexed completed-group-algebra stage is defined by changing coefficients.
theorem completedGroupAlgebraStageCoeffMapInClass_single
(C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S]
(f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C)
(q : CompletedGroupAlgebraQuotientInClass G C U) (r : R) :
completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U
(MonoidAlgebra.single q r) =
MonoidAlgebra.single q (f r)Coefficient change is performed stagewise: each coefficient is transported by the given ring homomorphism while the finite quotient support is left unchanged.
Show proof
by
exact MonoidAlgebra.mapRangeRingHom_single f q r
@[simp]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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem completedGroupAlgebraStageCoeffMapInClass_comp
(C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) (T : Type*) [CommRing S]
[CommRing T] (f : R →+* S) (g : S →+* T)
(U : CompletedGroupAlgebraIndexInClass G C) :
(completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp
(completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U) =
completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C T (g.comp f) UCoefficient change is performed stagewise: each coefficient is transported by the given ring homomorphism while the finite quotient support is left unchanged.
Show proof
by
exact (MonoidAlgebra.mapRangeRingHom_comp
(M := CompletedGroupAlgebraQuotientInClass G C U) g f).symmProof. 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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem finite_completedGroupAlgebraStageInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[Finite R] (U : CompletedGroupAlgebraIndexInClass G C) :
Finite (CompletedGroupAlgebraStageInClass C R G U)Show proof
by
classical
letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
finite_completedGroupAlgebraQuotientInClass G C hC U
letI : Fintype (CompletedGroupAlgebraQuotientInClass G C U) := Fintype.ofFinite _
letI : Fintype R := Fintype.ofFinite R
letI : DecidableEq (CompletedGroupAlgebraQuotientInClass G C U) := Classical.decEq _
letI : Finite (CompletedGroupAlgebraQuotientInClass G C U → R) := by
letI : Fintype (CompletedGroupAlgebraQuotientInClass G C U → R) := inferInstance
exact Finite.of_fintype _
let f :
CompletedGroupAlgebraStageInClass C R G U →
CompletedGroupAlgebraQuotientInClass G C U → R := fun x q => x q
refine Finite.of_injective f ?_
intro x y hxy
ext q
exact congrFun hxy qProof. 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.
□instance instRingCompletedGroupAlgebraStageInClass
(C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
Ring (CompletedGroupAlgebraStageInClass C R G U) := by
dsimp [CompletedGroupAlgebraStageInClass, CompletedGroupAlgebraQuotientInClass]
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 completedGroupAlgebraTransitionInClass
(C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
CompletedGroupAlgebraStageInClass C R G V →+*
CompletedGroupAlgebraStageInClass C R G U :=
MonoidAlgebra.mapDomainRingHom R
(OpenNormalSubgroupInClass.map
(C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)The transition map \(R[G/V] \to R[G/U]\) in the \(C\)-indexed completed-group-algebra tower.
theorem completedGroupAlgebraTransitionInClass_of
(C : ProCGroups.FiniteGroupClass.{v})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
(g : CompletedGroupAlgebraQuotientInClass G C V) :
completedGroupAlgebraTransitionInClass C R G hUV (MonoidAlgebra.of R _ g) =
MonoidAlgebra.single ((OpenNormalSubgroupInClass.map
(C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1The transition map sends group-like basis elements by quotient projection.
Show proof
by
classical
simp only [completedGroupAlgebraTransitionInClass, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
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. 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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem completedGroupAlgebraTransitionInClass_single
(C : ProCGroups.FiniteGroupClass.{v})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
(q : CompletedGroupAlgebraQuotientInClass G C V) (r : R) :
completedGroupAlgebraTransitionInClass C R G hUV (MonoidAlgebra.single q r) =
MonoidAlgebra.single
((OpenNormalSubgroupInClass.map
(C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) rThe \(C\)-indexed transition map between finite stages sends a singleton supported at a class of the finer quotient to the singleton supported at its image in the coarser quotient, preserving the coefficient.
Show proof
by
classical
simp only [completedGroupAlgebraTransitionInClass, MonoidAlgebra.single, MonoidAlgebra.mapDomainRingHom_apply,
Finsupp.mapDomain_single]
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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem completedGroupAlgebraTransitionInClass_id
(C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
completedGroupAlgebraTransitionInClass C R G (le_rfl : U ≤ U) = RingHom.id _The identity transition map in the \(C\)-indexed tower is the identity ring homomorphism.
Show proof
by
rw [completedGroupAlgebraTransitionInClass, OpenNormalSubgroupInClass.map_id]
exact MonoidAlgebra.mapDomainRingHom_id
(R := R) (M := CompletedGroupAlgebraQuotientInClass G C U)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. 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 completedGroupAlgebraTransitionInClass_comp
(C : ProCGroups.FiniteGroupClass.{v})
{U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
(completedGroupAlgebraTransitionInClass C R G hUV).comp
(completedGroupAlgebraTransitionInClass C R G hVW) =
completedGroupAlgebraTransitionInClass C R G (hUV.trans hVW)Transition maps in the \(C\)-indexed tower compose as expected.
Show proof
by
rw [completedGroupAlgebraTransitionInClass, completedGroupAlgebraTransitionInClass,
completedGroupAlgebraTransitionInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
congr 1
exact OpenNormalSubgroupInClass.map_comp
(C := C) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)
hUV hVWProof. 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. 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 completedGroupAlgebraStageCoeffMapInClass_compatible
(C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S] (f : R →+* S)
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
(completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U).comp
(completedGroupAlgebraTransitionInClass C R G hUV) =
(completedGroupAlgebraTransitionInClass C S G hUV).comp
(completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f V)\(C\)-indexed stage transitions commute with coefficient change.
Show proof
by
exact MonoidAlgebra.mapRangeRingHom_comp_mapDomainRingHom
(f := f)
(g := OpenNormalSubgroupInClass.map
(C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)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.
□theorem completedGroupAlgebraStageCoeffMapInClass_transition_comp
(C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) (T : Type*) [CommRing S]
[CommRing T] (f : R →+* S) (g : S →+* T)
{U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
((completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp
(completedGroupAlgebraTransitionInClass C S G hUV)).comp
((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f V).comp
(completedGroupAlgebraTransitionInClass C R G hVW)) =
(completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C T (g.comp f) U).comp
(completedGroupAlgebraTransitionInClass C R G (hUV.trans hVW))Two coefficient changes and two \(C\)-indexed group-quotient transitions compose as the combined change and combined transition.
Show proof
by
calc
((completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp
(completedGroupAlgebraTransitionInClass C S G hUV)).comp
((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f V).comp
(completedGroupAlgebraTransitionInClass C R G hVW))
=
(completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp
(((completedGroupAlgebraTransitionInClass C S G hUV).comp
(completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f V)).comp
(completedGroupAlgebraTransitionInClass C R G hVW)) := by
apply RingHom.ext
intro x
rfl
_ =
(completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp
(((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U).comp
(completedGroupAlgebraTransitionInClass C R G hUV)).comp
(completedGroupAlgebraTransitionInClass C R G hVW)) := by
rw [← completedGroupAlgebraStageCoeffMapInClass_compatible
(R := R) (G := G) C S f hUV]
_ =
((completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp
(completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)).comp
((completedGroupAlgebraTransitionInClass C R G hUV).comp
(completedGroupAlgebraTransitionInClass C R G hVW)) := by
apply RingHom.ext
intro x
rfl
_ =
(completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C T (g.comp f) U).comp
((completedGroupAlgebraTransitionInClass C R G hUV).comp
(completedGroupAlgebraTransitionInClass C R G hVW)) := by
rw [completedGroupAlgebraStageCoeffMapInClass_comp]
_ =
(completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C T (g.comp f) U).comp
(completedGroupAlgebraTransitionInClass C R G (hUV.trans hVW)) := by
rw [completedGroupAlgebraTransitionInClass_comp]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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem completedGroupAlgebraTransitionInClass_smul
(C : ProCGroups.FiniteGroupClass.{v})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
(r : R) (x : CompletedGroupAlgebraStageInClass C R G V) :
completedGroupAlgebraTransitionInClass C R G hUV (r • x) =
r • completedGroupAlgebraTransitionInClass C R G hUV xTransition maps commute with scalar multiplication by coefficients.
Show proof
by
rw [Algebra.smul_def, Algebra.smul_def, map_mul]
congr 1
simp only [completedGroupAlgebraTransitionInClass, 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.
□theorem completedGroupAlgebraTransitionInClass_algebraMap
(C : ProCGroups.FiniteGroupClass.{v})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (r : R) :
completedGroupAlgebraTransitionInClass C R G hUV
(algebraMap R (CompletedGroupAlgebraStageInClass C R G V) r) =
algebraMap R (CompletedGroupAlgebraStageInClass C R G U) rTransition maps commute with the coefficient algebra maps.
Show proof
by
simp only [completedGroupAlgebraTransitionInClass, 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.
□