This file develops open-ideal bases at zero in profinite rings, proves their quotients finite, and derives the finite-open-ideal quotient basis and linear-topology properties.
Open ideals form a neighborhood basis at zero.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
universe u v w zdef HasOpenIdealBasisAtZero (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : PropOpen ideals with finite quotient form a neighborhood basis at zero.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
universe u v w zdef HasFiniteOpenIdealQuotientBasis (Λ : Type u) [Ring Λ] [TopologicalSpace Λ] : PropAn open ideal of a compact topological ring has finite additive quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
universe u v w ztheorem finite_quotient_of_openIdeal
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsTopologicalRing Λ]
[CompactSpace Λ]
(I : Ideal Λ) (hI : IsOpen (I : Set Λ)) :
Nonempty (Fintype (Λ ⧸ I))Proposition 5.1.2(d/e), linear-topology interface: a profinite ring whose topology is linear has a fundamental system of open ideals with finite quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
universe u v w ztheorem profiniteRing_hasFiniteOpenIdealQuotientBasis_of_linearTopology
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsLinearTopology Λ Λ]
[IsTopologicalRing Λ] [CompactSpace Λ] :
HasFiniteOpenIdealQuotientBasis ΛProposition 5.1.2(d/e), linear-topology part for profinite rings.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
universe u v w ztheorem profiniteRing_isLinearTopology
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsTopologicalRing Λ]
[CompactSpace Λ] [T2Space Λ] [TotallyDisconnectedSpace Λ] :
IsLinearTopology Λ ΛProposition 5.1.2(d/e): a profinite ring has a fundamental system of open ideals with finite quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
universe u v w ztheorem profiniteRing_hasFiniteOpenIdealQuotientBasis
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsTopologicalRing Λ]
[CompactSpace Λ] [T2Space Λ] [TotallyDisconnectedSpace Λ] :
HasFiniteOpenIdealQuotientBasis ΛProposition 5.1.2(d): a profinite ring has a basis of open ideals at zero.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
universe u v w ztheorem profiniteRing_hasOpenIdealBasisAtZero
(Λ : Type u) [Ring Λ] [TopologicalSpace Λ] [IsTopologicalRing Λ]
[CompactSpace Λ] [T2Space Λ] [TotallyDisconnectedSpace Λ] :
HasOpenIdealBasisAtZero Λ