CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.Topology
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
theorem completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K)Each two-parameter finite quotient stage is a topological ring for its discrete topology.
Show proof
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
IsTopologicalRing (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) := by
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
haveI : DiscreteTopology (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K
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. 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 completedGroupAlgebraOpenFiniteQuotientStage_isProfiniteRing
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G] (hR : IsProfiniteRing R)
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K)If \(R\) is profinite, each two-parameter quotient stage is a finite discrete ring, hence profinite.
Show proof
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
IsProfiniteRing (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) := by
classical
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
haveI : DiscreteTopology (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K
let I : Ideal R := (OrderDual.ofDual K.1).1
have hIopen : IsOpen (I : Set R) := (OrderDual.ofDual K.1).2
rcases finite_quotient_of_openIdeal R hR I hIopen with ⟨hIfin⟩
letI : Fintype (R ⧸ I) := hIfin
letI : Fintype (CompletedGroupAlgebraQuotient G K.2) :=
Fintype.ofFinite (CompletedGroupAlgebraQuotient G K.2)
letI : Fintype (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
Fintype.ofEquiv (CompletedGroupAlgebraQuotient G K.2 → R ⧸ I)
Finsupp.equivFunOnFinite.symm
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, 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 completedGroupAlgebraOpenFiniteQuotientStage_fintype
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G] (hR : IsProfiniteRing R)
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
Nonempty (Fintype (CompletedGroupAlgebraOpenFiniteQuotientStage R G K))Show proof
by
classical
let I : Ideal R := (OrderDual.ofDual K.1).1
have hIopen : IsOpen (I : Set R) := (OrderDual.ofDual K.1).2
rcases finite_quotient_of_openIdeal R hR I hIopen with ⟨hIfin⟩
letI : Fintype (R ⧸ I) := hIfin
letI : Fintype (CompletedGroupAlgebraQuotient G K.2) :=
Fintype.ofFinite (CompletedGroupAlgebraQuotient G K.2)
exact ⟨Fintype.ofEquiv
(CompletedGroupAlgebraQuotient G K.2 → R ⧸ I)
Finsupp.equivFunOnFinite.symm⟩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. 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.
□instance instContinuousAddCompletedGroupAlgebraOpenFiniteQuotientLimit :
ContinuousAdd (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
continuous_add := by
let A := CompletedGroupAlgebraOpenFiniteQuotientLimit R G
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
fun K => (completedGroupAlgebraOpenFiniteQuotientSystem R G).topologicalSpace K
have hval : Continuous fun p : A × A =>
((p.1 + p.2 : A) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
change Continuous fun p : A × A =>
fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K p.1 +
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K p.2
apply continuous_pi
intro K
letI : IsTopologicalRing ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing (R := R) (G := G) K
exact (((completedGroupAlgebraOpenFiniteQuotientSystem R G).continuous_projection K).comp
continuous_fst).add
(((completedGroupAlgebraOpenFiniteQuotientSystem R G).continuous_projection K).comp
continuous_snd)
exact Continuous.subtype_mk hval fun p => (p.1 + p.2).2Addition on the open-finite completed group algebra is continuous for the inverse-limit topology.
instance instContinuousNegCompletedGroupAlgebraOpenFiniteQuotientLimit :
ContinuousNeg (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
continuous_neg := by
let A := CompletedGroupAlgebraOpenFiniteQuotientLimit R G
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
fun K => (completedGroupAlgebraOpenFiniteQuotientSystem R G).topologicalSpace K
have hval : Continuous fun x : A =>
((-x : A) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
change Continuous fun x : A =>
fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
-completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K x
apply continuous_pi
intro K
letI : IsTopologicalRing ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing (R := R) (G := G) K
exact ((completedGroupAlgebraOpenFiniteQuotientSystem R G).continuous_projection K).neg
exact Continuous.subtype_mk hval fun x => (-x).2Negation on the completed group algebra is continuous for the inverse-limit topology.
instance instContinuousMulCompletedGroupAlgebraOpenFiniteQuotientLimit :
ContinuousMul (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
continuous_mul := by
let A := CompletedGroupAlgebraOpenFiniteQuotientLimit R G
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
fun K => (completedGroupAlgebraOpenFiniteQuotientSystem R G).topologicalSpace K
have hval : Continuous fun p : A × A =>
((p.1 * p.2 : A) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
change Continuous fun p : A × A =>
fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K p.1 *
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K p.2
apply continuous_pi
intro K
letI : IsTopologicalRing ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing (R := R) (G := G) K
exact (((completedGroupAlgebraOpenFiniteQuotientSystem R G).continuous_projection K).comp
continuous_fst).mul
(((completedGroupAlgebraOpenFiniteQuotientSystem R G).continuous_projection K).comp
continuous_snd)
exact Continuous.subtype_mk hval fun p => (p.1 * p.2).2Multiplication on the completed group algebra is continuous for the inverse-limit topology.
instance instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientLimit :
IsTopologicalRing (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by
letI : ContinuousAdd (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
instContinuousAddCompletedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G)
letI : ContinuousMul (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
instContinuousMulCompletedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G)
letI : ContinuousNeg (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
instContinuousNegCompletedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G)
letI : IsTopologicalSemiring (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
IsTopologicalSemiring.mk
exact IsTopologicalRing.mkThe open-finite quotient limit is a topological ring.
theorem completedGroupAlgebraOpenFiniteQuotientLimit_compactSpace
(hR : IsProfiniteRing R) :
CompactSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G)The open-finite quotient limit is compact when the coefficient ring is profinite.
Show proof
by
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
CompactSpace ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := fun K =>
(completedGroupAlgebraOpenFiniteQuotientStage_isProfiniteRing (R := R) (G := G) hR K).2.1
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
T2Space ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := fun K =>
(completedGroupAlgebraOpenFiniteQuotientStage_isProfiniteRing (R := R) (G := G) hR K).2.2.1
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 completedGroupAlgebraOpenFiniteQuotientLimit_t2Space
(hR : IsProfiniteRing R) :
T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G)The open-finite quotient limit is Hausdorff when the coefficient ring is profinite.
Show proof
by
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
T2Space ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := fun K =>
(completedGroupAlgebraOpenFiniteQuotientStage_isProfiniteRing (R := R) (G := G) hR K).2.2.1
exact (completedGroupAlgebraOpenFiniteQuotientSystem R G).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, 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 completedGroupAlgebraOpenFiniteQuotientLimit_totallyDisconnectedSpace
(hR : IsProfiniteRing R) :
TotallyDisconnectedSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G)The open-finite quotient limit is totally disconnected when the coefficient ring is profinite.
Show proof
by
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
TotallyDisconnectedSpace ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := fun K =>
(completedGroupAlgebraOpenFiniteQuotientStage_isProfiniteRing (R := R) (G := G) hR K).2.2.2
exact (completedGroupAlgebraOpenFiniteQuotientSystem R G).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, 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 completedGroupAlgebraOpenFiniteQuotientLimit_isProfiniteRing
(hR : IsProfiniteRing R) :
IsProfiniteRing (CompletedGroupAlgebraOpenFiniteQuotientLimit R G)The two-parameter kernel-neighborhood limit is a profinite ring.
Show proof
by
letI : CompactSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
completedGroupAlgebraOpenFiniteQuotientLimit_compactSpace (R := R) (G := G) hR
letI : T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
completedGroupAlgebraOpenFiniteQuotientLimit_t2Space (R := R) (G := G) hR
letI : TotallyDisconnectedSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
completedGroupAlgebraOpenFiniteQuotientLimit_totallyDisconnectedSpace (R := R) (G := G) 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, 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. 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. 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. 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.
□