English
Let I be an ideal of a local ring R; if R/I is Artinian, then there exists n with maximalIdeal(R)^n ≤ I.
Русский
Пусть I — идеал локального кольца R; если R/I артинен, то существует натуральное n такое, что (макс. идеал R)^n ≤ I.
LaTeX
$$$\\text{If } [\\text{IsArtinianRing } (R/ I)], \\exists n : \\mathbb N, (\\ maximalIdeal R)^n \\le I$$$
Lean4
theorem exists_maximalIdeal_pow_le_of_isArtinianRing_quotient (I : Ideal R) [IsArtinianRing (R ⧸ I)] :
∃ n, maximalIdeal R ^ n ≤ I := by
by_cases hI : I = ⊤
· simp [hI]
have : Nontrivial (R ⧸ I) := Ideal.Quotient.nontrivial hI
have := IsLocalRing.of_surjective' (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective
have := IsLocalHom.of_surjective (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective
obtain ⟨n, hn⟩ := IsArtinianRing.isNilpotent_jacobson_bot (R := R ⧸ I)
have : (maximalIdeal R).map (Ideal.Quotient.mk I) = maximalIdeal (R ⧸ I) :=
by
ext x
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
simp [sup_eq_left.mpr (le_maximalIdeal hI)]
rw [jacobson_eq_maximalIdeal _ bot_ne_top, ← this, ← Ideal.map_pow, Ideal.zero_eq_bot, Ideal.map_eq_bot_iff_le_ker,
Ideal.mk_ker] at hn
exact ⟨n, hn⟩
