CompletedGroupAlgebra.AllFiniteFunctoriality.Map
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 completedGroupAlgebraMap
(R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) :
Carrier R G →+* Carrier R H where
toFun x := ⟨fun V =>
completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x), by
intro V W hVW
change completedGroupAlgebraTransition R H hVW
(completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ W
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ W) x)) =
completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)
have hcomp := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraFunctorialStageMap_transition (R := R) (G := G) (H := H)
hG φ hφ hVW))
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ W) x)
rw [RingHom.comp_apply, RingHom.comp_apply] at hcomp
rw [← completedGroupAlgebraProjection_compatible (R := R) (G := G) x
(completedGroupAlgebraComapIndex_mono (G := G) hG φ hφ hVW)]
exact hcomp⟩
map_zero' := by
apply (completedGroupAlgebraSystem R H).ext
intro V
exact map_zero (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
hG φ hφ V)
map_one' := by
apply (completedGroupAlgebraSystem R H).ext
intro V
exact map_one (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
hG φ hφ V)
map_add' x y := by
apply (completedGroupAlgebraSystem R H).ext
intro V
exact map_add (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
hG φ hφ V)
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) y)
map_mul' x y := by
apply (completedGroupAlgebraSystem R H).ext
intro V
exact map_mul (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
hG φ hφ V)
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) y)In Lemma 5.3.5(e), map construction, a continuous homomorphism of profinite groups \(\varphi : G \to H\) induces a continuous ring homomorphism \(\widehat{R[G]} \to \widehat{R[H]}\).
theorem completedGroupAlgebraProjection_map
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
(V : CompletedGroupAlgebraIndex H) (x : Carrier R G) :
completedGroupAlgebraProjection R H V
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x) =
completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)Projection of the completed functorial map is computed by the corresponding stage map.
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, 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. 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. 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.
□def completedGroupAlgebraMapAlgHom
(R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) :
Carrier R G →ₐ[R] Carrier R H where
toRingHom := completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
commutes' := by
intro r
apply (completedGroupAlgebraSystem R H).ext
intro V
change 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) r
exact completedGroupAlgebraFunctorialStageMap_algebraMap
(R := R) (G := G) (H := H) hG φ hφ V rIn Lemma 5.3.5(e), algebra form, a continuous homomorphism of profinite groups induces an \(R\)-algebra homomorphism on completed group algebras.
theorem completedGroupAlgebraMapAlgHom_apply
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
(x : Carrier R G) :
completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG φ hφ x =
completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ xThe algebra homomorphism form of the completed functorial map has the same underlying function as the corresponding completed ring homomorphism.
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, 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 continuous_completedGroupAlgebraMap
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) :
Continuous (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)The completed group-algebra map induced by a continuous group homomorphism is continuous.
Show proof
by
let A := Carrier R G
letI : ∀ V : CompletedGroupAlgebraIndex H,
TopologicalSpace (CompletedGroupAlgebraStage R H V) :=
fun V => (completedGroupAlgebraSystem R H).topologicalSpace V
have hval : Continuous fun x : A =>
((completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x) :
(V : CompletedGroupAlgebraIndex H) → (completedGroupAlgebraSystem R H).X V) := by
change Continuous fun x : A =>
fun V : CompletedGroupAlgebraIndex H =>
completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)
apply continuous_pi
intro V
letI : TopologicalSpace
(CompletedGroupAlgebraStage R G (completedGroupAlgebraComapIndex (G := G) hG φ hφ V)) :=
(completedGroupAlgebraSystem R G).topologicalSpace
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V)
exact (continuous_completedGroupAlgebraFunctorialStageMap (R := R) (G := G) (H := H)
hG φ hφ V).comp
((completedGroupAlgebraSystem R G).continuous_projection
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V))
exact Continuous.subtype_mk hval fun x =>
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x).2Proof. 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. 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 completedGroupAlgebraMap_comp_toCompletedGroupAlgebra
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) :
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ).comp
(toCompletedGroupAlgebraRingHom R G) =
(toCompletedGroupAlgebraRingHom R H).comp (MonoidAlgebra.mapDomainRingHom R φ)The completed functorial map agrees on the dense abstract group algebra with the ordinary group-algebra map induced by the group homomorphism.
Show proof
by
apply RingHom.ext
intro x
apply (completedGroupAlgebraSystem R H).ext
intro V
have hstage := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraFunctorialStageMap_comp_stageMap (R := R) (G := G) (H := H)
hG φ hφ V))
x
change completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
(completedGroupAlgebraStageMap R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x) =
completedGroupAlgebraStageMap R H V (MonoidAlgebra.mapDomainRingHom R φ x)
exact hstageProof. 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. 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. 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.
□