CompletedGroupAlgebra.UniversalProperty.OpenSubmoduleQuotient
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.
theorem completedGroupAlgebra_existsUnique_lift_to_openSubmoduleQuotient
(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 : Submodule R N) (hW : IsOpen (W : Set N)) :
∃! F : Carrier R G →L[R] N ⧸ W,
∀ g : G, F (completedGroupAlgebraOf R G g) = Submodule.mkQ W (f g)The quotient-target form of the existence step in Lemma 5.3.5(d): after quotienting a profinite target module by an open submodule, the prescribed continuous map from \(G\) extends uniquely from \(\widehat{R[G]}\).
Show proof
by
let hdisc : IsDiscreteModule R (N ⧸ W) :=
quotient_openSubmodule_isDiscreteModule R N hN W hW
letI : IsTopologicalRing R := hN.1.1
letI : IsTopologicalAddGroup (N ⧸ W) := hdisc.1.2.1
letI : ContinuousAdd (N ⧸ W) := inferInstance
letI : ContinuousSMul R (N ⧸ W) := hdisc.1.2.2
letI : DiscreteTopology (N ⧸ W) := hdisc.2
letI : T2Space (N ⧸ W) := inferInstance
have hqcont : Continuous (Submodule.mkQ W : N → N ⧸ W) := by
change Continuous (Submodule.Quotient.mk (p := W))
exact continuous_quotient_mk'
rcases exists_completedGroupAlgebraIndex_factor_continuous_discrete
(G := G) hG (N ⧸ W) (fun g : G => Submodule.mkQ W (f g))
(hqcont.comp hf) with
⟨U, fbar, hfac⟩
exact completedGroupAlgebra_existsUnique_lift_of_factors (R := R) (G := G) hG (N ⧸ W)
U (fun g : G => Submodule.mkQ W (f g)) fbar hfacProof. 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 completedGroupAlgebraLiftToOpenSubmoduleQuotient
(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 : Submodule R N) (hW : IsOpen (W : Set N)) :
Carrier R G →L[R] N ⧸ W :=
Classical.choose
(completedGroupAlgebra_existsUnique_lift_to_openSubmoduleQuotient
(R := R) (G := G) hG N hN f hf W hW)The chosen quotient-valued extension attached to an open submodule of a profinite target.
theorem completedGroupAlgebraLiftToOpenSubmoduleQuotient_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)
(W : Submodule R N) (hW : IsOpen (W : Set N)) (g : G) :
completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf W hW
(completedGroupAlgebraOf R G g) =
Submodule.mkQ W (f g)The quotient-valued lift has the prescribed value on completed group-like elements.
Show proof
by
exact (Classical.choose_spec
(completedGroupAlgebra_existsUnique_lift_to_openSubmoduleQuotient
(R := R) (G := G) hG N hN f hf W hW)).1 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, 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 completedGroupAlgebraLiftToOpenSubmoduleQuotient_factor
(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 V : Submodule R N} (hWV : W ≤ V)
(hW : IsOpen (W : Set N)) (hV : IsOpen (V : Set N))
(x : Carrier R G) :
Submodule.factor hWV
(completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf W hW x) =
completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf V hV xThe quotient-valued extensions are compatible with refinement of open submodules.
Show proof
by
let hdiscV : IsDiscreteModule R (N ⧸ V) :=
quotient_openSubmodule_isDiscreteModule R N hN V hV
let hdiscW : IsDiscreteModule R (N ⧸ W) :=
quotient_openSubmodule_isDiscreteModule R N hN W hW
letI : DiscreteTopology (N ⧸ W) := hdiscW.2
letI : DiscreteTopology (N ⧸ V) := hdiscV.2
letI : T2Space (N ⧸ V) := inferInstance
let factorCLM : N ⧸ W →L[R] N ⧸ V :=
{ toLinearMap := Submodule.factor hWV
cont := continuous_of_discreteTopology }
have hEq :
factorCLM.comp
(completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf W hW) =
completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf V hV := by
apply completedGroupAlgebraContinuousLinearMap_ext_of_basis (R := R) (G := G) hG
intro g
change Submodule.factor hWV
(completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf W hW
(completedGroupAlgebraOf R G g)) =
completedGroupAlgebraLiftToOpenSubmoduleQuotient
(R := R) (G := G) hG N hN f hf V hV
(completedGroupAlgebraOf R G g)
rw [completedGroupAlgebraLiftToOpenSubmoduleQuotient_apply_of,
completedGroupAlgebraLiftToOpenSubmoduleQuotient_apply_of,
Submodule.factor_mk]
exact congrArg (fun F : Carrier R G →L[R] N ⧸ V => F x) hEqProof. 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.
□