exists_pow_le_of_le_radical_of_fg

English

If I ≤ J.radical and I.FG, then there exists n with I^n ≤ J.

Русский

Если I ≤ J.radical и I FG, тогда существует n с I^n ≤ J.

LaTeX

$$I ≤ J.radical ∧ I.FG ⇒ ∃ n, I^n ≤ J$$

Lean4

theorem exists_pow_le_of_le_radical_of_fg {R : Type*} [CommSemiring R] {I J : Ideal R} (h' : I ≤ J.radical) (h : I.FG) :
    ∃ n : ℕ, I ^ n ≤ J := by
  revert h'
  apply Submodule.fg_induction _ _ _ _ _ I h
  · intro x hJ
    simp only [Ideal.submodule_span_eq, Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe] at hJ
    obtain ⟨n, hn⟩ := hJ
    refine ⟨n, by simpa [Ideal.span_singleton_pow, Ideal.span_le]⟩
  · intro I₁ I₂ h₁ h₂ hJ
    obtain ⟨n₁, hn₁⟩ := h₁ (le_sup_left.trans hJ)
    obtain ⟨n₂, hn₂⟩ := h₂ (le_sup_right.trans hJ)
    use n₁ + n₂
    exact Ideal.sup_pow_add_le_pow_sup_pow.trans (sup_le hn₁ hn₂)

Похожие утверждения