CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
def completedGroupAlgebraStageMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(U : CompletedGroupAlgebraIndexInClass G C) :
MonoidAlgebra R G →+* CompletedGroupAlgebraStageInClass C R G U :=
MonoidAlgebra.mapDomainRingHom R
(openNormalSubgroupInClassProj (C := C) (G := G) U)theorem completedGroupAlgebraStageMapInClass_of
(C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
(g : G) :
completedGroupAlgebraStageMapInClass C R G U (MonoidAlgebra.of R G g) =
MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1Show proof
by
classical
simp only [completedGroupAlgebraStageMapInClass, 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraStageMapInClass_single
(C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
(g : G) (r : R) :
completedGroupAlgebraStageMapInClass C R G U (MonoidAlgebra.single g r) =
MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) rThe finite-stage map sends a singleton basis element to the singleton determined by its quotient image and coefficient.
Show proof
by
classical
simp only [completedGroupAlgebraStageMapInClass, 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraStageMapInClass_smul
(C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
(r : R) (x : MonoidAlgebra R G) :
completedGroupAlgebraStageMapInClass C R G U (r • x) =
r • completedGroupAlgebraStageMapInClass C R G U xThe finite-stage map from the abstract group algebra to the quotient stage is compatible with scalar multiplication.
Show proof
by
rw [Algebra.smul_def, Algebra.smul_def, map_mul]
congr 1
simp only [completedGroupAlgebraStageMapInClass, 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraStageMapInClass_algebraMap
(C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
(r : R) :
completedGroupAlgebraStageMapInClass C R G U (algebraMap R (MonoidAlgebra R G) r) =
algebraMap R (CompletedGroupAlgebraStageInClass C R G U) rCoefficient change is performed stagewise: each coefficient is transported by the given ring homomorphism while the finite quotient support is left unchanged.
Show proof
by
simp only [completedGroupAlgebraStageMapInClass, 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraStageMapInClass_surjective
(C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
Function.Surjective (completedGroupAlgebraStageMapInClass C R G U)The dense finite-stage map from the abstract group algebra onto the quotient-stage group algebra is surjective.
Show proof
by
classical
intro x
induction x using Finsupp.induction with
| zero =>
exact ⟨0, map_zero (completedGroupAlgebraStageMapInClass C R G U)⟩
| single_add q r x _ _ ih =>
rcases openNormalSubgroupInClassProj_surjective (C := C) (G := G) U q with ⟨g, hg⟩
rcases ih with ⟨y, hy⟩
refine ⟨(MonoidAlgebra.single g r : MonoidAlgebra R G) + y, ?_⟩
rw [map_add, completedGroupAlgebraStageMapInClass_single, hy, hg]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. Surjectivity is obtained by lifting a representative through the underlying surjective quotient or group homomorphism and then checking the defining finite-stage formula. 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. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. 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. For surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□theorem completedGroupAlgebraStageMapInClass_compatible
(C : ProCGroups.FiniteGroupClass.{v})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
(completedGroupAlgebraTransitionInClass C R G hUV).comp
(completedGroupAlgebraStageMapInClass C R G V) =
completedGroupAlgebraStageMapInClass C R G UThe class-restricted completed group-algebra stage map is compatible with transition maps and coordinate projections for the completed group algebra.
Show proof
by
rw [completedGroupAlgebraTransitionInClass, completedGroupAlgebraStageMapInClass,
completedGroupAlgebraStageMapInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
congr 1Proof. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraStageMapInClass_compatibleMaps
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
(completedGroupAlgebraSystemInClass C hC R G).CompatibleMaps
(fun U => completedGroupAlgebraStageMapInClass C R G U)The \(C\)-indexed finite-stage quotient maps form a compatible family.
Show proof
by
intro U V hUV
funext x
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageMapInClass_compatible (R := R) (G := G) C hUV))
xProof. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def toCompletedGroupAlgebraInClass
(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]
(x : MonoidAlgebra R G) : CompletedGroupAlgebraInClass C hC R G :=
⟨fun U => completedGroupAlgebraStageMapInClass C R G U x, by
intro U V hUV
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageMapInClass_compatible (R := R) (G := G) C hUV))
x⟩
@[simp]The canonical map \(R[G] \to \widehat{R[G]}_C\), obtained from all \(C\)-indexed quotient maps.
theorem completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) (x : MonoidAlgebra R G) :
completedGroupAlgebraProjectionInClass C hC R G U
(toCompletedGroupAlgebraInClass C hC R G x) =
completedGroupAlgebraStageMapInClass C R G U xProjecting the canonical dense map to a finite quotient stage gives the corresponding stage map.
Show proof
rfl
@[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. 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. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem toCompletedGroupAlgebraInClass_smul
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(r : R) (x : MonoidAlgebra R G) :
toCompletedGroupAlgebraInClass C hC R G (r • x) =
r • toCompletedGroupAlgebraInClass C hC R G xThe specified completed-group-algebra map is compatible with scalar multiplication by coefficients.
Show proof
by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
change completedGroupAlgebraStageMapInClass C R G U (r • x) =
r • completedGroupAlgebraStageMapInClass C R G U x
exact completedGroupAlgebraStageMapInClass_smul (R := R) (G := G) C U r xProof. 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. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def toCompletedGroupAlgebraInClassRingHom
(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] :
MonoidAlgebra R G →+* CompletedGroupAlgebraInClass C hC R G where
toFun := toCompletedGroupAlgebraInClass C hC R G
map_zero' := by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
exact map_zero (completedGroupAlgebraStageMapInClass C R G U)
map_one' := by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
exact map_one (completedGroupAlgebraStageMapInClass C R G U)
map_add' x y := by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
exact map_add (completedGroupAlgebraStageMapInClass C R G U) x y
map_mul' x y := by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
exact map_mul (completedGroupAlgebraStageMapInClass C R G U) x y
@[simp]The canonical map \(R[G] \to \widehat{R[G]}_C\) is bundled as a ring homomorphism.
theorem toCompletedGroupAlgebraInClassRingHom_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(x : MonoidAlgebra R G) :
toCompletedGroupAlgebraInClassRingHom C hC R G x =
toCompletedGroupAlgebraInClass C hC R G xThe bundled ring homomorphism has the same underlying function as the coordinatewise construction.
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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def toCompletedGroupAlgebraInClassAlgHom
(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] :
MonoidAlgebra R G →ₐ[R] CompletedGroupAlgebraInClass C hC R G where
toRingHom := toCompletedGroupAlgebraInClassRingHom C hC R G
commutes' := by
intro r
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
change completedGroupAlgebraStageMapInClass C R G U
(algebraMap R (MonoidAlgebra R G) r) =
algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r
exact completedGroupAlgebraStageMapInClass_algebraMap (R := R) (G := G) C U r
@[simp]The canonical map \(R[G] \to \widehat{R[G]}_C\), as an algebra homomorphism.
theorem toCompletedGroupAlgebraInClassAlgHom_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(x : MonoidAlgebra R G) :
toCompletedGroupAlgebraInClassAlgHom C hC R G x =
toCompletedGroupAlgebraInClass C hC R G xThe bundled algebra homomorphism has the same underlying function as the coordinatewise construction.
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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def toCompletedGroupAlgebraInClassLinearMap
(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] :
MonoidAlgebra R G →ₗ[R] CompletedGroupAlgebraInClass C hC R G where
toFun := toCompletedGroupAlgebraInClass C hC R G
map_add' := by
intro x y
exact map_add (toCompletedGroupAlgebraInClassRingHom C hC R G) x y
map_smul' := toCompletedGroupAlgebraInClass_smul (R := R) (G := G) C hC
@[simp]The canonical map \(R[G] \to \widehat{R[G]}_C\), as a linear map.
theorem toCompletedGroupAlgebraInClassLinearMap_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(x : MonoidAlgebra R G) :
toCompletedGroupAlgebraInClassLinearMap C hC R G x =
toCompletedGroupAlgebraInClass C hC R G xThe bundled linear map has the same underlying function as the coordinatewise construction.
Show proof
rfl
@[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. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGAProjRingHomInClass_comp_toCompletedGAInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) :
(completedGroupAlgebraProjectionRingHomInClass C hC R G U).comp
(toCompletedGroupAlgebraInClassRingHom C hC R G) =
completedGroupAlgebraStageMapInClass C R G UComposing the comparison map with the dense map from the abstract group algebra recovers the canonical completed group-algebra map.
Show proof
by
apply RingHom.ext
intro x
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. 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. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem denseRange_toCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
DenseRange (toCompletedGroupAlgebraInClass C hC R G)The abstract group algebra is dense in the \(C\)-indexed completed group algebra when \(G\) is pro-\(C\) and \(C\) is a formation.
Show proof
by
let S := completedGroupAlgebraSystemInClass C hC R G
letI : Nonempty (OpenNormalSubgroupInClass C G) :=
IsProCGroup.openNormalSubgroupInClass_nonempty hG
letI : Nonempty (CompletedGroupAlgebraIndexInClass G C) := inferInstance
have hdir :
Directed (α := CompletedGroupAlgebraIndexInClass G C) (· ≤ ·) fun U => U :=
directed_openNormalSubgroupInClass (C := C) (G := G) hForm
have hdense :
DenseRange
(S.inverseLimitLift
(fun U : CompletedGroupAlgebraIndexInClass G C =>
completedGroupAlgebraStageMapInClass C R G U)
(completedGroupAlgebraStageMapInClass_compatibleMaps (R := R) (G := G) C hC)) :=
S.denseRange_lift
(fun U : CompletedGroupAlgebraIndexInClass G C =>
completedGroupAlgebraStageMapInClass C R G U)
(completedGroupAlgebraStageMapInClass_compatibleMaps (R := R) (G := G) C hC)
(fun U => completedGroupAlgebraStageMapInClass_surjective (R := R) (G := G) C U)
hdir
simpa [S, toCompletedGroupAlgebraInClass] using hdense
@[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, 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. 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. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraTransition_comp_projectionRingHom
{U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
(completedGroupAlgebraTransition R G hUV).comp
(completedGroupAlgebraProjectionRingHom R G V) =
completedGroupAlgebraProjectionRingHom R G UThe finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
apply RingHom.ext
intro x
exact completedGroupAlgebraProjection_compatible (R := R) (G := G) x hUVProof. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def completedGroupAlgebraStageMap (R : Type u) (G : Type v) [CommRing R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
MonoidAlgebra R G →+* CompletedGroupAlgebraStage R G U :=
MonoidAlgebra.mapDomainRingHom R
(openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U)theorem completedGroupAlgebraStageMap_of
(U : CompletedGroupAlgebraIndex G) (g : G) :
completedGroupAlgebraStageMap R G U (MonoidAlgebra.of R G g) =
MonoidAlgebra.single (openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1Show proof
by
classical
simp only [completedGroupAlgebraStageMap, 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraStageMap_single
(U : CompletedGroupAlgebraIndex G) (g : G) (r : R) :
completedGroupAlgebraStageMap R G U (MonoidAlgebra.single g r) =
MonoidAlgebra.single (openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) rThe finite-stage map sends a singleton basis element to the singleton determined by its quotient image and coefficient.
Show proof
by
classical
simp only [completedGroupAlgebraStageMap, 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraStageMap_smul
(U : CompletedGroupAlgebraIndex G) (r : R) (x : MonoidAlgebra R G) :
completedGroupAlgebraStageMap R G U (r • x) =
r • completedGroupAlgebraStageMap R G U xThe finite-stage map from the abstract group algebra to the quotient stage is compatible with scalar multiplication.
Show proof
by
rw [Algebra.smul_def, Algebra.smul_def, map_mul]
congr 1
simp only [completedGroupAlgebraStageMap, 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraStageMap_algebraMap
(U : CompletedGroupAlgebraIndex G) (r : R) :
completedGroupAlgebraStageMap R G U (algebraMap R (MonoidAlgebra R G) r) =
algebraMap R (CompletedGroupAlgebraStage R G U) rCoefficient change is performed stagewise: each coefficient is transported by the given ring homomorphism while the finite quotient support is left unchanged.
Show proof
by
simp only [completedGroupAlgebraStageMap, 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraStageMap_surjective (U : CompletedGroupAlgebraIndex G) :
Function.Surjective (completedGroupAlgebraStageMap R G U)The dense finite-stage map from the abstract group algebra onto the quotient-stage group algebra is surjective.
Show proof
by
classical
intro x
induction x using Finsupp.induction with
| zero =>
exact ⟨0, map_zero (completedGroupAlgebraStageMap R G U)⟩
| single_add q r x _ _ ih =>
rcases openNormalSubgroupInClassProj_surjective
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U q with
⟨g, hg⟩
rcases ih with ⟨y, hy⟩
refine ⟨(MonoidAlgebra.single g r : MonoidAlgebra R G) + y, ?_⟩
rw [map_add, completedGroupAlgebraStageMap_single, hy, hg]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. Surjectivity is obtained by lifting a representative through the underlying surjective quotient or group homomorphism and then checking the defining finite-stage formula. 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. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. 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. For surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□theorem completedGroupAlgebraStageMap_compatible
{U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
(completedGroupAlgebraTransition R G hUV).comp (completedGroupAlgebraStageMap R G V) =
completedGroupAlgebraStageMap R G UThe completed group-algebra stage map is compatible with transition maps and coordinate projections for the completed group algebra.
Show proof
by
rw [completedGroupAlgebraTransition, completedGroupAlgebraStageMap,
completedGroupAlgebraStageMap, ← MonoidAlgebra.mapDomainRingHom_comp]
congr 1Proof. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraStageMap_compatibleMaps :
(completedGroupAlgebraSystem R G).CompatibleMaps
(fun U => completedGroupAlgebraStageMap R G U)The finite-stage quotient maps form a compatible family into the completed group algebra system.
Show proof
by
intro U V hUV
funext x
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageMap_compatible (R := R) (G := G) (U := U) (V := V) hUV))
xProof. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def toCompletedGroupAlgebra (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
[IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(x : MonoidAlgebra R G) : Carrier R G :=
⟨fun U => completedGroupAlgebraStageMap R G U x, by
intro U V hUV
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageMap_compatible (R := R) (G := G) (U := U) (V := V) hUV))
x⟩
@[simp]The canonical map \(R[G] \to \widehat{R[G]}\), obtained from all quotient maps \(R[G]\to R[G/U]\).
theorem completedGroupAlgebraProjection_toCompletedGroupAlgebra
(U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) :
completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G x) =
completedGroupAlgebraStageMap R G U xProjecting the canonical dense map to a finite quotient stage gives the corresponding stage map.
Show proof
rfl
@[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. 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. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem toCompletedGroupAlgebra_smul (r : R) (x : MonoidAlgebra R G) :
toCompletedGroupAlgebra R G (r • x) =
r • toCompletedGroupAlgebra R G xThe specified completed-group-algebra map is compatible with scalar multiplication by coefficients.
Show proof
by
apply (completedGroupAlgebraSystem R G).ext
intro U
change completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G (r • x)) =
completedGroupAlgebraProjection R G U (r • toCompletedGroupAlgebra R G x)
rw [completedGroupAlgebraProjection_toCompletedGroupAlgebra,
completedGroupAlgebraProjection_smul,
completedGroupAlgebraProjection_toCompletedGroupAlgebra,
completedGroupAlgebraStageMap_smul]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, 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def toCompletedGroupAlgebraRingHom (R : Type u) (G : Type v) [CommRing R]
[TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] :
MonoidAlgebra R G →+* Carrier R G where
toFun := toCompletedGroupAlgebra R G
map_zero' := by
apply (completedGroupAlgebraSystem R G).ext
intro U
exact map_zero (completedGroupAlgebraStageMap R G U)
map_one' := by
apply (completedGroupAlgebraSystem R G).ext
intro U
exact map_one (completedGroupAlgebraStageMap R G U)
map_add' x y := by
apply (completedGroupAlgebraSystem R G).ext
intro U
exact map_add (completedGroupAlgebraStageMap R G U) x y
map_mul' x y := by
apply (completedGroupAlgebraSystem R G).ext
intro U
exact map_mul (completedGroupAlgebraStageMap R G U) x y
@[simp]The canonical map \(R[G] \to \widehat{R[G]}\) is bundled as a ring homomorphism.
theorem completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC).comp
(toCompletedGroupAlgebraRingHom R G) =
toCompletedGroupAlgebraInClassRingHom C hC R GComposing the comparison map with the dense map from the abstract group algebra recovers the canonical completed group-algebra map.
Show proof
by
apply RingHom.ext
intro x
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
rfl
@[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. 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. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraFromInClassRingHom_comp_toCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
(completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG).comp
(toCompletedGroupAlgebraInClassRingHom C hC R G) =
toCompletedGroupAlgebraRingHom R GComposing the comparison map with the dense map from the abstract group algebra recovers the canonical completed group-algebra map.
Show proof
by
rw [← completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra (R := R) (G := G) C hC,
← RingHom.comp_assoc, completedGroupAlgebraFromInClassRingHom_comp_toInClassRingHom]
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. 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. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def toCompletedGroupAlgebraAlgHom (R : Type u) (G : Type v) [CommRing R]
[TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] :
MonoidAlgebra R G →ₐ[R] Carrier R G where
toRingHom := toCompletedGroupAlgebraRingHom R G
commutes' := by
intro r
apply (completedGroupAlgebraSystem R G).ext
intro U
change completedGroupAlgebraStageMap R G U (algebraMap R (MonoidAlgebra R G) r) =
algebraMap R (CompletedGroupAlgebraStage R G U) r
exact completedGroupAlgebraStageMap_algebraMap (R := R) (G := G) U rThe canonical map \(R[G] \to \widehat{R[G]}\) as an \(R\)-algebra homomorphism.
def toCompletedGroupAlgebraLinearMap (R : Type u) (G : Type v) [CommRing R]
[TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] :
MonoidAlgebra R G →ₗ[R] Carrier R G where
toFun := toCompletedGroupAlgebra R G
map_add' := by
intro x y
exact map_add (toCompletedGroupAlgebraRingHom R G) x y
map_smul' := toCompletedGroupAlgebra_smul (R := R) (G := G)
@[simp]The canonical map \(R[G] \to \widehat{R[G]}\) as an \(R\)-linear map.
theorem completedGroupAlgebraProjectionRingHom_comp_toCompletedGroupAlgebra
(U : CompletedGroupAlgebraIndex G) :
(completedGroupAlgebraProjectionRingHom R G U).comp
(toCompletedGroupAlgebraRingHom R G) =
completedGroupAlgebraStageMap R G UComposing the comparison map with the dense map from the abstract group algebra recovers the canonical completed group-algebra map.
Show proof
by
apply RingHom.ext
intro x
exact completedGroupAlgebraProjection_toCompletedGroupAlgebra (R := R) (G := G) U xProof. 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. 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. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. 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.
□