CompletedGroupAlgebra.Augmentation.Functoriality
This module develops the augmentation side of the construction. It identifies the relevant kernels and ideals and compares the finite-stage and completed forms.
theorem completedGroupAlgebraCanonicalAugmentationInClass_map
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := H) C hC
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x) =
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC xThe in-class canonical augmentation is natural under functorial completed maps.
Show proof
by
let V : CompletedGroupAlgebraIndexInClass H C :=
terminalCompletedGroupAlgebraIndexInClass (G := H) C
calc
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := H) C hC
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x)
=
completedGroupAlgebraAugmentationAtInClass C R H hC V
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x) := by
exact completedGroupAlgebraCanonicalAugmentationInClass_eq_at
(R := R) (G := H) C hC V
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x)
_ =
completedGroupAlgebraStageAugmentationInClass C R H V
(completedGroupAlgebraFunctorialStageMapInClass
(G := G) (H := H) C hHer (R := R) φ hφ V
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)) := by
rw [completedGroupAlgebraAugmentationAtInClass, completedGroupAlgebraProjectionInClass_map]
_ =
completedGroupAlgebraStageAugmentationInClass C R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x) := by
have hstage := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraStageAugmentationInClass_comp_functorialStageMapInClass
(R := R) (G := G) (H := H) C hHer φ hφ V))
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
exact hstage
_ =
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC x := by
exact (completedGroupAlgebraCanonicalAugmentationInClass_eq_at
(R := R) (G := G) C hC
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ 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. 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_comp_map
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) :
(completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := H) C hC).comp
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ) =
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hCComposing an in-class completed map with augmentation gives the source augmentation.
Show proof
by
apply RingHom.ext
intro x
exact completedGroupAlgebraCanonicalAugmentationInClass_map
(R := R) (G := G) (H := H) C hC hHer φ 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. 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 completedGroupAlgebraMapInClass_mem_canonicalAugmentationIdeal_iff
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ)
(x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ x ∈
completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C hC ↔
x ∈ completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hCA functorial in-class completed group-algebra map preserves and reflects membership in the canonical augmentation ideal.
Show proof
by
rw [mem_completedGroupAlgebraCanonicalAugmentationIdealInClass_iff,
mem_completedGroupAlgebraCanonicalAugmentationIdealInClass_iff,
completedGroupAlgebraCanonicalAugmentationInClass_map]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\). 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. 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. 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 completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_map
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) :
Ideal.comap (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ)
(completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C hC) =
completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hCThe \(C\)-indexed canonical augmentation ideal is pulled back to itself by functorial maps.
Show proof
by
ext x
exact completedGroupAlgebraMapInClass_mem_canonicalAugmentationIdeal_iff
(R := R) (G := G) (H := H) C hC hHer φ 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\). 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. 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 completedGACanonicalAugmentationIdealInClass_map_functorial_of_surj
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(hR : IsProfiniteRing R) (hH : IsProCGroup C H)
(φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ) :
Ideal.map (completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ)
(completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC) =
completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C hCA surjective functorial map sends the \(C\)-indexed canonical augmentation ideal onto the target canonical augmentation ideal.
Show proof
by
rw [← completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_map
(R := R) (G := G) (H := H) C hC hHer φ hφ]
exact Ideal.map_comap_of_surjective
(completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ)
(completedGroupAlgebraMapInClass_surjective_of_surjective
(R := R) (G := G) (H := H) C hC hForm hHer hR hH φ hφ hφsurj)
(completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C hC)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\). 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 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.
□