English
If every prime ideal in a ring is finitely generated, then every ideal is finitely generated; i.e., the ring is Noetherian.
Русский
Если каждый простейший идеал в кольце конечножгенерирован, то и каждый идеал конечножгенерирован; то есть кольцо Нётерово.
LaTeX
$$$\\forall R\\,[IsNoetherianRing R] \\Rightarrow \\text{If } \\forall I:I.IsPrime \\Rightarrow I.FG, \\text{ then } IsNoetherianRing R$$$
Lean4
/-- If all prime ideals in a commutative ring are finitely generated, so are all other ideals. -/
theorem of_prime (H : ∀ I : Ideal R, I.IsPrime → I.FG) : IsNoetherianRing R :=
by
refine ⟨isOka_fg.forall_of_forall_prime' (fun C hC₁ hC₂ I hI h ↦ ⟨sSup C, ?_, h⟩) H⟩
obtain ⟨G, hG⟩ := h
obtain ⟨J, J_mem_C, G_subset_J⟩ : ∃ J ∈ C, G.toSet ⊆ J :=
by
refine hC₂.directedOn.exists_mem_subset_of_finset_subset_biUnion ⟨I, hI⟩ (fun _ hx ↦ ?_)
simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop]
exact (Submodule.mem_sSup_of_directed ⟨I, hI⟩ hC₂.directedOn).1 <| hG ▸ subset_span hx
suffices J_eq_sSup : J = sSup C from J_eq_sSup ▸ J_mem_C
exact le_antisymm (le_sSup J_mem_C) (hG ▸ Ideal.span_le.2 G_subset_J)
