English
Given a finite chain p of primes in Spec R and x ∈ last.asIdeal, there exists a refinement q of the same length with x ∈ (q 1).asIdeal and the same endpoints p.head, p.last, matching length.
Русский
Дана конечная цепь p цепи прим в Spec(R) и x ∈ last.asIdeal; существует цепь q той же длины, такая что x ∈ (q 1).asIdeal, и головы и хвоста совпадают: head(p) = head(q), last(p) = last(q).
LaTeX
$$$\\exists q: LTSeries(\\mathrm{PrimeSpectrum}\\ R),\\; x \\in (q\\ 1).asIdeal \\land p.length = q.length \\land p.head = q.head \\land p.last = q.last$$$
Lean4
/-- Let $R$ be a Noetherian ring, $\mathfrak{p}_0 < \dots < \mathfrak{p}_n$ be a
chain of primes, $x \in \mathfrak{p}_n$. Then we can find another chain of primes
$\mathfrak{q}_0 < \dots < \mathfrak{q}_n$ such that $x \in \mathfrak{q}_1$,
$\mathfrak{p}_0 = \mathfrak{q}_0$ and $\mathfrak{p}_n = \mathfrak{q}_n$. -/
theorem exist_ltSeries_mem_one_of_mem_last (p : LTSeries (PrimeSpectrum R)) {x : R} (hx : x ∈ p.last.asIdeal) :
∃ q : LTSeries (PrimeSpectrum R), x ∈ (q 1).asIdeal ∧ p.length = q.length ∧ p.head = q.head ∧ p.last = q.last :=
by
generalize hp : p.length = n
induction n generalizing p with
| zero =>
use RelSeries.singleton _ p.last
simp only [RelSeries.singleton_toFun, hx, RelSeries.singleton_length, RelSeries.head, RelSeries.last_singleton,
and_true, true_and]
rw [show 0 = Fin.last p.length from Fin.zero_eq_mk.mpr hp, RelSeries.last]
| succ n hn => ?_
by_cases h0 : n = 0
· use p
have h1 : 1 = Fin.last p.length := by
rw [Fin.last, hp, h0, zero_add]
exact Fin.natCast_eq_mk (Nat.one_lt_succ_succ 0)
simpa [h1, hp] using hx
obtain ⟨q, hxq, h2, hq⟩ : ∃ q : PrimeSpectrum R, x ∈ q.1 ∧ p ⟨p.length - 2, _⟩ < q ∧ q < p.last :=
(p ⟨p.length - 1, p.length.sub_lt_succ 1⟩).exist_mem_one_of_mem_two (p.strictMono (Nat.pred_lt (by simpa [hp])))
(p.strictMono (Nat.pred_lt (by simp [hp]))) hx
obtain ⟨Q, hx, hQ, hh, hl⟩ :=
hn (p.eraseLast.eraseLast.snoc q h2) (by simpa using hxq) <| by simpa [hp] using Nat.succ_pred_eq_of_ne_zero h0
have h1 : 1 < Q.length + 1 := Nat.lt_of_sub_ne_zero (hQ.symm.trans_ne h0)
have h : 1 = (1 : Fin (Q.length + 1)).castSucc := by simp [Fin.one_eq_mk_of_lt h1]
exact ⟨Q.snoc p.last (by simpa [← hl] using hq), by simpa [h], by simpa, by simp [← hh], by simp⟩
