CompletedGroupAlgebra.AllFiniteAugmentation.CanonicalAugmentation
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.
def completedGroupAlgebraAugmentationAt (R : Type u) (G : Type v) [CommRing R]
[TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
Carrier R G → R :=
fun x => completedGroupAlgebraStageAugmentation R G U (completedGroupAlgebraProjection R G U x)The completed augmentation evaluated at a finite stage.
theorem completedGroupAlgebraAugmentationAt_eq_of_le
{U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (x : Carrier R G) :
completedGroupAlgebraAugmentationAt R G U x =
completedGroupAlgebraAugmentationAt R G V xThe coordinate defining the completed augmentation is independent of the chosen sufficiently terminal index.
Show proof
by
unfold completedGroupAlgebraAugmentationAt
have hcomp := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageAugmentation_compatible (R := R) (G := G)
(U := U) (V := V) hUV))
(completedGroupAlgebraProjection R G V x)
calc
completedGroupAlgebraStageAugmentation R G U (completedGroupAlgebraProjection R G U x)
=
completedGroupAlgebraStageAugmentation R G U
(completedGroupAlgebraTransition R G hUV (completedGroupAlgebraProjection R G V x)) := by
rw [← completedGroupAlgebraProjection_compatible (R := R) (G := G) x hUV]
_ = completedGroupAlgebraStageAugmentation R G V
(completedGroupAlgebraProjection R G V x) := hcompProof. 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. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). 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 the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement.
□def completedGroupAlgebraCanonicalAugmentation (R : Type u) (G : Type v) [CommRing R]
[TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] :
Carrier R G →+* R where
toFun := completedGroupAlgebraAugmentationAt R G (terminalCompletedGroupAlgebraIndex G)
map_zero' := by
unfold completedGroupAlgebraAugmentationAt
simp only [InverseSystem.projection_apply, coe_zero_completedGroupAlgebra, Pi.zero_apply, map_zero]
map_one' := by
unfold completedGroupAlgebraAugmentationAt
simp only [InverseSystem.projection_apply, coe_one_completedGroupAlgebra, Pi.one_apply, map_one]
map_add' x y := by
unfold completedGroupAlgebraAugmentationAt
simp only [InverseSystem.projection_apply, coe_add_completedGroupAlgebra, Pi.add_apply, map_add]
map_mul' x y := by
unfold completedGroupAlgebraAugmentationAt
simp only [InverseSystem.projection_apply, coe_mul_completedGroupAlgebra, Pi.mul_apply, map_mul]The canonical augmentation \(\varepsilon:\widehat{R[G]}\to R\) is the ring homomorphism obtained by applying the finite-stage augmentation to any sufficiently terminal coordinate.
theorem completedGroupAlgebraCanonicalAugmentation_eq_at
(U : CompletedGroupAlgebraIndex G) (x : Carrier R G) :
completedGroupAlgebraCanonicalAugmentation R G x =
completedGroupAlgebraAugmentationAt R G U xThe canonical completed augmentation is computed at any finite stage.
Show proof
completedGroupAlgebraAugmentationAt_eq_of_le (R := R) (G := G)
(U := terminalCompletedGroupAlgebraIndex G) (V := U)
(terminalCompletedGroupAlgebraIndex_le (G := G) U) 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. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). 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. For the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement.
□theorem completedGroupAlgebraStageAugmentation_comp_projectionRingHom
(U : CompletedGroupAlgebraIndex G) :
(completedGroupAlgebraStageAugmentation R G U).comp
(completedGroupAlgebraProjectionRingHom R G U) =
completedGroupAlgebraCanonicalAugmentation R GFor every finite quotient stage \(U\), projecting \(\widehat{R[G]}\) to \(R[G/U]\) and then applying the finite-stage augmentation gives the canonical augmentation on \(\widehat{R[G]}\).
Show proof
by
apply RingHom.ext
intro x
exact (completedGroupAlgebraCanonicalAugmentation_eq_at (R := R) (G := G) U x).symmProof. 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. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). 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 the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement. 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 completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra
(x : MonoidAlgebra R G) :
completedGroupAlgebraCanonicalAugmentation R G (toCompletedGroupAlgebra R G x) =
groupAlgebraAugmentation R G xThe canonical augmentation extends the abstract group-algebra augmentation through the dense algebraic map.
Show proof
by
change completedGroupAlgebraStageAugmentation R G (terminalCompletedGroupAlgebraIndex G)
(completedGroupAlgebraProjection R G (terminalCompletedGroupAlgebraIndex G)
(toCompletedGroupAlgebra R G x)) = groupAlgebraAugmentation R G x
rw [completedGroupAlgebraProjection_toCompletedGroupAlgebra]
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageAugmentation_comp_stageMap (R := R) (G := G)
(terminalCompletedGroupAlgebraIndex 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, 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. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). 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 the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement.
□theorem completedGroupAlgebraCanonicalAugmentation_comp_toCompletedGroupAlgebra :
(completedGroupAlgebraCanonicalAugmentation R G).comp
(toCompletedGroupAlgebraRingHom R G) =
groupAlgebraAugmentation R GComposing the canonical augmentation with the dense map gives the abstract augmentation.
Show proof
by
apply RingHom.ext
intro x
exact completedGroupAlgebraCanonicalAugmentation_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. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). 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 the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement.
□theorem completedGroupAlgebraCanonicalAugmentation_comp_coeffMap
(S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
(f : R →+* S) :
(completedGroupAlgebraCanonicalAugmentation S G).comp
(completedGroupAlgebraCoeffMap (R := R) (G := G) S f) =
f.comp (completedGroupAlgebraCanonicalAugmentation R G)Canonical augmentation is natural in the coefficient ring.
Show proof
by
apply RingHom.ext
intro x
change
completedGroupAlgebraStageAugmentation S G (terminalCompletedGroupAlgebraIndex G)
(completedGroupAlgebraProjection S G (terminalCompletedGroupAlgebraIndex G)
(completedGroupAlgebraCoeffMap (R := R) (G := G) S f x)) =
f (completedGroupAlgebraStageAugmentation R G (terminalCompletedGroupAlgebraIndex G)
(completedGroupAlgebraProjection R G (terminalCompletedGroupAlgebraIndex G) x))
rw [completedGroupAlgebraProjection_coeffMap]
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageAugmentation_comp_stageCoeffMap
(R := R) (G := G) S f (terminalCompletedGroupAlgebraIndex G)))
(completedGroupAlgebraProjection R G (terminalCompletedGroupAlgebraIndex G) x)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. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). 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 the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement.
□theorem completedGroupAlgebraCanonicalAugmentation_map
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
(x : Carrier R G) :
completedGroupAlgebraCanonicalAugmentation R H
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x) =
completedGroupAlgebraCanonicalAugmentation R G xCanonical augmentation is natural with respect to functorial completed group-algebra maps.
Show proof
by
let V : CompletedGroupAlgebraIndex H := terminalCompletedGroupAlgebraIndex H
calc
completedGroupAlgebraCanonicalAugmentation R H
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x)
=
completedGroupAlgebraAugmentationAt R H V
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x) := by
exact completedGroupAlgebraCanonicalAugmentation_eq_at (R := R) (G := H) V
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x)
_ =
completedGroupAlgebraStageAugmentation R H V
(completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) hG φ hφ V
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)) := by
rw [completedGroupAlgebraAugmentationAt, completedGroupAlgebraProjection_map]
_ =
completedGroupAlgebraStageAugmentation R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V)
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x) := by
have hstage := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageAugmentation_comp_functorialStageMap
(R := R) (G := G) (H := H) hG φ hφ V))
(completedGroupAlgebraProjection R G
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x)
exact hstage
_ =
completedGroupAlgebraCanonicalAugmentation R G x := by
exact (completedGroupAlgebraCanonicalAugmentation_eq_at (R := R) (G := G)
(completedGroupAlgebraComapIndex (G := G) hG φ hφ V) x).symmProof. 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. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). 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 the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement.
□theorem completedGroupAlgebraCanonicalAugmentation_comp_map
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) :
(completedGroupAlgebraCanonicalAugmentation R H).comp
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ) =
completedGroupAlgebraCanonicalAugmentation R GCanonical augmentation after the functorial completed map agrees with canonical augmentation.
Show proof
by
apply RingHom.ext
intro x
exact completedGroupAlgebraCanonicalAugmentation_map (R := R) (G := G) (H := H) hG φ hφ 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. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). 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 the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement.
□theorem completedGroupAlgebraCanonicalAugmentation_of (g : G) :
completedGroupAlgebraCanonicalAugmentation R G (completedGroupAlgebraOf R G g) = 1The canonical augmentation sends every completed group-like element to one.
Show proof
by
rw [completedGroupAlgebraOf,
completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra]
simp only [MonoidAlgebra.of_apply, groupAlgebraAugmentation_single]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. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). 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 the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement.
□theorem completedGroupAlgebraCanonicalAugmentation_surjective :
Function.Surjective (completedGroupAlgebraCanonicalAugmentation R G)The canonical augmentation \(\varepsilon:\widehat{R[G]}\to R\) is surjective.
Show proof
by
intro r
refine ⟨toCompletedGroupAlgebra R G (algebraMap R (MonoidAlgebra R G) r), ?_⟩
rw [completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra]
simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
groupAlgebraAugmentation_single]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. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). Surjectivity is obtained by lifting a representative through the underlying surjective quotient or group homomorphism and then checking the defining finite-stage formula. 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 the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement.
□theorem continuous_completedGroupAlgebraCanonicalAugmentation :
Continuous (completedGroupAlgebraCanonicalAugmentation R G)The canonical augmentation \(\varepsilon:\widehat{R[G]}\to R\) is continuous for the inverse-limit topology on \(\widehat{R[G]}\).
Show proof
by
let U := terminalCompletedGroupAlgebraIndex G
letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
(completedGroupAlgebraSystem R G).topologicalSpace U
change Continuous fun x : Carrier R G =>
completedGroupAlgebraStageAugmentation R G U (completedGroupAlgebraProjection R G U x)
exact (finiteGroupAlgebra_augmentation_continuous R (CompletedGroupAlgebraQuotient G U)).comp
((completedGroupAlgebraSystem R G).continuous_projection U)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. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). 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 the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the 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.
□