English
For a nonzero ideal I and a maximal M with I ≤ M in a Dedekind domain not a field, there exists a finite multiset Z of primes such that (M :: Z)⋅prod ≤ I but prod ≤ I fails.
Русский
Для ненулевого идеала I и максимального M с I ≤ M в Дедекинд домене не являющемся полем существует конечный мульттерес простых Z так, что (M :: Z)⋅prod ≤ I, но prod ≤ I не выполняется.
LaTeX
$$$$\\exists Z:\\ Multiset(PrimeSpectrum A),\\; (M \\colon Z) \\cdot \\prod Z \\le I \\land \\lnot(\\prod Z \\le I).$$$$
Lean4
/-- Specialization of `exists_primeSpectrum_prod_le_and_ne_bot_of_domain` to Dedekind domains:
Let `I : Ideal A` be a nonzero ideal, where `A` is a Dedekind domain that is not a field.
Then `exists_primeSpectrum_prod_le_and_ne_bot_of_domain` states we can find a product of prime
ideals that is contained within `I`. This lemma extends that result by making the product minimal:
let `M` be a maximal ideal that contains `I`, then the product including `M` is contained within `I`
and the product excluding `M` is not contained within `I`. -/
theorem exists_multiset_prod_cons_le_and_prod_not_le [IsDedekindDomain A] (hNF : ¬IsField A) {I M : Ideal A}
(hI0 : I ≠ ⊥) (hIM : I ≤ M) [hM : M.IsMaximal] :
∃ Z : Multiset (PrimeSpectrum A),
(M ::ₘ Z.map PrimeSpectrum.asIdeal).prod ≤ I ∧ ¬Multiset.prod (Z.map PrimeSpectrum.asIdeal) ≤ I :=
by
-- Let `Z` be a minimal set of prime ideals such that their product is contained in `J`.
obtain ⟨Z₀, hZ₀⟩ := PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain hNF hI0
obtain ⟨Z, ⟨hZI, hprodZ⟩, h_eraseZ⟩ :=
wellFounded_lt.has_min {Z | (Z.map PrimeSpectrum.asIdeal).prod ≤ I ∧ (Z.map PrimeSpectrum.asIdeal).prod ≠ ⊥}
⟨Z₀, hZ₀.1, hZ₀.2⟩
obtain ⟨_, hPZ', hPM⟩ :=
hM.isPrime.multiset_prod_le.mp
(hZI.trans hIM)
-- Then in fact there is a `P ∈ Z` with `P ≤ M`.
obtain ⟨P, hPZ, rfl⟩ := Multiset.mem_map.mp hPZ'
classical
have := Multiset.map_erase PrimeSpectrum.asIdeal (fun _ _ => PrimeSpectrum.ext) P Z
obtain ⟨hP0, hZP0⟩ : P.asIdeal ≠ ⊥ ∧ ((Z.erase P).map PrimeSpectrum.asIdeal).prod ≠ ⊥ := by
rwa [Ne, ← Multiset.cons_erase hPZ', Multiset.prod_cons, Ideal.mul_eq_bot, not_or, ← this] at hprodZ
have hPM' := (P.isPrime.isMaximal hP0).eq_of_le hM.ne_top hPM
subst hPM'
refine ⟨Z.erase P, ?_, ?_⟩
· convert hZI
rw [this, Multiset.cons_erase hPZ']
· refine fun h => h_eraseZ (Z.erase P) ⟨h, ?_⟩ (Multiset.erase_lt.mpr hPZ)
exact hZP0
