CompletedGroupAlgebra.Basic.InClass.Projection
Completed Group Algebra / Basic / Within a Class / Projection.
abbrev completedGroupAlgebraProjectionInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(U : CompletedGroupAlgebraIndexInClass G C) :
CompletedGroupAlgebraInClass C hC R G → CompletedGroupAlgebraStageInClass C R G U :=
(completedGroupAlgebraSystemInClass C hC R G).projection UThe projection from a \(C\)-indexed completed group algebra to a finite stage.
theorem completedGroupAlgebraProjectionInClass_algebraMap
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) (r : R) :
completedGroupAlgebraProjectionInClass C hC R G U
(completedGroupAlgebraAlgebraMapInClass (R := R) (G := G) C hC r) =
algebraMap R (CompletedGroupAlgebraStageInClass C R G U) rProjection of a coefficient element to a finite stage is the stage algebra 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. 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. 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. 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.
□theorem completedGroupAlgebraProjectionInClass_coeffMap
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
(f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C)
(x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraProjectionInClass C hC S G U
(completedGroupAlgebraCoeffMapInClass (R := R) (G := G) C hC S f x) =
completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U
(completedGroupAlgebraProjectionInClass C hC R G U x)Projection of a coefficient-changed element is coefficient change of the 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. 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. 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 completedGroupAlgebraProjectionRingHomInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(U : CompletedGroupAlgebraIndexInClass G C) :
CompletedGroupAlgebraInClass C hC R G →+* CompletedGroupAlgebraStageInClass C R G U :=
projectionRingHom (S := completedGroupAlgebraSystemInClass C hC R G) UThe projection from a \(C\)-indexed completed group algebra to a finite stage is bundled as a ring homomorphism.
theorem completedGroupAlgebraProjectionRingHomInClass_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraProjectionRingHomInClass C hC R G U x =
completedGroupAlgebraProjectionInClass C hC R G U xThe ring-homomorphism projection from the \(C\)-indexed completed group algebra agrees pointwise with the finite-stage 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 completedGroupAlgebraProjectionAlgHomInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(U : CompletedGroupAlgebraIndexInClass G C) :
CompletedGroupAlgebraInClass C hC R G →ₐ[R] CompletedGroupAlgebraStageInClass C R G U where
toRingHom := completedGroupAlgebraProjectionRingHomInClass C hC R G U
commutes' := by
intro r
rflThe projection from a \(C\)-indexed completed group algebra to a finite stage is bundled as an algebra homomorphism.
theorem completedGroupAlgebraProjectionAlgHomInClass_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraProjectionAlgHomInClass C hC R G U x =
completedGroupAlgebraProjectionInClass C hC R G U xThe algebra-homomorphism projection from the \(C\)-indexed completed group algebra agrees pointwise with the finite-stage 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 completedGroupAlgebraProjectionLinearMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(U : CompletedGroupAlgebraIndexInClass G C) :
CompletedGroupAlgebraInClass C hC R G →ₗ[R] CompletedGroupAlgebraStageInClass C R G U where
toFun := completedGroupAlgebraProjectionInClass C hC R G U
map_add' := by
intro x y
rfl
map_smul' := by
intro r x
rflThe projection from a \(C\)-indexed completed group algebra to a finite stage is bundled as an \(R\)-linear map.
theorem completedGroupAlgebraProjectionLinearMapInClass_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraProjectionLinearMapInClass C hC R G U x =
completedGroupAlgebraProjectionInClass C hC R G U xThe linear projection from the \(C\)-indexed completed group algebra agrees pointwise with the finite-stage 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.
□theorem completedGroupAlgebraProjectionInClass_compatible
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
(x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraTransitionInClass C R G hUV
(completedGroupAlgebraProjectionInClass C hC R G V x) =
completedGroupAlgebraProjectionInClass C hC R G U xThe finite-stage projections are compatible with the \(C\)-indexed transition maps.
Show proof
x.2 U V 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, 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.
□theorem completedGroupAlgebraTransitionInClass_comp_projectionRingHom
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
(completedGroupAlgebraTransitionInClass C R G hUV).comp
(completedGroupAlgebraProjectionRingHomInClass C hC R G V) =
completedGroupAlgebraProjectionRingHomInClass C hC R G UComposing a stage projection with a transition map gives the coarser stage projection.
Show proof
by
apply RingHom.ext
intro x
exact completedGroupAlgebraProjectionInClass_compatible (R := R) (G := G) C hC hUV 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. 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.
□theorem continuous_completedGroupAlgebraProjectionInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) :
letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U)Continuity of the projection from the \(C\)-indexed completed group algebra to a stage.
Show proof
(completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
Continuous (completedGroupAlgebraProjectionInClass C hC R G U) := by
letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
(completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
exact (completedGroupAlgebraSystemInClass C hC R G).continuous_projection UProof. 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 completedGroupAlgebraProjectionContinuousLinearMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(U : CompletedGroupAlgebraIndexInClass G C) :
letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
(completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
CompletedGroupAlgebraInClass C hC R G →L[R] CompletedGroupAlgebraStageInClass C R G U := by
letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
(completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
exact
{ toLinearMap := completedGroupAlgebraProjectionLinearMapInClass C hC R G U
cont := (completedGroupAlgebraSystemInClass C hC R G).continuous_projection U }The projection from a \(C\)-indexed completed group algebra to a finite stage is bundled as a continuous \(R\)-linear map.
theorem completedGroupAlgebraProjectionContinuousLinearMapInClass_apply
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraInClass C hC R G) :
completedGroupAlgebraProjectionContinuousLinearMapInClass C hC R G U x =
completedGroupAlgebraProjectionInClass C hC R G U xThe continuous linear projection has the same underlying coordinate map as the finite-stage 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. 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.
□