English
If I is a finitely generated radical ideal, there exists n such that radical(I)^n ≤ I.
Русский
Если радикал идеала I конечно порождается, существует число n так, что радикал(I)^n ≤ I.
LaTeX
$$∃ n, I.radical^n ≤ I$$
Lean4
theorem exists_radical_pow_le_of_fg {R : Type*} [CommSemiring R] (I : Ideal R) (h : I.radical.FG) :
∃ n : ℕ, I.radical ^ n ≤ I := by
have := le_refl I.radical; revert this
refine Submodule.fg_induction _ _ (fun J => J ≤ I.radical → ∃ n : ℕ, J ^ n ≤ I) ?_ ?_ _ h
· intro x hx
obtain ⟨n, hn⟩ := hx (subset_span (Set.mem_singleton x))
exact ⟨n, by rwa [← Ideal.span, span_singleton_pow, span_le, Set.singleton_subset_iff]⟩
· intro J K hJ hK hJK
obtain ⟨n, hn⟩ := hJ fun x hx => hJK <| Ideal.mem_sup_left hx
obtain ⟨m, hm⟩ := hK fun x hx => hJK <| Ideal.mem_sup_right hx
use n + m
rw [← Ideal.add_eq_sup, add_pow, Ideal.sum_eq_sup, Finset.sup_le_iff]
refine fun i _ => Ideal.mul_le_right.trans ?_
obtain h | h := le_or_gt n i
· apply Ideal.mul_le_right.trans ((Ideal.pow_le_pow_right h).trans hn)
· apply Ideal.mul_le_left.trans
refine (Ideal.pow_le_pow_right ?_).trans hm
rw [add_comm, Nat.add_sub_assoc h.le]
apply Nat.le_add_right
