CompletedGroupAlgebra.Basic.AllFinite.Index
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
abbrev CompletedGroupAlgebraIndex :=
OrderDual (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G)The index set for the Section 5.3 completed group algebra tower, ordered so that larger indices give finer finite quotients.
abbrev CompletedGroupAlgebraQuotient (U : CompletedGroupAlgebraIndex G) : Type v :=
(openNormalSubgroupInClassSystem ProCGroups.FiniteGroupClass.allFinite G).X Uinstance instFiniteCompletedGroupAlgebraQuotient
(U : CompletedGroupAlgebraIndex G) :
Finite (CompletedGroupAlgebraQuotient G U) :=
(OrderDual.ofDual U).2The finite completed group-algebra quotient is finite.
def terminalCompletedGroupAlgebraSubgroup : Subgroup G where
carrier := Set.univ
one_mem' := by simp only [Set.mem_univ]
mul_mem' := by intro a b ha hb; simp only [Set.mem_univ]
inv_mem' := by intro a ha; simp only [Set.mem_univ]The whole group \(G\), as a subgroup, used for the terminal quotient \(G/G\).
def terminalCompletedGroupAlgebraOpenSubgroup : OpenSubgroup G :=
OpenSubgroup.mk (terminalCompletedGroupAlgebraSubgroup G) isOpen_univThe whole group \(G\) is an open subgroup.
def terminalCompletedGroupAlgebraOpenNormalSubgroup : OpenNormalSubgroup G :=
OpenNormalSubgroup.mk (terminalCompletedGroupAlgebraOpenSubgroup G)
(Subgroup.Normal.mk (by
intro n hn g
simp only [terminalCompletedGroupAlgebraOpenSubgroup, terminalCompletedGroupAlgebraSubgroup, Subgroup.mem_mk,
Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_univ]))The whole group \(G\) is an open normal subgroup.
theorem terminalCompletedGroupAlgebraOpenNormalSubgroup_coe :
((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) : Subgroup G) =
⊤Show proof
by
ext g
simp only [terminalCompletedGroupAlgebraOpenNormalSubgroup, terminalCompletedGroupAlgebraOpenSubgroup,
terminalCompletedGroupAlgebraSubgroup, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_univ,
Subgroup.mem_top]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. 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.
□instance terminalCompletedGroupAlgebraQuotient_subsingleton :
Subsingleton
(G ⧸ ((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :
Subgroup G)) := by
rw [terminalCompletedGroupAlgebraOpenNormalSubgroup_coe (G := G)]
constructor
intro x y
rcases QuotientGroup.mk'_surjective (⊤ : Subgroup G) x with ⟨a, rfl⟩
rcases QuotientGroup.mk'_surjective (⊤ : Subgroup G) y with ⟨b, rfl⟩
exact (QuotientGroup.eq).2 (by simp only [Subgroup.mem_top])The terminal completed group-algebra quotient is a subsingleton, since it is the quotient by the whole group.
def terminalCompletedGroupAlgebraSubgroupInClass :
OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G := by
refine ⟨terminalCompletedGroupAlgebraOpenNormalSubgroup G, ?_⟩
letI : Subsingleton
(G ⧸ ((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :
Subgroup G)) :=
terminalCompletedGroupAlgebraQuotient_subsingleton (G := G)
exact Finite.of_subsingletondef terminalCompletedGroupAlgebraIndex : CompletedGroupAlgebraIndex G :=
OrderDual.toDual (terminalCompletedGroupAlgebraSubgroupInClass G)instance instNonemptyCompletedGroupAlgebraIndex :
Nonempty (CompletedGroupAlgebraIndex G) :=
⟨terminalCompletedGroupAlgebraIndex G⟩The completed group algebra is nonempty, with the terminal quotient or canonical base object as witness.
theorem terminalCompletedGroupAlgebraIndex_le (U : CompletedGroupAlgebraIndex G) :
terminalCompletedGroupAlgebraIndex G ≤ UShow proof
by
change ((OrderDual.ofDual U).1 : Subgroup G) ≤
((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) : Subgroup G)
rw [terminalCompletedGroupAlgebraOpenNormalSubgroup_coe (G := G)]
intro g hg
simp only [Subgroup.mem_top]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.
□def completedGroupAlgebraIndexInClassToAllFinite
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) : CompletedGroupAlgebraIndex G :=
OrderDual.toDual ⟨(OrderDual.ofDual U).1, hC (OrderDual.ofDual U).2⟩A quotient indexed by a finite quotient class is also an all-finite quotient.
theorem completedGroupAlgebraIndexInClassToAllFinite_le
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
completedGroupAlgebraIndexInClassToAllFinite G C hC U ≤
completedGroupAlgebraIndexInClassToAllFinite G C hC VThe comparison of all-finite and class-indexed indices is monotone.
Show proof
by
change ((OrderDual.ofDual V).1 : Subgroup G) ≤ ((OrderDual.ofDual U).1 : Subgroup G)
exact hUVProof. 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.
□def completedGroupAlgebraIndexToInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
(hG : IsProCGroup C G)
(U : CompletedGroupAlgebraIndex G) : CompletedGroupAlgebraIndexInClass G C :=
OrderDual.toDual ⟨(OrderDual.ofDual U).1,
IsProCGroup.quotient_mem (C := C) hForm hG
((OrderDual.ofDual U).1 : OpenNormalSubgroup G)⟩theorem completedGroupAlgebraIndexToInClass_le
(C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
(hG : IsProCGroup C G)
{U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
completedGroupAlgebraIndexToInClass G C hForm hG U ≤
completedGroupAlgebraIndexToInClass G C hForm hG VThe comparison of all-finite and class-indexed indices is monotone.
Show proof
by
change ((OrderDual.ofDual V).1 : Subgroup G) ≤ ((OrderDual.ofDual U).1 : Subgroup G)
exact hUVProof. 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 completedGroupAlgebraIndexInClassToAllFinite_indexToInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G)
(U : CompletedGroupAlgebraIndex G) :
completedGroupAlgebraIndexInClassToAllFinite G C hC
(completedGroupAlgebraIndexToInClass G C hForm hG U) = UShow proof
by
change (⟨(OrderDual.ofDual U).1,
hC (IsProCGroup.quotient_mem (C := C) hForm hG
((OrderDual.ofDual U).1 : OpenNormalSubgroup G))⟩ :
OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) = OrderDual.ofDual U
exact Subtype.ext 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, 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 completedGroupAlgebraIndexToInClass_indexInClassToAllFinite
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G)
(U : CompletedGroupAlgebraIndexInClass G C) :
completedGroupAlgebraIndexToInClass G C hForm hG
(completedGroupAlgebraIndexInClassToAllFinite G C hC U) = UFor a pro-\(C\) group, converting a \(C\)-indexed completed-group-algebra index to the all-finite tower and then back to the \(C\)-indexed tower returns the original index.
Show proof
by
change (⟨(OrderDual.ofDual U).1,
IsProCGroup.quotient_mem (C := C) hForm hG
((OrderDual.ofDual U).1 : OpenNormalSubgroup G)⟩ :
OpenNormalSubgroupInClass C G) = OrderDual.ofDual U
exact Subtype.ext 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, 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.
□