Documentation

Mathlib.Topology.Algebra.Ring.Compact

Compact Hausdorff Rings #

Main results #

IsArtinianRing.finite_of_compactSpace_of_t2Space: Compact Hausdorff Artinian rings are finite (and thus discrete).
Ideal.isOpen_of_isMaximal: Maximal ideals are open in compact Hausdorff Noetherian rings.
IsLocalRing.isOpen_iff_finite_quotient: An ideal in a compact Hausdorff Noetherian local ring is open iff it has finite index.
IsDedekindDomain.isOpen_iff: An ideal in a compact Hausdorff Dedekind domain (that is not a field) is open iff it is non-zero.

Future projects #

Show that compact Hausdorff rings are totally disconnected and linearly topologized. See https://ncatlab.org/nlab/show/compact+Hausdorff+rings+are+profinite

theorem IsArtinianRing.finite_of_compactSpace_of_t2Space {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsArtinianRing R] :

Compact Hausdorff Artinian (commutative) rings are finite. This is not an instance, as it would apply to every Finite goal, causing slowly failing typeclass search in some cases.

theorem Ideal.isOpen_of_isMaximal {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsNoetherianRing R] (I : Ideal R) [I.IsMaximal] :

theorem Ideal.isOpen_pow_of_isMaximal {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsNoetherianRing R] (I : Ideal R) [I.IsMaximal] (n : ℕ) :

IsOpen ↑(I ^ n)

@[instance 100]

instance instFiniteQuotientIdealOfIsMaximal {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsNoetherianRing R] (I : Ideal R) [I.IsMaximal] :

Finite (R ⧸ I)

theorem IsLocalRing.isOpen_maximalIdeal_pow (R : Type u_1) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsLocalRing R] [IsNoetherianRing R] (n : ℕ) :

IsOpen ↑(maximalIdeal R ^ n)

theorem IsLocalRing.isOpen_maximalIdeal (R : Type u_1) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsLocalRing R] [IsNoetherianRing R] :

IsOpen ↑(maximalIdeal R)

instance IsLocalRing.finite_residueField_of_compactSpace {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsLocalRing R] [IsNoetherianRing R] :

Finite (ResidueField R)

theorem IsLocalRing.isOpen_iff_finite_quotient {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsLocalRing R] [IsNoetherianRing R] {I : Ideal R} :

IsOpen ↑I ↔ Finite (R ⧸ I)

theorem IsDedekindDomain.isOpen_of_ne_bot {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ ⊥) :

theorem IsDedekindDomain.isOpen_iff {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsDedekindDomain R] (hR : ¬IsField R) {I : Ideal R} :

IsOpen ↑I ↔ I ≠ ⊥

theorem IsDiscreteValuationRing.isOpen_iff {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsDomain R] [IsDiscreteValuationRing R] {I : Ideal R} :

IsOpen ↑I ↔ I ≠ ⊥