CompletedGroupAlgebra.Basic.InClass.Index
Completed Group Algebra / Basic / Within a Class / Index.
abbrev CompletedGroupAlgebraIndexInClass (C : ProCGroups.FiniteGroupClass.{v}) :=
OrderDual (OpenNormalSubgroupInClass C G)The \(C\)-indexed open-normal quotient tower for a completed group algebra. The order is chosen so that larger indices give finer quotients.
abbrev CompletedGroupAlgebraQuotientInClass (C : ProCGroups.FiniteGroupClass.{v})
(U : CompletedGroupAlgebraIndexInClass G C) : Type v :=
(openNormalSubgroupInClassSystem C G).X Utheorem finite_completedGroupAlgebraQuotientInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) :
Finite (CompletedGroupAlgebraQuotientInClass G C U)Quotients appearing in a finite quotient class are finite.
Show proof
hC (OrderDual.ofDual U).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. 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 quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□def terminalCompletedGroupAlgebraIndexInClass
(C : ProCGroups.FiniteGroupClass.{v})
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
CompletedGroupAlgebraIndexInClass G C :=
OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := G))The terminal \(C\)-indexed completed-group-algebra quotient, corresponding to \(G/G\).
theorem terminalCompletedGroupAlgebraIndexInClass_le
(C : ProCGroups.FiniteGroupClass.{v})
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(U : CompletedGroupAlgebraIndexInClass G C) :
terminalCompletedGroupAlgebraIndexInClass (G := G) C ≤ UThe terminal in-class completed-group-algebra index is below every in-class index.
Show proof
by
change ((OrderDual.ofDual U).1 : Subgroup G) ≤ (⊤ : Subgroup G)
exact le_topProof. 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. 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. 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.
□