def completedGroupAlgebraLiftFiberSet
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
(hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
(x : Carrier R G)
(W : ProfiniteModuleOpenSubmodule (R := R) N) : Set N :=
{y | Submodule.mkQ W.1 y =
completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf W.1 W.2 x}theorem completedGroupAlgebraLiftFiberSet_isClosed
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
(hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
(x : Carrier R G)
(W : ProfiniteModuleOpenSubmodule (R := R) N) :
IsClosed (completedGroupAlgebraLiftFiberSet
(R := R) (G := G) hG N hN f hf x W)The quotient fiber attached to an open submodule is closed.
Show proof
by
let hdisc : IsDiscreteModule R (N ⧸ W.1) :=
quotient_openSubmodule_isDiscreteModule R N hN W.1 W.2
letI : DiscreteTopology (N ⧸ W.1) := hdisc.2
have hqcont : Continuous (Submodule.mkQ W.1 : N → N ⧸ W.1) := by
change Continuous (Submodule.Quotient.mk (p := W.1))
exact continuous_quotient_mk'
change IsClosed ((Submodule.mkQ W.1 : N → N ⧸ W.1) ⁻¹'
({completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf W.1 W.2 x} : Set (N ⧸ W.1)))
exact (isClosed_discrete _).preimage hqcontProof. 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 completedGroupAlgebraLiftFiberSet_finite_inter_nonempty
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
(hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
(x : Carrier R G)
(s : Finset (ProfiniteModuleOpenSubmodule (R := R) N)) :
(⋂ W ∈ s, completedGroupAlgebraLiftFiberSet
(R := R) (G := G) hG N hN f hf x W).NonemptyFinite intersection property for the fibers used to assemble the profinite-target lift.
Show proof
by
classical
rcases exists_openSubmodule_le_finset (R := R) N s with ⟨K, hK⟩
rcases Submodule.mkQ_surjective K.1
(completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf K.1 K.2 x) with
⟨z, hz⟩
refine ⟨z, ?_⟩
simp only [Set.mem_iInter]
intro W hWs
dsimp [completedGroupAlgebraLiftFiberSet]
calc
Submodule.mkQ W.1 z = Submodule.factor (hK W hWs) (Submodule.mkQ K.1 z) := by
rw [Submodule.factor_mk]
_ = Submodule.factor (hK W hWs)
(completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf K.1 K.2 x) := by
rw [hz]
_ = completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf W.1 W.2 x := by
exact completedGroupAlgebraLiftToOpenSubmoduleQuotient_factor
(R := R) (G := G) hG N hN f hf (hK W hWs) K.2 W.2 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. 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 completedGroupAlgebraLiftFiberSet_iInter_nonempty
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
(hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
(x : Carrier R G) :
(⋂ W : ProfiniteModuleOpenSubmodule (R := R) N,
completedGroupAlgebraLiftFiberSet
(R := R) (G := G) hG N hN f hf x W).NonemptyCompactness of the profinite target gives a simultaneous lift of the compatible quotient values.
Show proof
by
letI : CompactSpace N := hN.2.2.2.1
exact CompactSpace.iInter_nonempty
(t := fun W : ProfiniteModuleOpenSubmodule (R := R) N =>
completedGroupAlgebraLiftFiberSet
(R := R) (G := G) hG N hN f hf x W)
(fun W => completedGroupAlgebraLiftFiberSet_isClosed
(R := R) (G := G) hG N hN f hf x W)
(fun s => completedGroupAlgebraLiftFiberSet_finite_inter_nonempty
(R := R) (G := G) hG N hN f hf x s)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.
□def completedGroupAlgebraLiftToProfiniteModuleFun
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
(hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f) :
Carrier R G → N :=
fun x => Classical.choose
(completedGroupAlgebraLiftFiberSet_iInter_nonempty
(R := R) (G := G) hG N hN f hf x)The assembled pointwise lift from \(\widehat{R[G]}\) to a profinite target module.
theorem completedGroupAlgebraLiftToProfiniteModuleFun_quotient
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
(hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
(W : ProfiniteModuleOpenSubmodule (R := R) N)
(x : Carrier R G) :
Submodule.mkQ W.1
(completedGroupAlgebraLiftToProfiniteModuleFun
(R := R) (G := G) hG N hN f hf x) =
completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf W.1 W.2 xThe assembled point maps to the prescribed quotient-valued extension modulo every open submodule.
Show proof
by
have hmem := Classical.choose_spec
(completedGroupAlgebraLiftFiberSet_iInter_nonempty
(R := R) (G := G) hG N hN f hf x)
exact (Set.mem_iInter.1 hmem W : _)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 completedGroupAlgebraLiftToProfiniteModuleFun_apply_of
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
(hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
(g : G) :
completedGroupAlgebraLiftToProfiniteModuleFun
(R := R) (G := G) hG N hN f hf (completedGroupAlgebraOf R G g) = f gThe assembled lift has the prescribed values on the completed group-like elements.
Show proof
by
apply profiniteModule_ext_of_openSubmoduleQuotients (R := R) N hN
intro W hW
rw [completedGroupAlgebraLiftToProfiniteModuleFun_quotient
(R := R) (G := G) hG N hN f hf ⟨W, hW⟩,
completedGroupAlgebraLiftToOpenSubmoduleQuotient_apply_of]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. 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 completedGroupAlgebraLiftToProfiniteModuleFun_add
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
(hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
(x y : Carrier R G) :
completedGroupAlgebraLiftToProfiniteModuleFun
(R := R) (G := G) hG N hN f hf (x + y) =
completedGroupAlgebraLiftToProfiniteModuleFun
(R := R) (G := G) hG N hN f hf x +
completedGroupAlgebraLiftToProfiniteModuleFun
(R := R) (G := G) hG N hN f hf yAdditivity of the assembled profinite-target lift, checked after all open-submodule quotients.
Show proof
by
apply profiniteModule_ext_of_openSubmoduleQuotients (R := R) N hN
intro W hW
rw [completedGroupAlgebraLiftToProfiniteModuleFun_quotient
(R := R) (G := G) hG N hN f hf ⟨W, hW⟩,
map_add,
← completedGroupAlgebraLiftToProfiniteModuleFun_quotient
(R := R) (G := G) hG N hN f hf ⟨W, hW⟩ x,
← completedGroupAlgebraLiftToProfiniteModuleFun_quotient
(R := R) (G := G) hG N hN f hf ⟨W, hW⟩ 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. 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 completedGroupAlgebraLiftToProfiniteModuleFun_smul
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
(hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
(r : R) (x : Carrier R G) :
completedGroupAlgebraLiftToProfiniteModuleFun
(R := R) (G := G) hG N hN f hf (r • x) =
r • completedGroupAlgebraLiftToProfiniteModuleFun
(R := R) (G := G) hG N hN f hf xThe assembled profinite-target lift is compatible with scalar multiplication after all open-submodule quotients.
Show proof
by
apply profiniteModule_ext_of_openSubmoduleQuotients (R := R) N hN
intro W hW
rw [completedGroupAlgebraLiftToProfiniteModuleFun_quotient
(R := R) (G := G) hG N hN f hf ⟨W, hW⟩,
map_smul,
← completedGroupAlgebraLiftToProfiniteModuleFun_quotient
(R := R) (G := G) hG N hN f hf ⟨W, hW⟩ 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. 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 completedGroupAlgebraLiftToProfiniteModule
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
(hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f) :
Carrier R G →L[R] N where
toFun := completedGroupAlgebraLiftToProfiniteModuleFun (R := R) (G := G) hG N hN f hf
map_add' := completedGroupAlgebraLiftToProfiniteModuleFun_add
(R := R) (G := G) hG N hN f hf
map_smul' := completedGroupAlgebraLiftToProfiniteModuleFun_smul
(R := R) (G := G) hG N hN f hf
cont := by
apply continuous_of_forall_openSubmodule_quotient_continuous (R := R) N hN
intro W hW
have hEq : (fun x : Carrier R G =>
Submodule.mkQ W
(completedGroupAlgebraLiftToProfiniteModuleFun
(R := R) (G := G) hG N hN f hf x)) =
completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf W hW := by
funext x
exact completedGroupAlgebraLiftToProfiniteModuleFun_quotient
(R := R) (G := G) hG N hN f hf ⟨W, hW⟩ x
rw [hEq]
exact (completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf W hW).continuousExistence half of Lemma 5.3.5(d): a continuous map from the profinite group \(G\) to a profinite \(R\)-module extends to a continuous \(R\)-linear map out of \(\widehat{R[G]}\).
theorem completedGroupAlgebraLiftToProfiniteModule_apply_of
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
(hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
(g : G) :
completedGroupAlgebraLiftToProfiniteModule
(R := R) (G := G) hG N hN f hf (completedGroupAlgebraOf R G g) = f gThe profinite-target lift has the prescribed value on completed group-like elements.
Show proof
completedGroupAlgebraLiftToProfiniteModuleFun_apply_of
(R := R) (G := G) hG N hN f hf gProof. 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. 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 completedGroupAlgebra_existsUnique_lift_to_profiniteModule
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
(hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f) :
∃! F : Carrier R G →L[R] N,
∀ g : G, F (completedGroupAlgebraOf R G g) = f gLemma 5.3.5(d): the completed group algebra satisfies the full universal property for maps into profinite modules.
Show proof
by
letI : T2Space N := hN.2.2.2.2.1
let F := completedGroupAlgebraLiftToProfiniteModule (R := R) (G := G) hG N hN f hf
refine ⟨F, ?_, ?_⟩
· intro g
exact completedGroupAlgebraLiftToProfiniteModule_apply_of
(R := R) (G := G) hG N hN f hf g
· intro K hK
apply completedGroupAlgebraContinuousLinearMap_ext_of_basis (R := R) (G := G) hG
intro g
rw [completedGroupAlgebraLiftToProfiniteModule_apply_of, hK]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 completedGroupAlgebraOf_freeProfiniteModule
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
IsFreeProfiniteModuleOn R G (Carrier R G) (completedGroupAlgebraOf R G)Ribes--Zalesskii Lemma 5.3.5(d): \(\widehat{R[G]}\) is the free profinite \(R\)-module on the profinite space G, with basis map \(g\mapsto [g]\) inside the completed group algebra.
Show proof
by
refine ⟨hR, completedGroupAlgebra_isProfiniteModule (R := R) (G := G) hR,
continuous_completedGroupAlgebraOf (R := R) (G := G),
completedGroupAlgebraOf_dense_span (R := R) (G := G) hG, ?_⟩
intro N _addN _topN _modN hN f hf
exact completedGroupAlgebra_existsUnique_lift_to_profiniteModule
(R := R) (G := G) hG N hN f hfProof. 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.
□