CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
def completedGroupAlgebraToOpenFiniteQuotientLimit
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(x : Carrier R G) :
CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
⟨fun K => completedGroupAlgebraOpenFiniteQuotientProjection R G K x, by
intro K L hKL
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraOpenFiniteQuotientTransition_comp_projection R G hKL))
x⟩
@[simp]The canonical map from the fixed-coefficient completed group algebra \(\widehat{R[G]}\) to the two-parameter limit \(\varprojlim_{I,U} (R/I)[G/U]\).
theorem completedGroupAlgebraOpenFiniteQuotientLimitProjection_fromCompleted
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) (x : Carrier R G) :
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K
(completedGroupAlgebraToOpenFiniteQuotientLimit R G x) =
completedGroupAlgebraOpenFiniteQuotientProjection R G K xThe open-finite-limit projection after the comparison from the completed group algebra is the original finite-stage projection.
Show proof
rfl
@[simp]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 completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(x : MonoidAlgebra R G) :
completedGroupAlgebraToOpenFiniteQuotientLimit R G (toCompletedGroupAlgebra R G x) =
toCompletedGroupAlgebraOpenFiniteQuotientLimit R G xThe comparison from the completed group algebra to the open-finite quotient limit agrees with the canonical dense map on abstract group-algebra elements.
Show proof
by
apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
intro K
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. 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.
□def completedGroupAlgebraToOpenFiniteQuotientLimitRingHom
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
Carrier R G →+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G where
toFun := completedGroupAlgebraToOpenFiniteQuotientLimit R G
map_zero' := by
apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
intro K
exact map_zero (completedGroupAlgebraOpenFiniteQuotientProjection R G K)
map_one' := by
apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
intro K
exact map_one (completedGroupAlgebraOpenFiniteQuotientProjection R G K)
map_add' x y := by
apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
intro K
exact map_add (completedGroupAlgebraOpenFiniteQuotientProjection R G K) x y
map_mul' x y := by
apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
intro K
exact map_mul (completedGroupAlgebraOpenFiniteQuotientProjection R G K) x y
@[simp]The canonical map \(\widehat{R[G]} \to \varprojlim_{I,U} (R/I)[G/U]\) is bundled as a ring homomorphism.
theorem openFiniteLimitProjectionRingHom_comp_fromCompleted
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
(completedGroupAlgebraOpenFiniteQuotientLimitProjectionRingHom R G K).comp
(completedGroupAlgebraToOpenFiniteQuotientLimitRingHom R G) =
completedGroupAlgebraOpenFiniteQuotientProjection R G KThe ring-hom projection from the open-finite quotient limit, composed with the comparison from the completion, recovers the corresponding completed projection.
Show proof
by
apply RingHom.ext
intro x
rfl
@[simp]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. 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 completedGAToOpenFiniteQuotientLimitRingHom_comp_toCompletedGA :
(completedGroupAlgebraToOpenFiniteQuotientLimitRingHom R G).comp
(toCompletedGroupAlgebraRingHom R G) =
toCompletedGroupAlgebraOpenFiniteQuotientLimitRingHom R GComposing the comparison map with the dense map from the abstract group algebra recovers the canonical completed group-algebra map.
Show proof
by
apply RingHom.ext
intro x
exact completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra (R := R) (G := G) 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 continuous_completedGroupAlgebraToOpenFiniteQuotientLimit :
Continuous (completedGroupAlgebraToOpenFiniteQuotientLimit R G)The comparison map \(\widehat{R[G]} \to \varprojlim_{I,U} (R/I)[G/U]\) is continuous.
Show proof
by
let A := Carrier R G
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
have hval : Continuous fun x : A =>
((completedGroupAlgebraToOpenFiniteQuotientLimit R G x) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
change Continuous fun x : A =>
fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
completedGroupAlgebraOpenFiniteQuotientProjection R G K x
apply continuous_pi
intro K
exact continuous_completedGroupAlgebraOpenFiniteQuotientProjection (R := R) (G := G) K
exact Continuous.subtype_mk hval fun x =>
(completedGroupAlgebraToOpenFiniteQuotientLimit 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. 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 denseRange_completedGroupAlgebraToOpenFiniteQuotientLimit
[Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
DenseRange (completedGroupAlgebraToOpenFiniteQuotientLimit R G)The image of the map from the completed group algebra to the open-finite quotient limit is dense in the target completed group-algebra object.
Show proof
by
have hdense :
DenseRange
((completedGroupAlgebraToOpenFiniteQuotientLimit R G) ∘
(toCompletedGroupAlgebra R G)) := by
simpa [Function.comp] using
denseRange_toCompletedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G)
exact DenseRange.of_comp 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.
□theorem injective_completedGroupAlgebraToOpenFiniteQuotientLimit
(hR : IsProfiniteRing R) :
Function.Injective (completedGroupAlgebraToOpenFiniteQuotientLimit R G)The comparison map to the two-parameter kernel-neighborhood limit is injective when the coefficient ring is profinite. This is the completed-stage form of the kernel-intersection claim in Lemma 5.3.5(a).
Show proof
by
intro x y hxy
apply (completedGroupAlgebraSystem R G).ext
intro U
apply Finsupp.ext
intro q
have hzero : ((completedGroupAlgebraProjection R G U x -
completedGroupAlgebraProjection R G U y) q) = 0 := by
apply profiniteRing_eq_zero_of_forall_openIdeal_quotient_eq_zero (R := R) hR
intro Iopen
let K : CompletedGroupAlgebraOpenQuotientIndex R G := (OrderDual.toDual Iopen, U)
have hcoord := congrArg
(fun z : CompletedGroupAlgebraOpenFiniteQuotientLimit R G =>
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K z) hxy
change completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 U
(completedGroupAlgebraProjection R G U x) =
completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 U
(completedGroupAlgebraProjection R G U y) at hcoord
have hdiff : completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 U
(completedGroupAlgebraProjection R G U x -
completedGroupAlgebraProjection R G U y) = 0 := by
rw [map_sub, hcoord, sub_self]
have hq := congrArg
(fun z : CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 U => z q) hdiff
simpa [completedGroupAlgebraStageCoeffQuotientMap,
MonoidAlgebra.mapRangeRingHom_apply] using hq
have hsub : (completedGroupAlgebraProjection R G U x) q -
(completedGroupAlgebraProjection R G U y) q = 0 := by
simpa using hzero
exact sub_eq_zero.mp hsubProof. 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. 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. Injectivity follows because two elements with identical finite-stage coordinates are equal in the inverse limit, and subtype inclusions are injective on their underlying elements. 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. For injectivity, suppose two source elements have the same image. After projecting to every finite quotient stage the corresponding finite-stage map is injective, or the equality is simply equality of subtype carriers; hence all source coordinates agree, and the inverse-limit extensionality principle identifies the original elements.
□theorem surjective_completedGroupAlgebraToOpenFiniteQuotientLimit
(hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
Function.Surjective (completedGroupAlgebraToOpenFiniteQuotientLimit R G)The comparison map to the two-parameter kernel-neighborhood limit is onto for profinite coefficients: its dense image is compact, hence closed, in the Hausdorff two-parameter limit.
Show proof
by
letI : CompactSpace (Carrier R G) :=
completedGroupAlgebra_compactSpace (R := R) (G := G) hR
letI : T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
completedGroupAlgebraOpenFiniteQuotientLimit_t2Space (R := R) (G := G) hR
have hclosed : IsClosed (Set.range (completedGroupAlgebraToOpenFiniteQuotientLimit R G)) := by
exact (isCompact_range
(continuous_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G))).isClosed
have hdense :
closure (Set.range (completedGroupAlgebraToOpenFiniteQuotientLimit R G)) = Set.univ :=
(denseRange_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G)).closure_range
have hrange : Set.range (completedGroupAlgebraToOpenFiniteQuotientLimit R G) = Set.univ := by
rwa [hclosed.closure_eq] at hdense
intro y
have hy : y ∈ Set.range (completedGroupAlgebraToOpenFiniteQuotientLimit R G) := by
rw [hrange]
exact Set.mem_univ y
simpa using hyProof. 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. 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. 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. 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. 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.
□theorem bijective_completedGroupAlgebraToOpenFiniteQuotientLimit
(hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
Function.Bijective (completedGroupAlgebraToOpenFiniteQuotientLimit R G)The comparison map \(\widehat{R[G]} \to \varprojlim_{I,U} (R/I)[G/U]\) is a bijection under the profinite coefficient hypothesis.
Show proof
⟨injective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G) hR,
surjective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G) hR⟩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. 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. 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 completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv
(hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
Carrier R G ≃+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
RingEquiv.ofBijective (completedGroupAlgebraToOpenFiniteQuotientLimitRingHom R G)
(bijective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G) hR)
@[simp]Ribes--Zalesskii Section \(5.3\) comparison: the fixed-coefficient inverse-limit model \(\widehat{R[G]}\) is ring-isomorphic to the two-parameter kernel-neighborhood limit \(\varprojlim_{I,U} (R/I)[G/U]\) for profinite coefficient rings.
theorem completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv_apply
(hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)]
(x : Carrier R G) :
completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv (R := R) (G := G) hR x =
completedGroupAlgebraToOpenFiniteQuotientLimit R G xThe comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison 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. 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. 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 completedGroupAlgebraOpenFiniteQuotientLimitHomeomorph
(hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
Carrier R G ≃ₜ CompletedGroupAlgebraOpenFiniteQuotientLimit R G := by
letI : CompactSpace (Carrier R G) :=
completedGroupAlgebra_compactSpace (R := R) (G := G) hR
letI : T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
completedGroupAlgebraOpenFiniteQuotientLimit_t2Space (R := R) (G := G) hR
let e : Carrier R G ≃ CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
(completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv (R := R) (G := G) hR).toEquiv
exact Continuous.homeoOfEquivCompactToT2 (f := e) (by
change Continuous (completedGroupAlgebraToOpenFiniteQuotientLimit R G)
exact continuous_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G))The fixed-coefficient completed group algebra is homeomorphic to the two-parameter open finite quotient inverse limit.
theorem denseRange_toCompletedGroupAlgebra (hG : ProCGroups.IsProfiniteGroup G) :
DenseRange (toCompletedGroupAlgebra R G)In Lemma 5.3.5(c), fixed-coefficient inverse-limit form, the abstract group algebra maps dense into the completed group algebra.
Show proof
by
let S := completedGroupAlgebraSystem R G
letI : TopologicalSpace (MonoidAlgebra R G) := ⊥
have hProC : IsProCGroup ProCGroups.FiniteGroupClass.allFinite G :=
(isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG
letI : Nonempty (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) :=
IsProCGroup.openNormalSubgroupInClass_nonempty hProC
letI : Nonempty (CompletedGroupAlgebraIndex G) := inferInstance
have hdir : Directed (α := CompletedGroupAlgebraIndex G) (· ≤ ·) fun U => U :=
directed_openNormalSubgroupInClass
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) ProCGroups.FiniteGroupClass.allFinite_formation
have hdense :
DenseRange
(S.inverseLimitLift (fun U : CompletedGroupAlgebraIndex G => completedGroupAlgebraStageMap R G U)
(completedGroupAlgebraStageMap_compatibleMaps (R := R) (G := G))) :=
S.denseRange_lift
(fun U : CompletedGroupAlgebraIndex G => completedGroupAlgebraStageMap R G U)
(completedGroupAlgebraStageMap_compatibleMaps (R := R) (G := G))
(fun U => completedGroupAlgebraStageMap_surjective (R := R) (G := G) U)
hdir
simpa [S, toCompletedGroupAlgebra] 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, 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. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. 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_toCompletedGroupAlgebraRingHom (hG : ProCGroups.IsProfiniteGroup G) :
DenseRange (toCompletedGroupAlgebraRingHom R G)The image of the canonical ring homomorphism into the completed group algebra is dense.
Show proof
by
simpa [toCompletedGroupAlgebraRingHom] using
denseRange_toCompletedGroupAlgebra (R := R) (G := G) hGProof. 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. 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.
□def completedGroupAlgebraNaturalTopology (R : Type u) (G : Type v) [CommRing R]
[TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] :
TopologicalSpace (MonoidAlgebra R G) :=
TopologicalSpace.induced (toCompletedGroupAlgebra R G) inferInstanceThe completion topology on the abstract group algebra, induced by the canonical map into \(\widehat{R[G]}\); below it is identified with the kernel-neighborhood topology generated by the maps \(R[G] \to (R/I)[G/U]\).
theorem continuous_toCompletedGroupAlgebraRingHom_naturalTopology :
letI : TopologicalSpace (MonoidAlgebra R G)The dense map from the abstract group algebra to the completed group algebra is continuous for the natural finite-quotient topology.
Show proof
completedGroupAlgebraNaturalTopology R G
Continuous (toCompletedGroupAlgebraRingHom R G) := by
letI : TopologicalSpace (MonoidAlgebra R G) :=
completedGroupAlgebraNaturalTopology R G
change Continuous (toCompletedGroupAlgebra R G)
exact (continuous_induced_dom : Continuous (toCompletedGroupAlgebra R G))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. 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.
□def toCompletedGroupAlgebraContinuousLinearMap_naturalTopology :
letI : TopologicalSpace (MonoidAlgebra R G) :=
completedGroupAlgebraNaturalTopology R G
MonoidAlgebra R G →L[R] Carrier R G := by
letI : TopologicalSpace (MonoidAlgebra R G) :=
completedGroupAlgebraNaturalTopology R G
exact
{ toLinearMap := toCompletedGroupAlgebraLinearMap R G
cont := continuous_toCompletedGroupAlgebraRingHom_naturalTopology (R := R) (G := G) }The canonical map as a continuous \(R\)-linear map for the topology induced from \(\widehat{R[G]}\).
theorem groupAlgebraOpenFiniteQuotientKernelTopology_eq_induced_toLimit :
groupAlgebraOpenFiniteQuotientKernelTopology R G =
TopologicalSpace.induced (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G) inferInstanceThe kernel-neighborhood topology is exactly the topology induced by the canonical map from \(R[G]\) to the two-parameter kernel-neighborhood limit.
Show proof
by
let S := completedGroupAlgebraOpenFiniteQuotientSystem R G
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
change TopologicalSpace.induced (groupAlgebraOpenFiniteQuotientProductMap R G) inferInstance =
TopologicalSpace.induced (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G)
(TopologicalSpace.induced (fun z : S.inverseLimit => z.1) inferInstance)
rw [induced_compose]
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. 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. For bundled structures, the finite-stage laws commute with all transition maps, so the coordinatewise operations assemble to a compatible family satisfying the required axioms. 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem completedGroupAlgebraNaturalTopology_eq_induced_toOpenFiniteQuotientLimit
(hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
completedGroupAlgebraNaturalTopology R G =
TopologicalSpace.induced (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G) inferInstanceUnder the profinite coefficient hypothesis, the topology on \(R[G]\) induced from \(\widehat{R[G]}\) agrees with the topology induced by the two-parameter kernel-neighborhood limit.
Show proof
by
let e := completedGroupAlgebraOpenFiniteQuotientLimitHomeomorph (R := R) (G := G) hR
have hcomp : e ∘ toCompletedGroupAlgebra R G =
toCompletedGroupAlgebraOpenFiniteQuotientLimit R G := by
funext x
exact completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra
(R := R) (G := G) x
dsimp [completedGroupAlgebraNaturalTopology]
rw [e.isInducing.eq_induced]
rw [induced_compose]
rw [hcomp]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. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. 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. For bundled structures, the finite-stage laws commute with all transition maps, so the coordinatewise operations assemble to a compatible family satisfying the required axioms. 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 completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology
(hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
completedGroupAlgebraNaturalTopology R G =
groupAlgebraOpenFiniteQuotientKernelTopology R GRibes--Zalesskii Section \(5.3\) natural topology comparison: the topology on the abstract group algebra induced from \(\widehat{R[G]}\) is the kernel-neighborhood topology generated by the maps \(R[G] \to (R/I)[G/U]\).
Show proof
by
rw [completedGroupAlgebraNaturalTopology_eq_induced_toOpenFiniteQuotientLimit
(R := R) (G := G) hR,
groupAlgebraOpenFiniteQuotientKernelTopology_eq_induced_toLimit (R := R) (G := G)]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. 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 continuous_toCompletedGroupAlgebraRingHom_kernelTopology
(hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
letI : TopologicalSpace (MonoidAlgebra R G)The canonical map \(R[G] \to \widehat{R[G]}\) is continuous for the kernel-neighborhood topology on \(R[G]\).
Show proof
groupAlgebraOpenFiniteQuotientKernelTopology R G
Continuous (toCompletedGroupAlgebraRingHom R G) := by
let τnat := completedGroupAlgebraNaturalTopology R G
let τker := groupAlgebraOpenFiniteQuotientKernelTopology R G
have hτ : τnat = τker :=
completedGroupAlgebraNaturalTopology_eq_openFiniteQuotientKernelTopology
(R := R) (G := G) hR
change @Continuous (MonoidAlgebra R G) (Carrier R G)
τker inferInstance (toCompletedGroupAlgebraRingHom R G)
rw [← hτ]
exact continuous_toCompletedGroupAlgebraRingHom_naturalTopology (R := R) (G := G)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. 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.
□def toCompletedGroupAlgebraContinuousLinearMap_kernelTopology
(hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
letI : TopologicalSpace (MonoidAlgebra R G) :=
groupAlgebraOpenFiniteQuotientKernelTopology R G
MonoidAlgebra R G →L[R] Carrier R G := by
letI : TopologicalSpace (MonoidAlgebra R G) :=
groupAlgebraOpenFiniteQuotientKernelTopology R G
exact
{ toLinearMap := toCompletedGroupAlgebraLinearMap R G
cont := continuous_toCompletedGroupAlgebraRingHom_kernelTopology
(R := R) (G := G) hR }The canonical map as a continuous \(R\)-linear map for the kernel-neighborhood topology.
theorem completedGroupAlgebra_kernelTopologyCompletionData
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
letI : TopologicalSpace (MonoidAlgebra R G)Lemma 5.3.5(b/c), in kernel-topology form: for profinite \(R\) and profinite \(G\), the concrete inverse limit \(\widehat{R[G]}\) is profinite and the canonical map from \(R[G]\), with the kernel-neighborhood topology, is dense and continuous.
Show proof
groupAlgebraOpenFiniteQuotientKernelTopology R G
IsProfiniteRing (Carrier R G) ∧
DenseRange (toCompletedGroupAlgebraRingHom R G) ∧
Continuous (toCompletedGroupAlgebraRingHom R G) := by
have hProC : IsProCGroup ProCGroups.FiniteGroupClass.allFinite G :=
(isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG
letI : Nonempty (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) :=
IsProCGroup.openNormalSubgroupInClass_nonempty hProC
letI : Nonempty (CompletedGroupAlgebraIndex G) := inferInstance
letI : Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G) := inferInstance
letI : TopologicalSpace (MonoidAlgebra R G) :=
groupAlgebraOpenFiniteQuotientKernelTopology R G
exact ⟨completedGroupAlgebra_isProfiniteRing (R := R) (G := G) hR,
denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG,
continuous_toCompletedGroupAlgebraRingHom_kernelTopology (R := R) (G := G) hR⟩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. 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. 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 completedGroupAlgebra_kernelTopologyModuleCompletionData
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
letI : TopologicalSpace (MonoidAlgebra R G)Linear-module form of the kernel-topology completion data for Lemma 5.3.5.
Show proof
groupAlgebraOpenFiniteQuotientKernelTopology R G
IsProfiniteModule R (Carrier R G) ∧
DenseRange (toCompletedGroupAlgebraLinearMap R G) ∧
Continuous (toCompletedGroupAlgebraLinearMap R G) := by
have hProC : IsProCGroup ProCGroups.FiniteGroupClass.allFinite G :=
(isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG
letI : Nonempty (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) :=
IsProCGroup.openNormalSubgroupInClass_nonempty hProC
letI : Nonempty (CompletedGroupAlgebraIndex G) := inferInstance
letI : Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G) := inferInstance
letI : TopologicalSpace (MonoidAlgebra R G) :=
groupAlgebraOpenFiniteQuotientKernelTopology R G
refine ⟨completedGroupAlgebra_isProfiniteModule (R := R) (G := G) hR, ?_, ?_⟩
· change DenseRange (toCompletedGroupAlgebra R G)
simpa [toCompletedGroupAlgebraRingHom] using
denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG
· change Continuous (toCompletedGroupAlgebra R G)
exact continuous_toCompletedGroupAlgebraRingHom_kernelTopology (R := R) (G := G) hRProof. 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. 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.
□