English
In a Dedekind domain, for any 0 < I ≤ J there exists a ∈ R such that J = I ⊔ (a).
Русский
В домене Дедекдина для любых 0 < I ≤ J существует элемент a ∈ R такой, что J = I + (a).
LaTeX
$$$\forall I,J\; (0 < I \le J) \;\exists a:\ R,\; I \oplus \langle a \rangle = J.$$$
Lean4
/-- In a Dedekind domain, for every ideals `0 < I ≤ J` there exists `a` such that `J = I + ⟨a⟩`.
TODO: Show that this property uniquely characterizes Dedekind domains. -/
theorem exists_sup_span_eq {I J : Ideal R} (hIJ : I ≤ J) (hI : I ≠ 0) : ∃ a, I ⊔ Ideal.span { a } = J := by
classical
obtain ⟨I, rfl⟩ := Ideal.dvd_iff_le.mpr hIJ
simp only [ne_eq, mul_eq_zero, not_or] at hI
obtain ⟨hJ, hI⟩ := hI
suffices ∃ a, ∃ K, J * K = Ideal.span { a } ∧ I + K = ⊤
by
obtain ⟨a, K, e, e'⟩ := this
exact ⟨a, by rw [← e, ← Ideal.add_eq_sup, ← mul_add, e', Ideal.mul_top]⟩
let s := (I.finite_factors hI).toFinset
have : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ { p }, q.asIdeal :=
by
intro p hps
conv_rhs => rw [← mul_one (J * _)]
rw [Finset.prod_eq_mul_prod_diff_singleton hps, ← mul_assoc, mul_right_comm _ p.asIdeal]
refine mul_lt_mul_of_pos_left ?_ ?_
· rw [Ideal.one_eq_top, lt_top_iff_ne_top]
exact p.2.ne_top
· rw [Ideal.zero_eq_bot, bot_lt_iff_ne_bot, ← Ideal.zero_eq_bot, mul_ne_zero_iff, Finset.prod_ne_zero_iff]
exact ⟨hJ, fun x _ ↦ x.3⟩
choose! a ha ha' using fun p hps ↦ SetLike.exists_of_lt (this p hps)
obtain ⟨K, hK⟩ : J ∣ Ideal.span {∑ p ∈ s, a p} :=
by
rw [Ideal.dvd_iff_le, Ideal.span_singleton_le_iff_mem]
exact sum_mem fun p hp ↦ Ideal.mul_le_right (ha p hp)
refine ⟨_, _, hK.symm, ?_⟩
by_contra H
obtain ⟨p, hp, h⟩ := Ideal.exists_le_maximal _ H
let p' : HeightOneSpectrum R := ⟨p, hp.isPrime, fun e ↦ hI (by simp_all)⟩
have hp's : p' ∈ s := by simpa [p', s, Ideal.dvd_iff_le] using le_sup_left.trans h
have H₁ : J * K ≤ J * p := Ideal.mul_mono_right (le_sup_right.trans h)
replace H₁ := hK.trans_le H₁ (Ideal.mem_span_singleton_self _)
have H₂ : ∑ q ∈ s \ { p' }, a q ∈ J * p := by
refine sum_mem fun q hq ↦ ?_
rw [Finset.mem_sdiff, Finset.mem_singleton] at hq
refine Ideal.mul_mono_right ?_ (ha q hq.1)
exact Ideal.prod_le_inf.trans (Finset.inf_le (b := p') (by simpa [hp's] using Ne.symm hq.2))
apply ha' _ hp's
have :=
IsDedekindDomain.inf_prime_pow_eq_prod s (fun i ↦ i.asIdeal) (fun _ ↦ 1) (fun i _ ↦ i.prime)
(fun i _ j _ e ↦ mt HeightOneSpectrum.ext e)
simp only [pow_one] at this
have inst : Nonempty { x // x ∈ s } := ⟨_, hp's⟩
rw [← this, Finset.inf_eq_iInf, iInf_subtype', Ideal.mul_iInf, Ideal.mem_iInf]
rintro ⟨q, hq⟩
by_cases hqp : q = p'
· subst hqp
convert sub_mem H₁ H₂
rw [Finset.sum_eq_add_sum_diff_singleton hp's, add_sub_cancel_right]
· refine Ideal.mul_mono_right ?_ (ha p' hp's)
exact Ideal.prod_le_inf.trans (Finset.inf_le (b := q) (by simpa [hq] using hqp))
