CompletedGroupAlgebra.Augmentation.StageAugmentation
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 completedGroupAlgebraStageAugmentationInClass
(C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(U : CompletedGroupAlgebraIndexInClass G C) :
CompletedGroupAlgebraStageInClass C R G U →+* R :=
groupAlgebraAugmentation R (CompletedGroupAlgebraQuotientInClass G C U)The augmentation map on one \(C\)-indexed finite stage.
theorem completedGroupAlgebraStageAugmentationInClass_of
(C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
(q : CompletedGroupAlgebraQuotientInClass G C U) :
completedGroupAlgebraStageAugmentationInClass C R G U (MonoidAlgebra.of R _ q) = 1The in-class finite-stage augmentation sends every group-like basis element to one.
Show proof
by
simp only [completedGroupAlgebraStageAugmentationInClass, 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, 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.
□theorem completedGroupAlgebraStageAugmentationInClass_single
(C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
(q : CompletedGroupAlgebraQuotientInClass G C U) (r : R) :
completedGroupAlgebraStageAugmentationInClass C R G U (MonoidAlgebra.single q r) = rThe in-class finite-stage augmentation sends a singleton to its coefficient.
Show proof
by
simp only [completedGroupAlgebraStageAugmentationInClass, 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. 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_compatible
(C : ProCGroups.FiniteGroupClass.{v})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
(completedGroupAlgebraStageAugmentationInClass C R G U).comp
(completedGroupAlgebraTransitionInClass C R G hUV) =
completedGroupAlgebraStageAugmentationInClass C R G VIn-class finite-stage augmentations are compatible with transition maps.
Show proof
by
apply RingHom.ext
intro x
exact groupAlgebraAugmentation_mapDomainRingHom R
(CompletedGroupAlgebraQuotientInClass G C V)
(CompletedGroupAlgebraQuotientInClass G C U)
(OpenNormalSubgroupInClass.map
(C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) 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. 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.
□theorem completedGroupAlgebraStageAugmentationInClass_comp_stageMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
(completedGroupAlgebraStageAugmentationInClass C R G U).comp
(completedGroupAlgebraStageMapInClass C R G U) =
groupAlgebraAugmentation R GComposing the in-class finite-stage augmentation with the stage map gives the abstract augmentation.
Show proof
by
apply RingHom.ext
intro x
exact groupAlgebraAugmentation_mapDomainRingHom R G
(CompletedGroupAlgebraQuotientInClass G C U)
(openNormalSubgroupInClassProj (C := C) (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, 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.
□theorem completedGroupAlgebraStageAugmentationInClass_comp_stageCoeffMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S]
(f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C) :
(completedGroupAlgebraStageAugmentationInClass C S G U).comp
(completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U) =
f.comp (completedGroupAlgebraStageAugmentationInClass C R G U)In-class finite-stage augmentation is natural in the coefficient ring.
Show proof
by
apply RingHom.ext
intro x
exact groupAlgebraAugmentation_mapRangeRingHom R S
(CompletedGroupAlgebraQuotientInClass G C U) f 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. 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_functorialStageMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
(completedGroupAlgebraStageAugmentationInClass C R H V).comp
(completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ V) =
completedGroupAlgebraStageAugmentationInClass C R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)In-class finite-stage augmentation is natural for functorial finite-stage maps.
Show proof
by
apply RingHom.ext
intro x
exact groupAlgebraAugmentation_mapDomainRingHom R
(CompletedGroupAlgebraQuotientInClass G C
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))
(CompletedGroupAlgebraQuotientInClass H C V)
(completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V) 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. 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.
□