CompletedGroupAlgebra.Basic.InClass.Topology
Completed Group Algebra / Basic / Within a Class / Topology.
theorem completedGroupAlgebraStageInClass_isTopologicalRing
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) :
letI : Finite (CompletedGroupAlgebraQuotientInClass G C U)Each \(C\)-indexed finite stage is a topological ring.
Show proof
finite_completedGroupAlgebraQuotientInClass G C hC U
letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
(completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
IsTopologicalRing (CompletedGroupAlgebraStageInClass C R G U) := by
letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
finite_completedGroupAlgebraQuotientInClass G C hC U
letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
(completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
dsimp [completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass]
exact finiteGroupAlgebra_isTopologicalRing R (CompletedGroupAlgebraQuotientInClass G C U)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.
□instance instIsTopologicalRingCompletedGroupAlgebraSystemInClassX
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(U : CompletedGroupAlgebraIndexInClass G C) :
IsTopologicalRing ((completedGroupAlgebraSystemInClass C hC R G).X U) :=
completedGroupAlgebraStageInClass_isTopologicalRing (R := R) (G := G) C hC UThe inverse system of finite-stage group algebras inherits a ring structure from the compatible finite-stage rings.
instance instIsTopologicalRingCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
IsTopologicalRing (CompletedGroupAlgebraInClass C hC R G) := by
change IsTopologicalRing (completedGroupAlgebraSystemInClass C hC R G).inverseLimit
infer_instanceThe \(C\)-indexed completed group algebra inherits a ring structure from the compatible finite-stage rings.
instance instContinuousSMulCompletedGroupAlgebraInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
ContinuousSMul R (CompletedGroupAlgebraInClass C hC R G) where
continuous_smul := by
let A := CompletedGroupAlgebraInClass C hC R G
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 p : R × A =>
fun U : CompletedGroupAlgebraIndexInClass G C =>
(show CompletedGroupAlgebraStageInClass C R G U from (p.1 • p.2).1 U) := by
change Continuous fun p : R × A =>
fun U : CompletedGroupAlgebraIndexInClass G C =>
p.1 • completedGroupAlgebraProjectionInClass C hC R G U p.2
apply continuous_pi
intro U
letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
finite_completedGroupAlgebraQuotientInClass G C hC U
letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
S.topologicalSpace U
letI : ContinuousSMul R (CompletedGroupAlgebraStageInClass C R G U) :=
finiteGroupAlgebra_continuousSMul R (CompletedGroupAlgebraQuotientInClass G C U)
exact continuous_fst.smul ((S.continuous_projection U).comp continuous_snd)
exact Continuous.subtype_mk hval fun p => (p.1 • p.2).2Scalar multiplication is continuous for the relevant inverse-limit topology.
theorem continuous_completedGroupAlgebraAlgebraMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
Continuous (algebraMap R (CompletedGroupAlgebraInClass C hC R G))The coefficient-ring map into the \(C\)-indexed completed group algebra is continuous.
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 r : R =>
fun U : CompletedGroupAlgebraIndexInClass G C =>
(show CompletedGroupAlgebraStageInClass C R G U from
(algebraMap R (CompletedGroupAlgebraInClass C hC R G) r).1 U) := by
change Continuous fun r : R =>
fun U : CompletedGroupAlgebraIndexInClass G C =>
algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r
apply continuous_pi
intro U
letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
finite_completedGroupAlgebraQuotientInClass G C hC U
letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
S.topologicalSpace U
exact finiteGroupAlgebra_algebraMap_continuous R (CompletedGroupAlgebraQuotientInClass G C U)
exact Continuous.subtype_mk hval fun r =>
(algebraMap R (CompletedGroupAlgebraInClass C hC R G) r).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. 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. 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 completedGroupAlgebraStageInClass_isProfiniteRing
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hR : IsProfiniteRing R) (U : CompletedGroupAlgebraIndexInClass G C) :
IsProfiniteRing ((completedGroupAlgebraSystemInClass C hC R G).X U)Each \(C\)-indexed finite stage is a profinite ring when the coefficient ring is profinite.
Show proof
by
letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
finite_completedGroupAlgebraQuotientInClass G C hC U
dsimp [completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass]
exact finiteGroupAlgebra_isProfiniteRing R (CompletedGroupAlgebraQuotientInClass G C U) hRProof. 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. 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 completedGroupAlgebraInClass_compactSpace
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hR : IsProfiniteRing R) :
CompactSpace (CompletedGroupAlgebraInClass C hC R G)The \(C\)-indexed completed group algebra is compact when the coefficient ring is profinite.
Show proof
by
let S := completedGroupAlgebraSystemInClass C hC R G
letI : ∀ U : CompletedGroupAlgebraIndexInClass G C, CompactSpace (S.X U) := fun U =>
(completedGroupAlgebraStageInClass_isProfiniteRing (R := R) (G := G) C hC hR U).2.1
letI : ∀ U : CompletedGroupAlgebraIndexInClass G C, T2Space (S.X U) := fun U =>
(completedGroupAlgebraStageInClass_isProfiniteRing (R := R) (G := G) C hC hR U).2.2.1
change CompactSpace S.inverseLimit
infer_instanceProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. 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 completedGroupAlgebraInClass_t2Space
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hR : IsProfiniteRing R) :
T2Space (CompletedGroupAlgebraInClass C hC R G)The \(C\)-indexed completed group algebra is Hausdorff when the coefficient ring is profinite.
Show proof
by
let S := completedGroupAlgebraSystemInClass C hC R G
letI : ∀ U : CompletedGroupAlgebraIndexInClass G C, T2Space (S.X U) := fun U =>
(completedGroupAlgebraStageInClass_isProfiniteRing (R := R) (G := G) C hC hR U).2.2.1
exact S.t2Space_inverseLimitProof. 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. 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 completedGroupAlgebraInClass_totallyDisconnectedSpace
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hR : IsProfiniteRing R) :
TotallyDisconnectedSpace (CompletedGroupAlgebraInClass C hC R G)The \(C\)-indexed completed group algebra is totally disconnected for profinite coefficients.
Show proof
by
let S := completedGroupAlgebraSystemInClass C hC R G
letI : ∀ U : CompletedGroupAlgebraIndexInClass G C, TotallyDisconnectedSpace (S.X U) :=
fun U =>
(completedGroupAlgebraStageInClass_isProfiniteRing (R := R) (G := G) C hC hR U).2.2.2
exact S.totallyDisconnectedSpace_inverseLimitProof. 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. 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 completedGroupAlgebraInClass_isProfiniteRing
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hR : IsProfiniteRing R) :
IsProfiniteRing (CompletedGroupAlgebraInClass C hC R G)The \(C\)-indexed completed group algebra is profinite when the coefficient ring is profinite.
Show proof
by
letI : IsTopologicalRing (CompletedGroupAlgebraInClass C hC R G) :=
instIsTopologicalRingCompletedGroupAlgebraInClass (R := R) (G := G) C hC
letI : CompactSpace (CompletedGroupAlgebraInClass C hC R G) :=
completedGroupAlgebraInClass_compactSpace (R := R) (G := G) C hC hR
letI : T2Space (CompletedGroupAlgebraInClass C hC R G) :=
completedGroupAlgebraInClass_t2Space (R := R) (G := G) C hC hR
letI : TotallyDisconnectedSpace (CompletedGroupAlgebraInClass C hC R G) :=
completedGroupAlgebraInClass_totallyDisconnectedSpace (R := R) (G := G) C hC hR
exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. 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. 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 completedGroupAlgebraInClass_isProfiniteModule
(C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
(hR : IsProfiniteRing R) :
IsProfiniteModule R (CompletedGroupAlgebraInClass C hC R G)The \(C\)-indexed completed group algebra is a profinite module over its coefficient ring.
Show proof
by
letI : IsTopologicalRing R := hR.1
letI : IsTopologicalRing (CompletedGroupAlgebraInClass C hC R G) :=
instIsTopologicalRingCompletedGroupAlgebraInClass (R := R) (G := G) C hC
letI : IsTopologicalAddGroup (CompletedGroupAlgebraInClass C hC R G) := inferInstance
letI : ContinuousSMul R (CompletedGroupAlgebraInClass C hC R G) :=
instContinuousSMulCompletedGroupAlgebraInClass (R := R) (G := G) C hC
letI : CompactSpace (CompletedGroupAlgebraInClass C hC R G) :=
completedGroupAlgebraInClass_compactSpace (R := R) (G := G) C hC hR
letI : T2Space (CompletedGroupAlgebraInClass C hC R G) :=
completedGroupAlgebraInClass_t2Space (R := R) (G := G) C hC hR
letI : TotallyDisconnectedSpace (CompletedGroupAlgebraInClass C hC R G) :=
completedGroupAlgebraInClass_totallyDisconnectedSpace (R := R) (G := G) C hC hR
exact ⟨hR, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance⟩Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. 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. 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.
□