English
In a Dedekind domain with fraction field K, given fractional ideals a, b, c with a ≤ c and a ≠ 0, b ≠ 0, there exists x ∈ K such that a + spanSingleton(x) · b = c.
Русский
В области Дедеконда с полем дробей K, пусть a, b, c — дробные идеалы, причем a ≤ c, a ≠ 0, b ≠ 0. Тогда существует x ∈ K такое, что a + spanSingleton(x) · b = c.
LaTeX
$$$\\exists x \\in K,\\ a + \\operatorname{spanSingleton}(x) \\cdot b = c$$$
Lean4
theorem exists_add_spanSingleton_mul_eq {a b c : FractionalIdeal R⁰ K} (hac : a ≤ c) (ha : a ≠ 0) (hb : b ≠ 0) :
∃ x : K, a + FractionalIdeal.spanSingleton R⁰ x * b = c :=
by
wlog hb' : b = 1
· obtain ⟨x, e⟩ :=
this (a := b⁻¹ * a) (b := 1) (c := b⁻¹ * c) (mul_le_mul_left' hac _) (by simp [ha, hb]) one_ne_zero rfl
use x
simpa [hb, ← mul_assoc, mul_add, mul_comm b (.spanSingleton _ _)] using congr(b * $e)
subst hb'
have H : Ideal.span { c.den.1 } * a.num ≤ c.num * Ideal.span { a.den.1 } :=
by
rw [← FractionalIdeal.coeIdeal_le_coeIdeal K]
simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton,
← FractionalIdeal.den_mul_self_eq_num']
ring_nf
exact mul_le_mul_left' hac _
obtain ⟨x, hx⟩ := exists_sup_span_eq H (by simpa using FractionalIdeal.num_eq_zero_iff.not.mpr ha)
refine ⟨algebraMap R K x / algebraMap R K (a.den.1 * c.den.1), ?_⟩
refine mul_left_injective₀ (b := .spanSingleton _ (algebraMap R K (a.den.1 * c.den.1))) ?_ ?_
· simp [FractionalIdeal.spanSingleton_eq_zero_iff]
· simp only [map_mul, mul_one, add_mul, FractionalIdeal.spanSingleton_mul_spanSingleton, isUnit_iff_ne_zero, ne_eq,
mul_eq_zero, FaithfulSMul.algebraMap_eq_zero_iff, nonZeroDivisors.coe_ne_zero, or_self, not_false_eq_true,
IsUnit.div_mul_cancel]
rw [← FractionalIdeal.spanSingleton_mul_spanSingleton, ← mul_assoc, mul_comm a,
FractionalIdeal.den_mul_self_eq_num', ← mul_assoc, mul_right_comm, mul_comm c,
FractionalIdeal.den_mul_self_eq_num', mul_comm]
simp_rw [← FractionalIdeal.coeIdeal_span_singleton, ← FractionalIdeal.coeIdeal_mul, ← hx, ←
FractionalIdeal.coeIdeal_sup]
