Maximal ideals over an ideal with semilocal quotient

The maximal ideals of a commutative ring R containing an ideal 𝔞 are the pullbacks of the maximal ideals of R ⧸ 𝔞. So if the quotient R ⧸ 𝔞 is semilocal (has only finitely many maximal ideals), then 𝔞 lies in only finitely many maximal ideals of R. This applies for instance when R ⧸ 𝔞 is Artinian (IsArtinianRing.setOfPred_isMaximal_finite), in particular when it is finite.

Main results

• Ideal.finite_setOfPred_isMaximal_and_le: an ideal with semilocal quotient ring lies in only finitely many maximal ideals.

theorem Ideal.finite_setOfPred_isMaximal_and_le {R : Type u_1} [CommRing R] (𝔞 : Ideal R) [Finite (MaximalSpectrum (R ⧸ 𝔞))] : {P : Ideal R | P.IsMaximal ∧ 𝔞 ≤ P}.Finite

An ideal with semilocal quotient ring, for instance with Artinian or finite quotient ring, lies in only finitely many maximal ideals.