CompletedGroupAlgebra.Augmentation.CanonicalAugmentation
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.
def completedGroupAlgebraAugmentationAtInClass
(C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
[TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) :
CompletedGroupAlgebraInClass C hC R G → R :=
fun x => completedGroupAlgebraStageAugmentationInClass C R G U
(completedGroupAlgebraProjectionInClass C hC R G U x)The \(C\)-indexed completed augmentation evaluated at a finite stage.
theorem completedGroupAlgebraAugmentationAtInClass_eq_of_le
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
(x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraAugmentationAtInClass C R G hC U x =
completedGroupAlgebraAugmentationAtInClass C R G hC V xThe augmentation value read at a finer in-class stage agrees after transition.
Show proof
by
unfold completedGroupAlgebraAugmentationAtInClass
have hcomp := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageAugmentationInClass_compatible
(R := R) (G := G) C (U := U) (V := V) hUV))
(completedGroupAlgebraProjectionInClass C hC R G V x)
calc
completedGroupAlgebraStageAugmentationInClass C R G U
(completedGroupAlgebraProjectionInClass C hC R G U x)
=
completedGroupAlgebraStageAugmentationInClass C R G U
(completedGroupAlgebraTransitionInClass C R G hUV
(completedGroupAlgebraProjectionInClass C hC R G V x)) := by
rw [← completedGroupAlgebraProjectionInClass_compatible
(R := R) (G := G) C hC hUV x]
_ =
completedGroupAlgebraStageAugmentationInClass C R G V
(completedGroupAlgebraProjectionInClass C hC 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, 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□def completedGroupAlgebraCanonicalAugmentationInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
CompletedGroupAlgebraInClass C hC R G →+* R :=
(completedGroupAlgebraStageAugmentationInClass C R G
(terminalCompletedGroupAlgebraIndexInClass (G := G) C)).comp
(completedGroupAlgebraProjectionRingHomInClass C hC R G
(terminalCompletedGroupAlgebraIndexInClass (G := G) C))The canonical augmentation on the \(C\)-indexed completed group algebra.
theorem completedGroupAlgebraCanonicalAugmentationInClass_eq_at
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC x =
completedGroupAlgebraAugmentationAtInClass C R G hC U xThe in-class canonical augmentation can be computed at any in-class stage.
Show proof
completedGroupAlgebraAugmentationAtInClass_eq_of_le (R := R) (G := G) C hC
(U := terminalCompletedGroupAlgebraIndexInClass (G := G) C) (V := U)
(terminalCompletedGroupAlgebraIndexInClass_le (G := G) C 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, 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. 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. 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 completedGroupAlgebraStageAugmentationInClass_comp_projectionRingHomInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(U : CompletedGroupAlgebraIndexInClass G C) :
(completedGroupAlgebraStageAugmentationInClass C R G U).comp
(completedGroupAlgebraProjectionRingHomInClass C hC R G U) =
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hCStage augmentation after projection is the in-class canonical augmentation.
Show proof
by
apply RingHom.ext
intro x
exact (completedGroupAlgebraCanonicalAugmentationInClass_eq_at
(R := R) (G := G) C hC 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. 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. 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 canonicalAugmentationInClass_toCompleted
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] (x : MonoidAlgebra R G) :
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
(toCompletedGroupAlgebraInClass C hC R G x) =
groupAlgebraAugmentation R G xThe in-class canonical augmentation extends the abstract augmentation on the dense algebraic map.
Show proof
by
change completedGroupAlgebraStageAugmentationInClass C R G
(terminalCompletedGroupAlgebraIndexInClass (G := G) C)
(completedGroupAlgebraProjectionInClass C hC R G
(terminalCompletedGroupAlgebraIndexInClass (G := G) C)
(toCompletedGroupAlgebraInClass C hC R G x)) =
groupAlgebraAugmentation R G x
rw [completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass]
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageAugmentationInClass_comp_stageMapInClass
(R := R) (G := G) C (terminalCompletedGroupAlgebraIndexInClass (G := G) C)))
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\). 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. 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. 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 completedGACanonicalAugmentationInClass_comp_toCompletedGAInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
(completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC).comp
(toCompletedGroupAlgebraInClassRingHom C hC R G) =
groupAlgebraAugmentation R GComposing the dense in-class map with canonical augmentation gives abstract augmentation.
Show proof
by
apply RingHom.ext
intro x
exact canonicalAugmentationInClass_toCompleted
(R := R) (G := G) C hC 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\). 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. 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. 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 completedGroupAlgebraCanonicalAugmentationInClass_comp_coeffMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
(f : R →+* S) :
(completedGroupAlgebraCanonicalAugmentationInClass (R := S) (G := G) C hC).comp
(completedGroupAlgebraCoeffMapInClass (R := R) (G := G) C hC S f) =
f.comp (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC)In-class canonical augmentation is natural in the coefficient ring.
Show proof
by
apply RingHom.ext
intro x
let U := terminalCompletedGroupAlgebraIndexInClass (G := G) C
change
completedGroupAlgebraStageAugmentationInClass C S G U
(completedGroupAlgebraProjectionInClass C hC S G U
(completedGroupAlgebraCoeffMapInClass (R := R) (G := G) C hC S f x)) =
f (completedGroupAlgebraStageAugmentationInClass C R G U
(completedGroupAlgebraProjectionInClass C hC R G U x))
rw [completedGroupAlgebraProjectionInClass_coeffMap]
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMapInClass
(R := R) (G := G) C S f U))
(completedGroupAlgebraProjectionInClass C hC R G U 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\). 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. 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 completedGroupAlgebraCanonicalAugmentationInClass_algebraMap
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] (r : R) :
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
(algebraMap R (CompletedGroupAlgebraInClass C hC R G) r) = rThe in-class canonical augmentation sends scalar algebra-map elements to their scalar.
Show proof
by
let U := terminalCompletedGroupAlgebraIndexInClass (G := G) C
calc
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
(algebraMap R (CompletedGroupAlgebraInClass C hC R G) r)
=
completedGroupAlgebraStageAugmentationInClass C R G U
(completedGroupAlgebraProjectionInClass C hC R G U
(algebraMap R (CompletedGroupAlgebraInClass C hC R G) r)) := rfl
_ =
completedGroupAlgebraStageAugmentationInClass C R G U
(algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r) := by
change completedGroupAlgebraStageAugmentationInClass C R G U
(completedGroupAlgebraProjectionInClass C hC R G U
(completedGroupAlgebraAlgebraMapInClass (R := R) (G := G) C hC r)) =
completedGroupAlgebraStageAugmentationInClass C R G U
(algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r)
exact congrArg (completedGroupAlgebraStageAugmentationInClass C R G U)
(completedGroupAlgebraProjectionInClass_algebraMap
(R := R) (G := G) C hC U r)
_ = r := by
simp only [completedGroupAlgebraStageAugmentationInClass, 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, 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. 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. 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 completedGroupAlgebraCanonicalAugmentationInClass_surjective
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
Function.Surjective
(completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC)The \(C\)-indexed canonical augmentation \(\varepsilon_C:\widehat{R[G]}_C\to R\) is surjective.
Show proof
by
intro r
refine ⟨algebraMap R (CompletedGroupAlgebraInClass C hC R G) r, ?_⟩
simp only [completedGroupAlgebraCanonicalAugmentationInClass_algebraMap]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\). 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. 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. 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_completedGroupAlgebraCanonicalAugmentationInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
Continuous (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC)The \(C\)-indexed canonical augmentation is continuous for the inverse-limit topology on \(\widehat{R[G]}_C\).
Show proof
by
let U := terminalCompletedGroupAlgebraIndexInClass (G := G) C
letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
finite_completedGroupAlgebraQuotientInClass G C hC U
letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
(completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
change Continuous fun x : CompletedGroupAlgebraInClass C hC R G =>
completedGroupAlgebraStageAugmentationInClass C R G U
(completedGroupAlgebraProjectionInClass C hC R G U x)
exact (finiteGroupAlgebra_augmentation_continuous R
(CompletedGroupAlgebraQuotientInClass G C U)).comp
((completedGroupAlgebraSystemInClass C hC 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\). 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. 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 completedGroupAlgebraInClass_hasCompletedGroupAlgebraAugmentation
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
hasCompletedGroupAlgebraAugmentation R G (CompletedGroupAlgebraInClass C hC R G)
(toCompletedGroupAlgebraInClassRingHom C hC R G)The \(C\)-indexed completed group algebra carries the standard model-independent augmentation package.
Show proof
by
refine ⟨completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC, ?_, ?_⟩
· exact completedGACanonicalAugmentationInClass_comp_toCompletedGAInClass
(R := R) (G := G) C hC
· exact continuous_completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hCProof. 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. 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. 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.
□