CompletedGroupAlgebra.AllFiniteFunctoriality.InClassNaturality
Completed Group Algebra / All Finite Functoriality / Within a Class Naturality.
theorem completedGroupAlgebraRingHomToInClass_ext_of_comp_toCompleted
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
{f g : Carrier R G →+* CompletedGroupAlgebraInClass C hC R H}
(hf : Continuous f) (hg : Continuous g)
(hfg : f.comp (toCompletedGroupAlgebraRingHom R G) =
g.comp (toCompletedGroupAlgebraRingHom R G)) :
f = gContinuous ring homomorphisms from the all-finite completed group algebra to a \(C\)-indexed completed group algebra are determined by their values on the dense abstract group algebra.
Show proof
by
letI : T2Space (CompletedGroupAlgebraInClass C hC R H) :=
completedGroupAlgebraInClass_t2Space (R := R) (G := H) C hC hR
have hdense : DenseRange (toCompletedGroupAlgebraRingHom R G) :=
denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG
have hcomp : (f : Carrier R G → CompletedGroupAlgebraInClass C hC R H) ∘
(toCompletedGroupAlgebraRingHom R G) =
(g : Carrier R G → CompletedGroupAlgebraInClass C hC R H) ∘
(toCompletedGroupAlgebraRingHom R G) := by
funext x
exact congrFun (congrArg DFunLike.coe hfg) x
have hfun : (f : Carrier R G → CompletedGroupAlgebraInClass C hC R H) = g :=
DenseRange.equalizer hdense hf hg hcomp
exact RingHom.ext fun x => congrFun hfun 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. 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 completedGroupAlgebraToInClassRingHom_naturality
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
(φ : G →* H) (hφ : Continuous φ) :
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ).comp
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC) =
(completedGroupAlgebraToInClassRingHom (R := R) (G := H) C hC).comp
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)Naturality of the comparison from the all-finite completed group algebra to the \(C\)-indexed completed group algebra in the group variable.
Show proof
by
apply completedGroupAlgebraRingHomToInClass_ext_of_comp_toCompleted
(R := R) (G := G) (H := H) C hC hR hG
· exact (continuous_completedGroupAlgebraMapInClass (R := R) (G := G) (H := H)
C hC hHer φ hφ).comp
(continuous_completedGroupAlgebraToInClass (R := R) (G := G) C hC)
· exact (continuous_completedGroupAlgebraToInClass (R := R) (G := H) C hC).comp
(continuous_completedGroupAlgebraMap (R := R) (G := G) (H := H) hG φ hφ)
· apply RingHom.ext
intro x
have htoG := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra
(R := R) (G := G) C hC))
x
have hmapC := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
(R := R) (G := G) (H := H) C hC hHer φ hφ))
x
have hmapAll := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraMap_comp_toCompletedGroupAlgebra
(R := R) (G := G) (H := H) hG φ hφ))
x
have htoH := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra
(R := R) (G := H) C hC))
(MonoidAlgebra.mapDomainRingHom R φ x)
calc
((((completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ).comp
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)).comp
(toCompletedGroupAlgebraRingHom R G)) x) =
completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
((completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)
(toCompletedGroupAlgebraRingHom R G x)) := rfl
_ =
completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
(toCompletedGroupAlgebraInClassRingHom C hC R G x) := by
exact congrArg (completedGroupAlgebraMapInClass (G := G) (H := H)
C hC hHer R φ hφ) (by
exact htoG)
_ =
toCompletedGroupAlgebraInClassRingHom C hC R H
(MonoidAlgebra.mapDomainRingHom R φ x) := by
simpa [RingHom.comp_apply] using hmapC
_ =
completedGroupAlgebraToInClassRingHom (R := R) (G := H) C hC
(toCompletedGroupAlgebraRingHom R H (MonoidAlgebra.mapDomainRingHom R φ x)) := by
have htoH' :
completedGroupAlgebraToInClassRingHom (R := R) (G := H) C hC
(toCompletedGroupAlgebraRingHom R H
(MonoidAlgebra.mapDomainRingHom R φ x)) =
toCompletedGroupAlgebraInClassRingHom C hC R H
(MonoidAlgebra.mapDomainRingHom R φ x) := by
exact htoH
exact htoH'.symm
_ =
completedGroupAlgebraToInClassRingHom (R := R) (G := H) C hC
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
(toCompletedGroupAlgebraRingHom R G x)) := by
have hmapAll' :
completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
(toCompletedGroupAlgebraRingHom R G x) =
toCompletedGroupAlgebraRingHom R H (MonoidAlgebra.mapDomainRingHom R φ x) := by
exact hmapAll
exact congrArg (completedGroupAlgebraToInClassRingHom (R := R) (G := H) C hC)
hmapAll'.symm
_ =
((((completedGroupAlgebraToInClassRingHom (R := R) (G := H) C hC).comp
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)).comp
(toCompletedGroupAlgebraRingHom R G)) 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. 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. 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 completedGroupAlgebraToInClassAlgHom_naturality
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
(φ : G →* H) (hφ : Continuous φ) :
(completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hC hHer R φ hφ).comp
(completedGroupAlgebraToInClassAlgHom (R := R) (G := G) C hC) =
(completedGroupAlgebraToInClassAlgHom (R := R) (G := H) C hC).comp
(completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG φ hφ)Algebra-homomorphism form of the naturality of the comparison from the all-finite completed group algebra to the \(C\)-indexed completed group algebra.
Show proof
by
apply AlgHom.ext
intro x
have h := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraToInClassRingHom_naturality
(R := R) (G := G) (H := H) C hC hHer hR hG φ hφ))
x
simpa 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. 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 completedGroupAlgebraFromInClassRingHom_naturality
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hR : IsProfiniteRing R) (hG : IsProCGroup C G) (hH : IsProCGroup C H)
(φ : G →* H) (hφ : Continuous φ) :
(completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ).comp
(completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG) =
(completedGroupAlgebraFromInClassRingHom (R := R) (G := H) C hC hForm hH).comp
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ)Naturality of the inverse comparison from the \(C\)-indexed completed group algebra back to the all-finite completed group algebra, for pro-\(C\) groups.
Show proof
by
apply RingHom.ext
intro x
rcases completedGroupAlgebraToInClass_surjective (R := R) (G := G) C hC hForm hG x with
⟨y, rfl⟩
have hnat := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraToInClassRingHom_naturality
(R := R) (G := G) (H := H) C hC hHer hR hG.1 φ hφ))
y
calc
((completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ).comp
(completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG))
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC y)
=
completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
(completedGroupAlgebraToInClass (R := R) (G := G) C hC y)) := rfl
_ =
completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ y := by
rw [completedGroupAlgebraFromInClass_toInClass]
_ =
completedGroupAlgebraFromInClass (R := R) (G := H) C hC hForm hH
(completedGroupAlgebraToInClass (R := R) (G := H) C hC
(completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ y)) := by
rw [completedGroupAlgebraFromInClass_toInClass]
_ =
completedGroupAlgebraFromInClass (R := R) (G := H) C hC hForm hH
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
(completedGroupAlgebraToInClass (R := R) (G := G) C hC y)) := by
exact congrArg (completedGroupAlgebraFromInClass (R := R) (G := H) C hC hForm hH)
hnat.symm
_ =
((completedGroupAlgebraFromInClassRingHom (R := R) (G := H) C hC hForm hH).comp
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ))
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC y) := 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. 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 completedGroupAlgebraFromInClassAlgHom_naturality
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hR : IsProfiniteRing R) (hG : IsProCGroup C G) (hH : IsProCGroup C H)
(φ : G →* H) (hφ : Continuous φ) :
(completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG.1 φ hφ).comp
(completedGroupAlgebraFromInClassAlgHom (R := R) (G := G) C hC hForm hG) =
(completedGroupAlgebraFromInClassAlgHom (R := R) (G := H) C hC hForm hH).comp
(completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hC hHer R φ hφ)Algebra-homomorphism form of the naturality of the inverse comparison from the \(C\)-indexed completed group algebra back to the all-finite completed group algebra.
Show proof
by
apply AlgHom.ext
intro x
have h := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraFromInClassRingHom_naturality
(R := R) (G := G) (H := H) C hC hHer hForm hR hG hH φ hφ))
x
simpa 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. 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 completedGroupAlgebraInClassRingEquiv_naturality
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hR : IsProfiniteRing R) (hG : IsProCGroup C G) (hH : IsProCGroup C H)
(φ : G →* H) (hφ : Continuous φ) (x : Carrier R G) :
completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
(completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hC hForm hG x) =
completedGroupAlgebraInClassRingEquiv (R := R) (G := H) C hC hForm hH
(completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ x)The ring equivalence from all-finite to in-class completions is natural in the group.
Show proof
by
have h := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraToInClassRingHom_naturality
(R := R) (G := G) (H := H) C hC hHer hR hG.1 φ 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. For the all-finite and \(C\)-indexed comparisons, both composites have the same finite-stage coordinates; hence inverse-limit extensionality proves the ring, algebra, or topological equivalence. 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. 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 completedGroupAlgebraInClassRingEquiv_symm_naturality
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hR : IsProfiniteRing R) (hG : IsProCGroup C G) (hH : IsProCGroup C H)
(φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraMap (G := G) (H := H) R hG.1 φ hφ
((completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hC hForm hG).symm x) =
(completedGroupAlgebraInClassRingEquiv (R := R) (G := H) C hC hForm hH).symm
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x)The inverse ring equivalence from in-class to all-finite completions is natural in the group.
Show proof
by
have h := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraFromInClassRingHom_naturality
(R := R) (G := G) (H := H) C hC hHer hForm hR hG hH φ 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. For the all-finite and \(C\)-indexed comparisons, both composites have the same finite-stage coordinates; hence inverse-limit extensionality proves the ring, algebra, or topological equivalence. 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. 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 completedGroupAlgebraInClassAlgEquiv_naturality
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hR : IsProfiniteRing R) (hG : IsProCGroup C G) (hH : IsProCGroup C H)
(φ : G →* H) (hφ : Continuous φ) (x : Carrier R G) :
completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hC hHer R φ hφ
(completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hC hForm hG x) =
completedGroupAlgebraInClassAlgEquiv (R := R) (G := H) C hC hForm hH
(completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG.1 φ hφ x)The algebra equivalence from all-finite to in-class completions is natural in the group.
Show proof
by
have h := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraToInClassAlgHom_naturality
(R := R) (G := G) (H := H) C hC hHer hR hG.1 φ hφ))
x
simpa 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. For the all-finite and \(C\)-indexed comparisons, both composites have the same finite-stage coordinates; hence inverse-limit extensionality proves the ring, algebra, or topological equivalence. 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. 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 completedGroupAlgebraInClassAlgEquiv_symm_naturality
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hR : IsProfiniteRing R) (hG : IsProCGroup C G) (hH : IsProCGroup C H)
(φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraMapAlgHom (G := G) (H := H) R hG.1 φ hφ
((completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hC hForm hG).symm x) =
(completedGroupAlgebraInClassAlgEquiv (R := R) (G := H) C hC hForm hH).symm
(completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hC hHer R φ hφ x)The inverse algebra equivalence from in-class to all-finite completions is natural in the group.
Show proof
by
have h := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraFromInClassAlgHom_naturality
(R := R) (G := G) (H := H) C hC hHer hForm hR hG hH φ hφ))
x
simpa 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. For the all-finite and \(C\)-indexed comparisons, both composites have the same finite-stage coordinates; hence inverse-limit extensionality proves the ring, algebra, or topological equivalence. 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. 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.
□