CompletedGroupAlgebra.FunctorialityComposition
This module proves that completed group algebra functoriality is compatible with composition.
Imported by
theorem completedGroupAlgebraMap_comp
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
(hH : ProCGroups.IsProfiniteGroup H)
(φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
(completedGroupAlgebraMap (G := H) (H := K) R hH ψ hψ).comp
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ) =
completedGroupAlgebraMap (G := G) (H := K) R hG (ψ.comp φ) (hψ.comp hφ)Lemma 5.3.5(e), composition law for the completed-group-algebra functor.
Show proof
by
apply completedGroupAlgebraRingHom_ext_of_comp_toCompleted (R := R) (G := G) (H := K)
hR hG
· exact (continuous_completedGroupAlgebraMap (R := R) (G := H) (H := K) hH ψ hψ).comp
(continuous_completedGroupAlgebraMap (R := R) (G := G) (H := H) hG φ hφ)
· exact continuous_completedGroupAlgebraMap (R := R) (G := G) (H := K)
hG (ψ.comp φ) (hψ.comp hφ)
· apply RingHom.ext
intro x
have hφdense := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMap_comp_toCompletedGroupAlgebra (R := R) (G := G) (H := H)
hG φ hφ))
x
have hψdense := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMap_comp_toCompletedGroupAlgebra (R := R) (G := H) (H := K)
hH ψ hψ))
(MonoidAlgebra.mapDomainRingHom R φ x)
have hdomain := congrFun
(congrArg DFunLike.coe
(finiteGroupAlgebra_mapDomainRingHom_comp R G H K φ ψ))
x
have hcompdense := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMap_comp_toCompletedGroupAlgebra (R := R) (G := G) (H := K)
hG (ψ.comp φ) (hψ.comp hφ)))
x
calc
(((completedGroupAlgebraMap (G := H) (H := K) R hH ψ hψ).comp
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)).comp
(toCompletedGroupAlgebraRingHom R G)) x
=
completedGroupAlgebraMap (G := H) (H := K) R hH ψ hψ
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
(toCompletedGroupAlgebraRingHom R G x)) := rfl
_ =
completedGroupAlgebraMap (G := H) (H := K) R hH ψ hψ
(toCompletedGroupAlgebraRingHom R H (MonoidAlgebra.mapDomainRingHom R φ x)) := by
have hφdense' :
completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
(toCompletedGroupAlgebraRingHom R G x) =
toCompletedGroupAlgebraRingHom R H (MonoidAlgebra.mapDomainRingHom R φ x) := by
simpa [RingHom.comp_apply] using hφdense
exact congrArg (completedGroupAlgebraMap (G := H) (H := K) R hH ψ hψ) hφdense'
_ =
toCompletedGroupAlgebraRingHom R K
(MonoidAlgebra.mapDomainRingHom R ψ (MonoidAlgebra.mapDomainRingHom R φ x)) := by
simpa [RingHom.comp_apply] using hψdense
_ =
toCompletedGroupAlgebraRingHom R K
(MonoidAlgebra.mapDomainRingHom R (ψ.comp φ) x) := by
exact congrArg (toCompletedGroupAlgebraRingHom R K) (by
change (MonoidAlgebra.mapDomainRingHom R ψ)
((MonoidAlgebra.mapDomainRingHom R φ) x) =
(MonoidAlgebra.mapDomainRingHom R (ψ.comp φ)) x at hdomain
exact hdomain)
_ =
((completedGroupAlgebraMap (G := G) (H := K) R hG (ψ.comp φ) (hψ.comp hφ)).comp
(toCompletedGroupAlgebraRingHom R G)) x := by
simpa [RingHom.comp_apply] using hcompdense.symmProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem completedGroupAlgebraMapAlgHom_comp
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
(hH : ProCGroups.IsProfiniteGroup H)
(φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
(completedGroupAlgebraMapAlgHom (G := H) (H := K) R hH ψ hψ).comp
(completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG φ hφ) =
completedGroupAlgebraMapAlgHom (G := G) (H := K) R hG (ψ.comp φ) (hψ.comp hφ)Lemma 5.3.5(e), composition law for the completed-group-algebra functor, as an \(R\)-algebra homomorphism.
Show proof
by
apply AlgHom.ext
intro x
have h := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMap_comp (R := R) (G := G) (H := H) (K := K)
hR hG hH φ hφ ψ hψ))
x
simpa [RingHom.comp_apply] using hProof. 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□