CompletedGroupAlgebra.Basic.ClassComparison
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.
def completedGroupAlgebraProjectionToStageInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) :
Carrier R G → CompletedGroupAlgebraStageInClass C R G U :=
completedGroupAlgebraProjection R G
(completedGroupAlgebraIndexInClassToAllFinite G C hC U)
@[simp]The projection from the all-finite completed group algebra to a stage indexed by a finite quotient class \(C\).
theorem completedGroupAlgebraProjectionToStageInClass_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) (x : Carrier R G) :
completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC U x =
completedGroupAlgebraProjection R G
(completedGroupAlgebraIndexInClassToAllFinite G C hC U) xApplying the projection map to a completed element returns its corresponding finite-stage coordinate.
Show proof
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. 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. 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem completedGroupAlgebraProjectionToStageInClass_compatible
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
(x : Carrier R G) :
completedGroupAlgebraTransitionInClass C R G hUV
(completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC V x) =
completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC U xThe all-finite projection to a \(C\)-indexed stage is compatible with the transition maps of the \(C\)-indexed tower.
Show proof
by
change completedGroupAlgebraTransition R G
(completedGroupAlgebraIndexInClassToAllFinite_le (G := G) C hC hUV)
(completedGroupAlgebraProjection R G
(completedGroupAlgebraIndexInClassToAllFinite G C hC V) x) =
completedGroupAlgebraProjection R G
(completedGroupAlgebraIndexInClassToAllFinite G C hC U) x
exact completedGroupAlgebraProjection_compatible (R := R) (G := G) x
(completedGroupAlgebraIndexInClassToAllFinite_le (G := G) C hC hUV)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. 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□def completedGroupAlgebraToInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
Carrier R G → CompletedGroupAlgebraInClass C hC R G :=
(completedGroupAlgebraSystemInClass C hC R G).inverseLimitLift
(fun U => completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC U)
(by
intro U V hUV
funext x
exact completedGroupAlgebraProjectionToStageInClass_compatible
(R := R) (G := G) C hC hUV x)
@[simp]The comparison map from the ordinary all-finite completed group algebra to the inverse limit over any finite-quotient class.
theorem completedGroupAlgebraToInClass_projection
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) (x : Carrier R G) :
completedGroupAlgebraProjectionInClass C hC R G U
(completedGroupAlgebraToInClass (R := R) (G := G) C hC x) =
completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC U xProjecting the comparison map \(\widehat{R[G]}\to\widehat{R[G]}_{C}\) to a \(C\)-indexed finite stage recovers the corresponding all-finite projection.
Show proof
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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□def completedGroupAlgebraToInClassRingHom
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
Carrier R G →+* CompletedGroupAlgebraInClass C hC R G where
toFun := completedGroupAlgebraToInClass (R := R) (G := G) C hC
map_zero' := by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
rfl
map_one' := by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
rfl
map_add' x y := by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
rfl
map_mul' x y := by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
rfl
@[simp]The comparison from the all-finite completed group algebra to the \(C\)-indexed inverse limit is bundled as a ring homomorphism.
theorem completedGroupAlgebraToInClassRingHom_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(x : Carrier R G) :
completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC x =
completedGroupAlgebraToInClass (R := R) (G := G) C hC xThe comparison map from the all-finite completed group algebra to the \(C\)-indexed model is evaluated by reading the corresponding finite-stage coordinate.
Show proof
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.
□def completedGroupAlgebraToInClassAlgHom
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
Carrier R G →ₐ[R] CompletedGroupAlgebraInClass C hC R G where
toRingHom := completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC
commutes' := by
intro r
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
rfl
@[simp]The comparison from the all-finite completed group algebra to the \(C\)-indexed inverse limit, as an \(R\)-algebra homomorphism.
theorem completedGroupAlgebraToInClassAlgHom_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(x : Carrier R G) :
completedGroupAlgebraToInClassAlgHom (R := R) (G := G) C hC x =
completedGroupAlgebraToInClass (R := R) (G := G) C hC xThe comparison map from the all-finite completed group algebra to the \(C\)-indexed model is evaluated by reading the corresponding finite-stage coordinate.
Show proof
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 continuous_completedGroupAlgebraToInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
Continuous (completedGroupAlgebraToInClass (R := R) (G := G) C hC)The comparison map from the all-finite completed group algebra to the \(C\)-indexed completed group algebra is continuous for the inverse-limit topology.
Show proof
by
let S := completedGroupAlgebraSystemInClass C hC R G
letI : ∀ U : CompletedGroupAlgebraIndexInClass G C,
TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
fun U => S.topologicalSpace U
have hval : Continuous fun x : Carrier R G =>
fun U : CompletedGroupAlgebraIndexInClass G C =>
(show CompletedGroupAlgebraStageInClass C R G U from
(completedGroupAlgebraToInClass (R := R) (G := G) C hC x).1 U) := by
apply continuous_pi
intro U
change Continuous
(completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC U)
simpa [completedGroupAlgebraProjectionToStageInClass] using
(completedGroupAlgebraSystem R G).continuous_projection
(completedGroupAlgebraIndexInClassToAllFinite G C hC U)
exact Continuous.subtype_mk hval fun x =>
(completedGroupAlgebraToInClass (R := R) (G := G) C hC x).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. 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. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def completedGroupAlgebraFromInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
CompletedGroupAlgebraInClass C hC R G → Carrier R G :=
(completedGroupAlgebraSystem R G).inverseLimitLift
(fun U : CompletedGroupAlgebraIndex G =>
completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraIndexToInClass G C hForm hG U))
(by
intro U V hUV
funext x
change completedGroupAlgebraTransitionInClass C R G
(completedGroupAlgebraIndexToInClass_le (G := G) C hForm hG hUV)
(completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraIndexToInClass G C hForm hG V) x) =
completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraIndexToInClass G C hForm hG U) x
exact completedGroupAlgebraProjectionInClass_compatible
(R := R) (G := G) C hC
(completedGroupAlgebraIndexToInClass_le (G := G) C hForm hG hUV) x)
@[simp]For a pro-\(C\) group, the \(C\)-indexed inverse limit maps back to the ordinary all-finite completed group algebra by reading the same open-normal quotient stages.
theorem completedGroupAlgebraFromInClass_projection
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (U : CompletedGroupAlgebraIndex G)
(x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraProjection R G U
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x) =
completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraIndexToInClass G C hForm hG U) xProjecting the comparison map \(\widehat{R[G]}_{C}\to\widehat{R[G]}\) to an all-finite stage recovers the matching \(C\)-indexed projection.
Show proof
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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□def completedGroupAlgebraFromInClassRingHom
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
CompletedGroupAlgebraInClass C hC R G →+* Carrier R G where
toFun := completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
map_zero' := by
apply (completedGroupAlgebraSystem R G).ext
intro U
change completedGroupAlgebraProjection R G U
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG 0) =
completedGroupAlgebraProjection R G U (0 : Carrier R G)
rw [completedGroupAlgebraFromInClass_projection]
exact map_zero (completedGroupAlgebraProjectionRingHomInClass C hC R G
(completedGroupAlgebraIndexToInClass G C hForm hG U))
map_one' := by
apply (completedGroupAlgebraSystem R G).ext
intro U
change completedGroupAlgebraProjection R G U
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG 1) =
completedGroupAlgebraProjection R G U (1 : Carrier R G)
rw [completedGroupAlgebraFromInClass_projection]
exact map_one (completedGroupAlgebraProjectionRingHomInClass C hC R G
(completedGroupAlgebraIndexToInClass G C hForm hG U))
map_add' x y := by
apply (completedGroupAlgebraSystem R G).ext
intro U
change completedGroupAlgebraProjection R G U
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG (x + y)) =
completedGroupAlgebraProjection R G U
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x +
completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG y)
rw [completedGroupAlgebraFromInClass_projection]
exact map_add (completedGroupAlgebraProjectionRingHomInClass C hC R G
(completedGroupAlgebraIndexToInClass G C hForm hG U)) x y
map_mul' x y := by
apply (completedGroupAlgebraSystem R G).ext
intro U
change completedGroupAlgebraProjection R G U
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG (x * y)) =
completedGroupAlgebraProjection R G U
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x *
completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG y)
rw [completedGroupAlgebraFromInClass_projection]
exact map_mul (completedGroupAlgebraProjectionRingHomInClass C hC R G
(completedGroupAlgebraIndexToInClass G C hForm hG U)) x y
@[simp]The ring-homomorphism form of the comparison map is the bundled ring map determined by the underlying coordinate formula for the completed group algebra.
theorem completedGroupAlgebraFromInClassRingHom_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG x =
completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG xThe comparison map from the \(C\)-indexed completed group algebra to the all-finite model is evaluated by reading the corresponding finite-stage coordinate.
Show proof
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.
□def completedGroupAlgebraFromInClassAlgHom
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
CompletedGroupAlgebraInClass C hC R G →ₐ[R] Carrier R G where
toRingHom := completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG
commutes' := by
intro r
apply (completedGroupAlgebraSystem R G).ext
intro U
change completedGroupAlgebraProjection R G U
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
(algebraMap R (CompletedGroupAlgebraInClass C hC R G) r)) =
completedGroupAlgebraProjection R G U (algebraMap R (Carrier R G) r)
rw [completedGroupAlgebraFromInClass_projection]
change completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraIndexToInClass G C hForm hG U)
(algebraMap R (CompletedGroupAlgebraInClass C hC R G) r) =
algebraMap R (CompletedGroupAlgebraStage R G U) r
exact completedGroupAlgebraProjectionInClass_algebraMap (R := R) (G := G) C hC
(completedGroupAlgebraIndexToInClass G C hForm hG U) r
@[simp]The algebra homomorphism form of the comparison map is the bundled algebra map determined by the underlying coordinate formula for the completed group algebra.
theorem completedGroupAlgebraFromInClassAlgHom_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraFromInClassAlgHom (R := R) (G := G) C hC hForm hG x =
completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG xThe comparison map from the \(C\)-indexed completed group algebra to the all-finite model is evaluated by reading the corresponding finite-stage coordinate.
Show proof
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 continuous_completedGroupAlgebraFromInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
Continuous (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG)The comparison map from the \(C\)-indexed completed group algebra to the all-finite completed group algebra is continuous for the inverse-limit topology.
Show proof
by
let S := completedGroupAlgebraSystem R G
letI : ∀ U : CompletedGroupAlgebraIndex G, TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
fun U => S.topologicalSpace U
have hval : Continuous fun x : CompletedGroupAlgebraInClass C hC R G =>
fun U : CompletedGroupAlgebraIndex G =>
(show CompletedGroupAlgebraStage R G U from
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x).1 U) := by
apply continuous_pi
intro U
letI : TopologicalSpace
(CompletedGroupAlgebraStageInClass C R G (completedGroupAlgebraIndexToInClass G C hForm hG U)) :=
(completedGroupAlgebraSystemInClass C hC R G).topologicalSpace
(completedGroupAlgebraIndexToInClass G C hForm hG U)
change Continuous (completedGroupAlgebraProjectionInClass C hC R G
(completedGroupAlgebraIndexToInClass G C hForm hG U))
simpa using continuous_completedGroupAlgebraProjectionInClass
(R := R) (G := G) C hC (completedGroupAlgebraIndexToInClass G C hForm hG U)
exact Continuous.subtype_mk hval fun x =>
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x).2
@[simp]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. 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. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraFromInClass_toInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : Carrier R G) :
completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
(completedGroupAlgebraToInClass (R := R) (G := G) C hC x) = xThe composite from a \(C\)-indexed completion to the all-finite completion and back is the identity on the \(C\)-indexed completion.
Show proof
by
apply (completedGroupAlgebraSystem R G).ext
intro U
change completedGroupAlgebraProjection R G U
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
(completedGroupAlgebraToInClass (R := R) (G := G) C hC x)) =
completedGroupAlgebraProjection R G U x
rw [completedGroupAlgebraFromInClass_projection, completedGroupAlgebraToInClass_projection]
change x.1
(completedGroupAlgebraIndexInClassToAllFinite G C hC
(completedGroupAlgebraIndexToInClass G C hForm hG U)) = x.1 U
cases U
rfl
@[simp]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_fromInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraToInClass (R := R) (G := G) C hC
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x) = xShow proof
by
apply (completedGroupAlgebraSystemInClass C hC R G).ext
intro U
change completedGroupAlgebraProjectionInClass C hC R G U
(completedGroupAlgebraToInClass (R := R) (G := G) C hC
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x)) =
completedGroupAlgebraProjectionInClass C hC R G U x
rw [completedGroupAlgebraToInClass_projection]
change completedGroupAlgebraProjection R G
(completedGroupAlgebraIndexInClassToAllFinite G C hC U)
(completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x) =
completedGroupAlgebraProjectionInClass C hC R G U x
rw [completedGroupAlgebraFromInClass_projection]
change x.1
(completedGroupAlgebraIndexToInClass G C hForm hG
(completedGroupAlgebraIndexInClassToAllFinite G C hC U)) = x.1 U
cases U
rfl
@[simp]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 completedGroupAlgebraFromInClassRingHom_comp_toInClassRingHom
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
(completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG).comp
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC) =
RingHom.id (Carrier R G)The two comparison ring homomorphisms are inverse to one another after composition.
Show proof
by
apply RingHom.ext
intro x
exact completedGroupAlgebraFromInClass_toInClass (R := R) (G := G) C hC hForm hG x
@[simp]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. 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 completedGroupAlgebraToInClassRingHom_comp_fromInClassRingHom
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
(completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC).comp
(completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG) =
RingHom.id (CompletedGroupAlgebraInClass C hC R G)The two comparison ring homomorphisms are inverse to one another after composition.
Show proof
by
apply RingHom.ext
intro x
exact completedGroupAlgebraToInClass_fromInClass (R := R) (G := G) C hC hForm hG 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. 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 completedGroupAlgebraInClassRingEquiv
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
Carrier R G ≃+* CompletedGroupAlgebraInClass C hC R G where
toFun := completedGroupAlgebraToInClass (R := R) (G := G) C hC
invFun := completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
left_inv := by
intro x
exact completedGroupAlgebraFromInClass_toInClass (R := R) (G := G) C hC hForm hG x
right_inv := by
intro x
exact completedGroupAlgebraToInClass_fromInClass (R := R) (G := G) C hC hForm hG x
map_mul' := by
intro x y
exact map_mul (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC) x y
map_add' := by
intro x y
exact map_add (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC) x y
@[simp]For a pro-\(C\) group, the all-finite and \(C\)-indexed completed group algebras are the same ring, via the comparison maps.
theorem completedGroupAlgebraInClassRingEquiv_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : Carrier R G) :
completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hC hForm hG x =
completedGroupAlgebraToInClass (R := R) (G := G) C hC xThe comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison map.
Show proof
rfl
@[simp]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. 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 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. 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.
□theorem completedGroupAlgebraInClassRingEquiv_symm_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : CompletedGroupAlgebraInClass C hC R G) :
(completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hC hForm hG).symm x =
completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG xThe comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison map.
Show proof
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. 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 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. 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 completedGroupAlgebraInClassAlgEquiv
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
Carrier R G ≃ₐ[R] CompletedGroupAlgebraInClass C hC R G :=
AlgEquiv.ofRingEquiv (f := completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hC hForm hG)
(by
intro r
rfl)
@[simp]For a pro-\(C\) group, the all-finite and \(C\)-indexed completed group algebras are the same \(R\)-algebra.
theorem completedGroupAlgebraInClassAlgEquiv_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : Carrier R G) :
completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hC hForm hG x =
completedGroupAlgebraToInClass (R := R) (G := G) C hC xThe comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison map.
Show proof
rfl
@[simp]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. 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 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. 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.
□theorem completedGroupAlgebraInClassAlgEquiv_symm_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : CompletedGroupAlgebraInClass C hC R G) :
(completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hC hForm hG).symm x =
completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG xThe comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison map.
Show proof
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. 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 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. 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 completedGroupAlgebraInClassHomeomorph
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
Carrier R G ≃ₜ CompletedGroupAlgebraInClass C hC R G where
toEquiv := (completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hC hForm hG).toEquiv
continuous_toFun := continuous_completedGroupAlgebraToInClass (R := R) (G := G) C hC
continuous_invFun := continuous_completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
@[simp]The comparison equivalence is an equivalence of topological spaces.
theorem completedGroupAlgebraInClassHomeomorph_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : Carrier R G) :
completedGroupAlgebraInClassHomeomorph (R := R) (G := G) C hC hForm hG x =
completedGroupAlgebraToInClass (R := R) (G := G) C hC xThe comparison homeomorphism is evaluated by the underlying all-finite or \(C\)-indexed comparison map.
Show proof
rfl
@[simp]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. 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. 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 completedGroupAlgebraInClassHomeomorph_symm_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : CompletedGroupAlgebraInClass C hC R G) :
(completedGroupAlgebraInClassHomeomorph (R := R) (G := G) C hC hForm hG).symm x =
completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG xThe comparison homeomorphism is evaluated by the underlying all-finite or \(C\)-indexed comparison map.
Show proof
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. 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. 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_surjective
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
Function.Surjective (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC)Surjectivity of the induced map is obtained from surjectivity on the underlying quotient or dense algebraic model, together with closedness of the image in the completed target.
Show proof
by
intro x
refine ⟨completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x, ?_⟩
exact completedGroupAlgebraToInClass_fromInClass (R := R) (G := G) C hC hForm hG 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. 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. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□theorem completedGroupAlgebraFromInClass_surjective
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
Function.Surjective (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG)Surjectivity of the induced map is obtained from surjectivity on the underlying quotient or dense algebraic model, together with closedness of the image in the completed target.
Show proof
by
intro x
refine ⟨completedGroupAlgebraToInClass (R := R) (G := G) C hC x, ?_⟩
exact completedGroupAlgebraFromInClass_toInClass (R := R) (G := G) C hC hForm hG 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. 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. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□