Rings with finite quotients

A commutative ring is said to have finite quotients if, for any nonzero ideal I of R, the quotient R ⧸ I is finite.

Main results

• Ring.HasFiniteQuotients.instDimensionLEOne: A ring with finite quotients has dimension ≤ 1.
• Ring.HasFiniteQuotients.instIsNoetherianRing : A ring with finite quotients is noetherian.
• Ring.HasFiniteQuotients.of_module_finite: Assume that R has finite quotients and that S is a domain and a finite R-module. Then S has finite quotients.
• Ring.HasFiniteQuotients.instOfIsDomainOfFG: A domain that is also a finite ℤ-module has finite quotients.

class Ring.HasFiniteQuotients (R : Type u_1) [CommRing R] : Prop

A ring R has finite quotients if the quotient R ⧸ I is finite for all nonzero ideals of R.

• finiteQuotient {I : Ideal R} : I ≠ ⊥ → Finite (R ⧸ I)

instance Ring.HasFiniteQuotients.instOfFinite {R : Type u_1} [CommRing R] [Finite R] : HasFiniteQuotients R

A finite ring has finite quotients.

theorem Ring.HasFiniteQuotients.maximalOfPrime {R : Type u_1} [CommRing R] [HasFiniteQuotients R] {P : Ideal R} [P.IsPrime] (hp : P ≠ ⊥) : P.IsMaximal

A nonzero prime ideal of a ring with finite quotients is maximal.

instance Ring.HasFiniteQuotients.instDimensionLEOne {R : Type u_1} [CommRing R] [HasFiniteQuotients R] : DimensionLEOne R

A ring with finite quotients has dimension ≤ 1.

instance Ring.HasFiniteQuotients.instIsNoetherianRing {R : Type u_1} [CommRing R] [HasFiniteQuotients R] : IsNoetherianRing R

A ring with finite quotients is noetherian.

theorem Ring.HasFiniteQuotients.cardQuot_pos {R : Type u_1} [CommRing R] [HasFiniteQuotients R] (I : Ideal R) (hI : I ≠ ⊥) : 0 < Submodule.cardQuot I

theorem Ring.HasFiniteQuotients.finite_setOf_mem {R : Type u_1} [CommRing R] [HasFiniteQuotients R] (x : R) (hx : x ≠ 0) : {I : Ideal R | x ∈ I}.Finite

theorem Ring.HasFiniteQuotients.finite_cardQuot_le {R : Type u_1} [CommRing R] [HasFiniteQuotients R] (B : ℕ) : {I : Ideal R | Submodule.cardQuot I ≤ B}.Finite

For every bound B, a ring with finite quotients has only finitely many ideals of norm bounded by B.

theorem Ring.HasFiniteQuotients.finite_absNorm_le {R : Type u_1} [CommRing R] [HasFiniteQuotients R] [IsDedekindDomain R] [Module.Free ℤ R] (B : ℕ) : {I : Ideal R | Ideal.absNorm I ≤ B}.Finite

A ring with finite quotients has only finitely many ideals of bounded norm.

theorem Ring.HasFiniteQuotients.finite_cardQuot_heightOneSpectrum_le {R : Type u_1} [CommRing R] [HasFiniteQuotients R] (B : ℕ) : {p : IsDedekindDomain.HeightOneSpectrum R | Submodule.cardQuot p.asIdeal ≤ B}.Finite

A ring with finite quotients has only finitely many nonzero prime ideals of bounded norm.

theorem Ring.HasFiniteQuotients.finite_absNorm_heightOneSpectrum_le {R : Type u_1} [CommRing R] [HasFiniteQuotients R] [IsDedekindDomain R] [Module.Free ℤ R] (B : ℕ) : {p : IsDedekindDomain.HeightOneSpectrum R | Ideal.absNorm p.asIdeal ≤ B}.Finite

A ring with finite quotients has only finitely many nonzero prime ideals of bounded norm.

theorem Ring.HasFiniteQuotients.of_module_finite (R : Type u_1) [CommRing R] [HasFiniteQuotients R] (S : Type u_2) [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S] : HasFiniteQuotients S

Assume that R has finite quotients and that S is a domain and a finite R-module. Then S has finite quotients.

instance Ring.HasFiniteQuotients.instInt : HasFiniteQuotients ℤ

The ring ℤ has finite quotients.

instance Ring.HasFiniteQuotients.instOfIsDomainOfFG {R : Type u_1} [CommRing R] [IsDomain R] [AddGroup.FG R] : HasFiniteQuotients R

A domain that is finitely generated has finite quotients.