CompletedGroupAlgebra.AllFiniteFunctoriality.StageMap
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 completedGroupAlgebraFunctorialStageMap
(R : Type u) [CommRing R] (hG : ProCGroups.IsProfiniteGroup G)
(φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndex H) :
CompletedGroupAlgebraStage R G (completedGroupAlgebraComapIndex (G := G) hG φ hφ V) →+*
CompletedGroupAlgebraStage R H V :=
MonoidAlgebra.mapDomainRingHom R
(completedGroupAlgebraComapQuotientMap (G := G) hG φ hφ V)The finite-stage map \(R[G/\varphi^{-1}(V)]\to R[H/V]\) is induced by the continuous homomorphism \(\varphi : G \to H\).
theorem completedGroupAlgebraFunctorialStageMap_surjective_of_surjective
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
(hφsurj : Function.Surjective φ) (V : CompletedGroupAlgebraIndex H) :
Function.Surjective
(completedGroupAlgebraFunctorialStageMap
(G := G) (H := H) (R := R) hG φ hφ V)A surjective group homomorphism induces a surjective finite-stage algebra map.
Show proof
by
simpa [completedGroupAlgebraFunctorialStageMap, MonoidAlgebra.mapDomainRingHom_apply] using
(Finsupp.mapDomain_surjective (M := R)
(completedGroupAlgebraComapQuotientMap_surjective
(G := G) hG φ hφ hφsurj V))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. 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. 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 completedGroupAlgebraFunctorialStageMap_single
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
(V : CompletedGroupAlgebraIndex H)
(q : CompletedGroupAlgebraQuotient G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V)) (r : R) :
completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
(MonoidAlgebra.single q r) =
MonoidAlgebra.single (completedGroupAlgebraComapQuotientMap (G := G) hG φ hφ V q) rThe finite-stage functorial map induced by \(\varphi : G \to H\) carries a singleton basis function on \(G/\varphi^{-1}(V)\) to the singleton basis function on \(H/V\) supported at the induced image, with unchanged coefficient.
Show proof
by
classical
simp only [completedGroupAlgebraFunctorialStageMap, MonoidAlgebra.single,
MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]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. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem completedGroupAlgebraFunctorialStageMap_algebraMap
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
(V : CompletedGroupAlgebraIndex H) (r : R) :
completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
(algebraMap R
(CompletedGroupAlgebraStage R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V)) r) =
algebraMap R (CompletedGroupAlgebraStage R H V) rThe finite-stage functorial map preserves scalar algebra-map elements.
Show proof
by
simp only [completedGroupAlgebraFunctorialStageMap, 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. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem continuous_completedGroupAlgebraFunctorialStageMap
[TopologicalSpace R] [IsTopologicalRing R]
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
(V : CompletedGroupAlgebraIndex H) :
letI : TopologicalSpace
(CompletedGroupAlgebraStage R G (completedGroupAlgebraComapIndex (G := G) hG φ hφ V))Show proof
(completedGroupAlgebraSystem R G).topologicalSpace
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V)
letI : TopologicalSpace (CompletedGroupAlgebraStage R H V) :=
(completedGroupAlgebraSystem R H).topologicalSpace V
Continuous (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
hG φ hφ V) := by
letI : TopologicalSpace
(CompletedGroupAlgebraStage R G (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)) :=
(completedGroupAlgebraSystem R G).topologicalSpace
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V)
letI : TopologicalSpace (CompletedGroupAlgebraStage R H V) :=
(completedGroupAlgebraSystem R H).topologicalSpace V
exact finiteGroupAlgebra_mapDomainRingHom_continuous R
(CompletedGroupAlgebraQuotient G (completedGroupAlgebraComapIndex (G := G) hG φ hφ V))
(CompletedGroupAlgebraQuotient H V)
(completedGroupAlgebraComapQuotientMap (G := G) hG φ hφ V)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. 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 completedGroupAlgebraFunctorialStageMap_transition
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
{V W : CompletedGroupAlgebraIndex H} (hVW : V ≤ W) :
(completedGroupAlgebraTransition R H hVW).comp
(completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ W) =
(completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V).comp
(completedGroupAlgebraTransition R G
(completedGroupAlgebraComapIndex_mono (G := G) hG φ hφ hVW))Show proof
by
rw [completedGroupAlgebraTransition, completedGroupAlgebraFunctorialStageMap,
completedGroupAlgebraFunctorialStageMap, completedGroupAlgebraTransition,
← MonoidAlgebra.mapDomainRingHom_comp, ← MonoidAlgebra.mapDomainRingHom_comp]
congr 1
apply MonoidHom.ext
intro q
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) hG φ hφ W)).1 :
OpenNormalSubgroup G) : Subgroup G)) q with
⟨g, rfl⟩
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. 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 completedGroupAlgebraFunctorialStageMap_comp_stageMap
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
(V : CompletedGroupAlgebraIndex H) :
(completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V).comp
(completedGroupAlgebraStageMap R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V)) =
(completedGroupAlgebraStageMap R H V).comp
(MonoidAlgebra.mapDomainRingHom R φ)The finite-stage functorial map agrees with the dense stage map after applying \(\varphi\).
Show proof
by
rw [completedGroupAlgebraFunctorialStageMap, completedGroupAlgebraStageMap,
completedGroupAlgebraStageMap, ← MonoidAlgebra.mapDomainRingHom_comp,
← 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. 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. 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.
□