English
Under Noetherian hypothesis, multiplying a spanSingleton by the inverse of an image preserves Noetherianity.
Русский
При предположении о Неттере, умножение на обратную часть образа сохраняет Неотерминирование.
LaTeX
$$IsNoetherian R₁ x → IsNoetherian R₁ (spanSingleton R₁⁰ (algebraMap R₁ K x)⁻¹ * I)$$
Lean4
theorem isNoetherian_spanSingleton_inv_to_map_mul (x : R₁) {I : FractionalIdeal R₁⁰ K} (hI : IsNoetherian R₁ I) :
IsNoetherian R₁ (spanSingleton R₁⁰ (algebraMap R₁ K x)⁻¹ * I : FractionalIdeal R₁⁰ K) := by
classical
by_cases hx : x = 0
· rw [hx, RingHom.map_zero, inv_zero, spanSingleton_zero, zero_mul]
exact isNoetherian_zero
have h_gx : algebraMap R₁ K x ≠ 0 :=
mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).mp (IsFractionRing.injective _ _) x) hx
have h_spanx : spanSingleton R₁⁰ (algebraMap R₁ K x) ≠ 0 := spanSingleton_ne_zero_iff.mpr h_gx
rw [isNoetherian_iff] at hI ⊢
intro J hJ
rw [← div_spanSingleton, le_div_iff_mul_le h_spanx] at hJ
obtain ⟨s, hs⟩ := hI _ hJ
use s * {(algebraMap R₁ K x)⁻¹}
rw [Finset.coe_mul, Finset.coe_singleton, ← span_mul_span, hs, ← coe_spanSingleton R₁⁰, ← coe_mul, mul_assoc,
spanSingleton_mul_spanSingleton, mul_inv_cancel₀ h_gx, spanSingleton_one, mul_one]
