CompletedGroupAlgebra.AllFiniteAugmentation.InClassComparison
Completed Group Algebra / All Finite Augmentation / Within a Class Comparison.
theorem completedGroupAlgebraCanonicalAugmentationInClass_comp_toInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
(completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC).comp
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC) =
completedGroupAlgebraCanonicalAugmentation R GComposing the class-indexed canonical augmentation with the comparison map gives the all-finite augmentation.
Show proof
by
apply RingHom.ext
intro x
let Uc : CompletedGroupAlgebraIndexInClass G C :=
terminalCompletedGroupAlgebraIndexInClass (G := G) C
let U : CompletedGroupAlgebraIndex G :=
completedGroupAlgebraIndexInClassToAllFinite G C hC Uc
calc
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC x)
=
completedGroupAlgebraAugmentationAtInClass C R G hC Uc
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC x) := by
exact completedGroupAlgebraCanonicalAugmentationInClass_eq_at
(R := R) (G := G) C hC Uc
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC x)
_ =
completedGroupAlgebraStageAugmentationInClass C R G Uc
(completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC Uc x) := rfl
_ =
completedGroupAlgebraStageAugmentation R G U
(completedGroupAlgebraProjection R G U x) := rfl
_ = completedGroupAlgebraCanonicalAugmentation R G x := by
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. 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 completedGroupAlgebraCanonicalAugmentation_fromInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G)
(x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraCanonicalAugmentation R G
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x) =
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC xThe all-finite canonical augmentation after the comparison map from a class-indexed completion agrees with the class-indexed augmentation.
Show proof
by
have h := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraCanonicalAugmentationInClass_comp_toInClass
(R := R) (G := G) C hC))
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x)
change completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
(completedGroupAlgebraToInClass (R := R) (G := G) C hC
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x)) =
completedGroupAlgebraCanonicalAugmentation R G
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x) at h
rw [completedGroupAlgebraToInClass_fromInClass] at h
exact h.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.
□