CompletedGroupAlgebra.AllFiniteAugmentation.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.
import
def completedGroupAlgebraCanonicalAugmentationIdeal (R : Type u) (G : Type v) [CommRing R]
[TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] : Ideal (Carrier R G) :=
RingHom.ker (completedGroupAlgebraCanonicalAugmentation R G)The canonical augmentation ideal \(I_G\subseteq \widehat{R[G]}\) is the kernel of the completed augmentation \(\varepsilon:\widehat{R[G]}\to R\).
theorem mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff
(x : Carrier R G) :
x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R G ↔
completedGroupAlgebraCanonicalAugmentation R G x = 0An all-finite completed group-algebra element lies in the canonical augmentation ideal iff the 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. 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 completedGroupAlgebraCanonicalAugmentationIdeal_subtype_injective :
Function.Injective
(fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
(x : Carrier R G))The inclusion of the canonical completed 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, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. 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. 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_completedGroupAlgebraCanonicalAugmentationIdeal_subtype :
Function.Exact
(fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
(x : Carrier R G))
(completedGroupAlgebraCanonicalAugmentation R G)The canonical completed 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. 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_shortExact :
Function.Injective
(fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
(x : Carrier R G)) ∧
Function.Exact
(fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
(x : Carrier R G))
(completedGroupAlgebraCanonicalAugmentation R G) ∧
Function.Surjective (completedGroupAlgebraCanonicalAugmentation R G)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 ⟨completedGroupAlgebraCanonicalAugmentationIdeal_subtype_injective (R := R) (G := G),
exact_completedGroupAlgebraCanonicalAugmentationIdeal_subtype (R := R) (G := G),
completedGroupAlgebraCanonicalAugmentation_surjective (R := R) (G := G)⟩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, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. 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. 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 completedGroupAlgebraCanonicalAugmentationIdeal_comap_fromInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
Ideal.comap (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG)
(completedGroupAlgebraCanonicalAugmentationIdeal R G) =
completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hCThe all-finite augmentation ideal pulls back along the from-in-class comparison map to the class-indexed augmentation ideal.
Show proof
by
ext x
rw [Ideal.mem_comap, mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff,
mem_completedGroupAlgebraCanonicalAugmentationIdealInClass_iff,
completedGroupAlgebraFromInClassRingHom_apply,
completedGroupAlgebraCanonicalAugmentation_fromInClass]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. 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 completedGroupAlgebraCanonicalAugmentationIdealInClass_map_fromInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
Ideal.map (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG)
(completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC) =
completedGroupAlgebraCanonicalAugmentationIdeal R GThe from-in-class comparison map sends the class-indexed augmentation ideal into the all-finite augmentation ideal.
Show proof
by
rw [← completedGroupAlgebraCanonicalAugmentationIdeal_comap_fromInClass
(R := R) (G := G) C hC hForm hG]
exact Ideal.map_comap_of_surjective
(completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG)
(completedGroupAlgebraFromInClass_surjective (R := R) (G := G) C hC hForm hG)
(completedGroupAlgebraCanonicalAugmentationIdeal R G)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. 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 completedGroupAlgebraToInClass_mem_canonicalAugmentationIdeal_iff
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(x : Carrier R G) :
completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC x ∈
completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC ↔
x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R GThe all-finite-to-in-class comparison map preserves and reflects membership in the canonical augmentation ideal.
Show proof
by
rw [mem_completedGroupAlgebraCanonicalAugmentationIdealInClass_iff,
mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff]
have haug := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraCanonicalAugmentationInClass_comp_toInClass
(R := R) (G := G) C hC))
x
change completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C hC
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC x) =
completedGroupAlgebraCanonicalAugmentation R G x at haug
rw [haug]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. 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_comap_toInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
Ideal.comap (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)
(completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hC) =
completedGroupAlgebraCanonicalAugmentationIdeal R GThe class-indexed augmentation ideal pulls back along the to-in-class comparison map to the all-finite augmentation ideal.
Show proof
by
ext x
exact completedGroupAlgebraToInClass_mem_canonicalAugmentationIdeal_iff
(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\). 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 completedGroupAlgebraCanonicalAugmentationIdeal_map_toInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
Ideal.map (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)
(completedGroupAlgebraCanonicalAugmentationIdeal R G) =
completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C hCThe to-in-class comparison map sends the all-finite augmentation ideal into the class-indexed augmentation ideal.
Show proof
by
rw [← completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_toInClass
(R := R) (G := G) C hC]
exact Ideal.map_comap_of_surjective
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)
(completedGroupAlgebraToInClass_surjective (R := R) (G := G) C hC hForm hG)
(completedGroupAlgebraCanonicalAugmentationIdealInClass (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. 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 completedGroupAlgebraMap_sub_one_of
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) (g : G) :
completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ
(completedGroupAlgebraOf R G g - 1) =
completedGroupAlgebraOf R H (φ g) - 1A functorial all-finite completed group-algebra map sends augmentation generators to their images.
Show proof
by
rw [map_sub, completedGroupAlgebraMap_of, map_one]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. 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 completedGroupAlgebraMap_mem_canonicalAugmentationIdeal_iff
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ)
(x : Carrier R G) :
completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ x ∈
completedGroupAlgebraCanonicalAugmentationIdeal R H ↔
x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R GA functorial all-finite completed group-algebra map preserves and reflects membership in the canonical augmentation ideal.
Show proof
by
rw [mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff,
mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff,
completedGroupAlgebraCanonicalAugmentation_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, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. 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 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 completedGroupAlgebraCanonicalAugmentationIdeal_comap_map
(hG : ProCGroups.IsProfiniteGroup G) (φ : G →* H) (hφ : Continuous φ) :
Ideal.comap (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)
(completedGroupAlgebraCanonicalAugmentationIdeal R H) =
completedGroupAlgebraCanonicalAugmentationIdeal R GPulling back the target canonical augmentation ideal along a completed group-algebra map gives the source canonical augmentation ideal.
Show proof
by
ext x
exact completedGroupAlgebraMap_mem_canonicalAugmentationIdeal_iff
(R := R) (G := G) (H := H) hG φ 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. 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 completedGroupAlgebraCanonicalAugmentationIdeal_map_functorial_of_surjective
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G)
(hH : ProCGroups.IsProfiniteGroup H) (φ : G →* H) (hφ : Continuous φ)
(hφsurj : Function.Surjective φ) :
Ideal.map (completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)
(completedGroupAlgebraCanonicalAugmentationIdeal R G) =
completedGroupAlgebraCanonicalAugmentationIdeal R HA surjective functorial map sends the canonical completed augmentation ideal onto the target canonical augmentation ideal.
Show proof
by
rw [← completedGroupAlgebraCanonicalAugmentationIdeal_comap_map
(R := R) (G := G) (H := H) hG φ hφ]
exact Ideal.map_comap_of_surjective
(completedGroupAlgebraMap (G := G) (H := H) R hG φ hφ)
(completedGroupAlgebraMap_surjective_of_surjective
(R := R) (G := G) (H := H) hR hG hH φ hφ hφsurj)
(completedGroupAlgebraCanonicalAugmentationIdeal R H)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. 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.
□