English
Let S be a Dedekind domain, P an ideal with P ≠ ⊥ and [P IsPrime]. If a ∈ P^i \ P^{i+1} and c ∈ P^i, then there exist d ∈ S and e ∈ P^{i+1} such that a d + e = c.
Русский
Пусть S — область Дедекندا, P — идеал, не равный нулю, и PIsPrime. Если a ∈ P^i \\ P^{i+1} и c ∈ P^i, то существуют d ∈ S и e ∈ P^{i+1}, такие что a d + e = c.
LaTeX
$$$[\\text{IsDedekindDomain } S]\\;\\rightarrow\\; (h_P : P \\neq \\bottom) \\rightarrow \\forall i\\in\\mathbb{N}, a,c \\in S:\\; a \\in P^i \\land a \\notin P^{i+1} \\land c \\in P^i \\Rightarrow \\exists d\\in S,\\; \\exists e\\in P^{i+1},\\; a d + e = c$$$
Lean4
/-- If `a ∈ P^i \ P^(i+1)` and `c ∈ P^i`, then `a * d + e = c` for `e ∈ P^(i+1)`.
`Ideal.mul_add_mem_pow_succ_unique` shows the choice of `d` is unique, up to `P`.
Inspired by [Neukirch], proposition 6.1 -/
theorem exists_mul_add_mem_pow_succ [IsDedekindDomain S] (hP : P ≠ ⊥) {i : ℕ} (a c : S) (a_mem : a ∈ P ^ i)
(a_notMem : a ∉ P ^ (i + 1)) (c_mem : c ∈ P ^ i) : ∃ d : S, ∃ e ∈ P ^ (i + 1), a * d + e = c :=
by
suffices eq_b : P ^ i = Ideal.span { a } ⊔ P ^ (i + 1)
by
rw [eq_b] at c_mem
simp only [mul_comm a]
exact Ideal.mem_span_singleton_sup.mp c_mem
refine
(Ideal.eq_prime_pow_of_succ_lt_of_le hP (lt_of_le_of_ne le_sup_right ?_)
(sup_le (Ideal.span_le.mpr (Set.singleton_subset_iff.mpr a_mem)) (Ideal.pow_succ_lt_pow hP i).le)).symm
contrapose! a_notMem with this
rw [this]
exact mem_sup.mpr ⟨a, mem_span_singleton_self a, 0, by simp, by simp⟩
