CompletedGroupAlgebra.Augmentation.AugmentationIdeal
This module develops the augmentation side of the construction. It identifies the relevant kernels and ideals and compares the finite-stage and completed forms.
def completedGroupAlgebraCanonicalAugmentationIdealInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
Ideal (CompletedGroupAlgebraInClass C hC R G) :=
RingHom.ker (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC)The canonical augmentation ideal of the \(C\)-indexed completed group algebra.
theorem mem_completedGroupAlgebraCanonicalAugmentationIdealInClass_iff
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(x : CompletedGroupAlgebraInClass C hC R G) :
x ∈ completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC ↔
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC x = 0An in-class completed group-algebra element lies in the canonical augmentation ideal iff the in-class canonical augmentation sends it to zero.
Show proof
Iff.rflProof. 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\). 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. 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_subtype_injective
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
Function.Injective
(fun x : completedGroupAlgebraCanonicalAugmentationIdealInClass
(R := R) (G := G) C hC => (x : CompletedGroupAlgebraInClass C hC R G))The inclusion of the \(C\)-indexed canonical augmentation ideal is injective.
Show proof
by
intro x y hxy
exact Subtype.ext hxyProof. 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\). 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. Injectivity follows because two elements with identical finite-stage coordinates are equal in the inverse limit, and subtype inclusions are injective on their underlying elements. 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 exact_completedGroupAlgebraCanonicalAugmentationIdealInClass_subtype
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
Function.Exact
(fun x : completedGroupAlgebraCanonicalAugmentationIdealInClass
(R := R) (G := G) C hC => (x : CompletedGroupAlgebraInClass C hC R G))
(completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC)The \(C\)-indexed canonical augmentation ideal is exactly the kernel of the canonical augmentation.
Show proof
by
intro x
constructor
· intro hx
exact ⟨⟨x, hx⟩, rfl⟩
· rintro ⟨y, rfl⟩
exact y.2Proof. 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\). 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. 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_shortExact
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
Function.Injective
(fun x : completedGroupAlgebraCanonicalAugmentationIdealInClass
(R := R) (G := G) C hC => (x : CompletedGroupAlgebraInClass C hC R G)) ∧
Function.Exact
(fun x : completedGroupAlgebraCanonicalAugmentationIdealInClass
(R := R) (G := G) C hC => (x : CompletedGroupAlgebraInClass C hC R G))
(completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC) ∧
Function.Surjective
(completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC)The canonical augmentation sequence with augmentation ideal as kernel is short exact: the inclusion is injective, its image is the kernel of augmentation, and the augmentation is surjective.
Show proof
by
exact ⟨completedGroupAlgebraCanonicalAugmentationIdealInClass_subtype_injective
(R := R) (G := G) C hC,
exact_completedGroupAlgebraCanonicalAugmentationIdealInClass_subtype
(R := R) (G := G) C hC,
completedGroupAlgebraCanonicalAugmentationInClass_surjective (R := R) (G := G) 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. 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. Injectivity follows because two elements with identical finite-stage coordinates are equal in the inverse limit, and subtype inclusions are injective on their underlying elements. 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_of
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] (g : G) :
completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
(completedGroupAlgebraOfInClass C hC R G g) = 1The in-class canonical augmentation sends every completed group-like element to one.
Show proof
by
rw [completedGroupAlgebraOfInClass,
canonicalAugmentationInClass_toCompleted]
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, 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.
□