CompletedGroupAlgebra.InClassFunctoriality.Comparison
Completed Group Algebra / Functoriality Within a Class / Comparison.
import
theorem completedGroupAlgebraToInClass_of
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(g : G) :
completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC
(completedGroupAlgebraOf R G g) =
completedGroupAlgebraOfInClass C hC R G gThe all-finite completed group algebra comparison sends group-like elements to the \(C\)-indexed group-like elements.
Show proof
by
change ((completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC).comp
(toCompletedGroupAlgebraRingHom R G)) (MonoidAlgebra.of R G g) =
toCompletedGroupAlgebraInClassRingHom C hC R G (MonoidAlgebra.of R G g)
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra
(R := R) (G := G) C hC))
(MonoidAlgebra.of 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. 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. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem completedGroupAlgebraToInClass_of_sub_one
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(g : G) :
completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC
(completedGroupAlgebraOf R G g - 1) =
completedGroupAlgebraOfInClass C hC R G g - 1The comparison map to a class-indexed completion sends all-finite augmentation generators to class-indexed generators.
Show proof
by
rw [map_sub, completedGroupAlgebraToInClass_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, 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\). 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. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. 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_restrictScalars_sub_one_smul
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(A : Type w) [AddCommGroup A] [Module (CompletedGroupAlgebraInClass C hC R G) A]
(g : G) (a : A) :
letI : Module (Carrier R G) AAfter restricting scalars along \(\widehat{R[G]} \to \widehat{R[G]}_C\), the all-finite augmentation generator acts as the matching \(C\)-indexed generator.
Show proof
Module.compHom A (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)
(completedGroupAlgebraOf R G g - 1) • a =
(completedGroupAlgebraOfInClass C hC R G g - 1) • a := by
letI : Module (Carrier R G) A :=
Module.compHom A (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)
change (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC
(completedGroupAlgebraOf R G g - 1)) • a =
(completedGroupAlgebraOfInClass C hC R G g - 1) • a
rw [completedGroupAlgebraToInClass_of_sub_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, 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\). 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 completedGroupAlgebraFromInClass_of
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (g : G) :
completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
(completedGroupAlgebraOfInClass C hC R G g) =
completedGroupAlgebraOf R G gThe comparison map from a class-indexed completion sends class-indexed group-like elements to all-finite group-like elements.
Show proof
by
change ((completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG).comp
(toCompletedGroupAlgebraInClassRingHom C hC R G)) (MonoidAlgebra.of R G g) =
toCompletedGroupAlgebraRingHom R G (MonoidAlgebra.of R G g)
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraFromInClassRingHom_comp_toCompletedGroupAlgebraInClass
(R := R) (G := G) C hC hForm hG))
(MonoidAlgebra.of 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. 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. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem completedGroupAlgebraFromInClass_of_sub_one
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (g : G) :
completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
(completedGroupAlgebraOfInClass C hC R G g - 1) =
completedGroupAlgebraOf R G g - 1The comparison map from a class-indexed completion sends class-indexed augmentation generators to all-finite generators.
Show proof
by
change completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG
(completedGroupAlgebraOfInClass C hC R G g - 1) =
completedGroupAlgebraOf R G g - 1
rw [map_sub, map_one]
change completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
(completedGroupAlgebraOfInClass C hC R G g) - 1 =
completedGroupAlgebraOf R G g - 1
rw [completedGroupAlgebraFromInClass_of]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\). 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. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. 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 completedGroupAlgebraFromInClass_restrictScalars_sub_one_smul
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G)
(A : Type w) [AddCommGroup A] [Module (Carrier R G) A]
(g : G) (a : A) :
letI : Module (CompletedGroupAlgebraInClass C hC R G) AAfter restricting scalars along \(\widehat{R[G]}_C \to \widehat{R[G]}\), the \(C\)-indexed augmentation generator acts as the matching all-finite generator.
Show proof
Module.compHom A (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG)
(completedGroupAlgebraOfInClass C hC R G g - 1) • a =
(completedGroupAlgebraOf R G g - 1) • a := by
letI : Module (CompletedGroupAlgebraInClass C hC R G) A :=
Module.compHom A (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG)
change (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG
(completedGroupAlgebraOfInClass C hC R G g - 1)) • a =
(completedGroupAlgebraOf R G g - 1) • a
rw [completedGroupAlgebraFromInClassRingHom_apply,
completedGroupAlgebraFromInClass_of_sub_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, 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\). 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 completedGroupAlgebraMapInClass_of
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) (g : G) :
completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
(completedGroupAlgebraOfInClass C hC R G g) =
completedGroupAlgebraOfInClass C hC R H (φ g)The class-indexed completed group-algebra map sends the completed group-like element of \(g\) to the completed group-like element of its image.
Show proof
by
simpa [completedGroupAlgebraOfInClass] using
completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_of
(R := R) (G := G) (H := H) C hC hHer φ hφ gProof. 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. 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. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem completedGroupAlgebraMapInClass_of_sub_one
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) (g : G) :
completedGroupAlgebraMapInClass (G := G) (H := H) C hC hHer R φ hφ
(completedGroupAlgebraOfInClass C hC R G g - 1) =
completedGroupAlgebraOfInClass C hC R H (φ g) - 1The class-indexed functorial map sends group-like augmentation generators to their images.
Show proof
by
rw [map_sub, completedGroupAlgebraMapInClass_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.
□