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.

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.

instance Ring.HasFiniteQuotients.instFiniteQuotientIdealOfNeZero {R : Type u_1} [CommRing R] [HasFiniteQuotients R] {I : Ideal R} [NeZero I] : Finite (R ⧸ I)

A quotient of a ring with finite quotients by a nonzero ideal is finite.

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.

instance Ring.HasFiniteQuotients.instPerfectFieldResidueFieldOfFractionRing {R : Type u_1} [CommRing R] [HasFiniteQuotients R] [IsDomain R] [PerfectField (FractionRing R)] (P : Ideal R) [P.IsPrime] : PerfectField P.ResidueField

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.

theorem Ideal.finiteIndex' {S : Type u_1} [CommRing S] [Ring.HasFiniteQuotients S] {I : Ideal S} (hI : I ≠ ⊥) : (Submodule.toAddSubgroup I).FiniteIndex

A version of finiteIndex for a ring with finite quotients.

theorem Ideal.isFiniteRelIndex' {S : Type u_1} [CommRing S] [Ring.HasFiniteQuotients S] {I : Ideal S} (hI : I ≠ ⊥) (J : Ideal S) : (Submodule.toAddSubgroup I).IsFiniteRelIndex (Submodule.toAddSubgroup J)

A version of isFiniteRelIndex for a ring with finite quotients.