English
Let R be Noetherian and local, with a chain of primes p0 < p1 < 𝔪 = maximal ideal. If x lies in 𝔪, then there exists a prime q containing x with p0 < q < 𝔪.
Русский
Пусть R — Noetherian локальное кольцо, и есть цепочка праймов p0 < p1 < 𝔪, где 𝔪 — максимальный идеал. При любом x ∈ 𝔪 существует простая цепь q с x ∈ q, и p0 < q < 𝔪.
LaTeX
$$$\\text{If } R \\text{ is Noetherian and local, and } p_0 < p_1 < \\mathfrak m, \\text{ with } x \\in \\mathfrak m, \\text{ then } \\exists q:\\mathrm{Spec}(R),\\; x \\in q.asIdeal \\land p_0 < q \\land q.asIdeal < \\mathfrak m.$$$
Lean4
theorem exist_mem_one_of_mem_maximal_ideal [IsLocalRing R] {p₁ p₀ : PrimeSpectrum R} (h₀ : p₀ < p₁)
(h₁ : p₁ < closedPoint R) {x : R} (hx : x ∈ 𝔪) : ∃ q : PrimeSpectrum R, x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪 :=
by
by_cases hn : x ∈ p₀.1
· exact ⟨p₁, h₀.le hn, h₀, h₁⟩
let e := p₀.1.primeSpectrumQuotientOrderIsoZeroLocus.symm
obtain ⟨q, hq⟩ :=
(p₀.1 + span { x }).nonempty_minimalPrimes <|
sup_le (IsLocalRing.le_maximalIdeal_of_isPrime p₀.1) ((span_singleton_le_iff_mem 𝔪).mpr hx) |>.trans_lt
(IsMaximal.isPrime' 𝔪).1.lt_top |>.ne
let q : PrimeSpectrum R := ⟨q, hq.1.1⟩
have : q.1.IsPrime := q.2
have hxq : x ∈ q.1 := le_sup_right.trans hq.1.2 (mem_span_singleton_self x)
refine ⟨q, hxq, lt_of_le_not_ge (le_sup_left.trans hq.1.2) fun h ↦ hn (h hxq), ?_⟩
refine lt_of_le_of_ne (IsLocalRing.le_maximalIdeal_of_isPrime q.1) fun hqm ↦ ?_
have h : (e ⟨q, le_sup_left.trans hq.1.2⟩).1.height ≤ 1 := map_height_le_one_of_mem_minimalPrimes hq
simp_rw [show q = closedPoint R from PrimeSpectrum.ext hqm] at h
have hph : (e ⟨p₁, h₀.le⟩).1.height ≤ 0 :=
Order.lt_one_iff_nonpos.mp (height_le_iff.mp h _ inferInstance (by simpa using h₁))
refine ENat.not_lt_zero (e ⟨p₀, le_refl p₀⟩).1.height (height_le_iff.mp hph _ inferInstance ?_)
simpa using h₀
