English
Assume R is Noetherian and its residue field is finite. For any ideal I, R/I is finite iff some power of the maximal ideal is contained in I.
Русский
Пусть R — Noetherian кольцо, остаточное поле конечного размера. Тогда R/I есть конечный модуль тогда и только тогда, когда какая-то степень максимального идеала входит в I.
LaTeX
$$$[\\text{IsNoetherianRing } R]\\ [\\text{Finite }(\\mathrm{ResidueField } R)]\\ {I : \\mathrm{Ideal}(R)} :\\ Finite (R / I) \\iff \\exists n, (\\ maximalIdeal R)^n \\le I$$$
Lean4
theorem finite_quotient_iff [IsNoetherianRing R] [Finite (ResidueField R)] {I : Ideal R} :
Finite (R ⧸ I) ↔ ∃ n, (maximalIdeal R) ^ n ≤ I :=
by
refine ⟨fun _ ↦ exists_maximalIdeal_pow_le_of_isArtinianRing_quotient I, ?_⟩
rintro ⟨n, hn⟩
have : Finite (R ⧸ maximalIdeal R) := ‹_›
have := (Ideal.finite_quotient_pow (IsNoetherian.noetherian (maximalIdeal R)) n)
exact Finite.of_surjective _ (Ideal.Quotient.factor_surjective hn)
