CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.CanonicalMap
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
theorem groupAlgebraOpenFiniteQuotientMap_surjective
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
Function.Surjective (groupAlgebraOpenFiniteQuotientMap R G K)The abstract group-algebra map onto an open-finite quotient stage is surjective.
Show proof
groupAlgebraFiniteQuotientMap_surjective (R := R) (G := G)
((OrderDual.ofDual K.1).1 : Ideal R) K.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. Surjectivity is obtained by lifting a representative through the underlying surjective quotient or group homomorphism and then checking the defining finite-stage formula. 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. For surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage. 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 groupAlgebraOpenFiniteQuotientMap_compatibleMaps
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G] :
(completedGroupAlgebraOpenFiniteQuotientSystem R G).CompatibleMaps
(fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
groupAlgebraOpenFiniteQuotientMap R G K)The abstract group-algebra maps to open-finite quotient stages are compatible.
Show proof
by
intro K L hKL
funext x
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraOpenFiniteQuotientTransition_comp_map R G hKL))
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. 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 toCompletedGroupAlgebraOpenFiniteQuotientLimit
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(x : MonoidAlgebra R G) :
CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
⟨fun K => groupAlgebraOpenFiniteQuotientMap R G K x, by
intro K L hKL
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraOpenFiniteQuotientTransition_comp_map R G hKL))
x⟩The two-parameter inverse limit \(\varprojlim_{I,U}(R/I)[G/U]\) appearing in Ribes--Zalesskii Section 5.3.
theorem completedGroupAlgebraOpenFiniteQuotientLimitProjection_toLimit
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) (x : MonoidAlgebra R G) :
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K
(toCompletedGroupAlgebraOpenFiniteQuotientLimit R G x) =
groupAlgebraOpenFiniteQuotientMap R G K xProjecting the canonical map to the open-finite quotient limit recovers the stage quotient 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. 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 toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
MonoidAlgebra R G →+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G where
toFun := toCompletedGroupAlgebraOpenFiniteQuotientLimit R G
map_zero' := by
apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
intro K
exact map_zero (groupAlgebraOpenFiniteQuotientMap R G K)
map_one' := by
apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
intro K
exact map_one (groupAlgebraOpenFiniteQuotientMap R G K)
map_add' x y := by
apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
intro K
exact map_add (groupAlgebraOpenFiniteQuotientMap R G K) x y
map_mul' x y := by
apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
intro K
exact map_mul (groupAlgebraOpenFiniteQuotientMap R G K) x yThe canonical map from \(R[G]\) to the two-parameter limit is bundled as a ring homomorphism.
theorem toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom_apply
[IsTopologicalRing R]
(x : MonoidAlgebra R G) :
toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G x =
toCompletedGroupAlgebraOpenFiniteQuotientLimit R G xThe bundled ring homomorphism has the same underlying function as the coordinatewise construction.
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. 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 completedGroupAlgebraOpenFiniteQuotientLimitProjectionRingHom_comp_toLimit
[IsTopologicalRing R]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
(completedGroupAlgebraOpenFiniteQuotientLimitProjectionRingHom R G K).comp
(toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R G) =
groupAlgebraOpenFiniteQuotientMap R G KProjection after the canonical ring homomorphism is the corresponding open-finite quotient map.
Show proof
by
apply RingHom.ext
intro 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. 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 continuous_toCompletedGroupAlgebraOpenFiniteQuotientLimit_kernelTopology
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G] :
letI : TopologicalSpace (MonoidAlgebra R G)The canonical map to the open-finite quotient limit is continuous for the kernel topology.
Show proof
groupAlgebraOpenFiniteQuotientKernelTopology R G
Continuous (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by
letI : TopologicalSpace (MonoidAlgebra R G) :=
groupAlgebraOpenFiniteQuotientKernelTopology R G
let S := completedGroupAlgebraOpenFiniteQuotientSystem R G
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
have hprod : Continuous (groupAlgebraOpenFiniteQuotientProductMap R G) :=
continuous_groupAlgebraOpenFiniteQuotientProductMap_kernelTopology R G
change Continuous fun x : MonoidAlgebra R G =>
(⟨groupAlgebraOpenFiniteQuotientProductMap R G x, _⟩ :
CompletedGroupAlgebraOpenFiniteQuotientLimit R G)
exact Continuous.subtype_mk hprod fun x => (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G 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. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. 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 denseRange_toCompletedGroupAlgebraOpenFiniteQuotientLimit
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
[Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
DenseRange (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G)The two-parameter inverse limit \(\varprojlim_{I,U}(R/I)[G/U]\) appearing in Ribes--Zalesskii Section 5.3.
Show proof
by
let S := completedGroupAlgebraOpenFiniteQuotientSystem R G
letI : TopologicalSpace (MonoidAlgebra R G) := ⊥
have hdir :
Directed (α := CompletedGroupAlgebraOpenQuotientIndex R G) (· ≤ ·) fun K => K :=
directed_completedGroupAlgebraOpenQuotientIndex R G
have hdense :
DenseRange
(S.inverseLimitLift
(fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
groupAlgebraOpenFiniteQuotientMap R G K)
(groupAlgebraOpenFiniteQuotientMap_compatibleMaps R G)) :=
S.denseRange_lift
(fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
groupAlgebraOpenFiniteQuotientMap R G K)
(groupAlgebraOpenFiniteQuotientMap_compatibleMaps R G)
(fun K => groupAlgebraOpenFiniteQuotientMap_surjective R G K)
hdir
simpa [S, toCompletedGroupAlgebraOpenFiniteQuotientLimit] using hdenseProof. 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.
□