English
Under GoingDown, there exists an LT-Series of primes in S extending a given LT-Series in R with last element P lying over p, preserving length and linking to the original in a compatible way.
Русский
При условии GoingDown существует LT-последовательность примитивов в S, которая расширяет заданную LT-последовательность в R и удовлетворяет совместимости с исходной последовательностью.
LaTeX
$$Given the complexity, the statement asserts existence of an LT-Series L in PrimeSpectrum S matching a given L in R with last element P over p and preserving length and a specified map relation.$$
Lean4
theorem exists_ltSeries_of_hasGoingDown [Algebra.HasGoingDown R S] (l : LTSeries (PrimeSpectrum R)) (P : Ideal S)
[P.IsPrime] [lo : P.LiesOver l.last.asIdeal] :
∃ (L : LTSeries (PrimeSpectrum S)),
L.length = l.length ∧ L.last = ⟨P, inferInstance⟩ ∧ List.map (algebraMap R S).specComap L.toList = l.toList :=
by
induction l using RelSeries.inductionOn generalizing P with
| singleton q =>
use RelSeries.singleton _ ⟨P, inferInstance⟩
simp only [RelSeries.singleton_length, RelSeries.last_singleton, RelSeries.toList_singleton, List.map_cons,
List.map_nil, List.cons.injEq, and_true, true_and]
ext : 1
simpa using lo.over.symm
| cons l q lt ih =>
simp only [RelSeries.last_cons] at lo
obtain ⟨L, len, last, spec⟩ := ih P
have : L.head.asIdeal.LiesOver l.head.asIdeal := by
constructor
rw [← L.toList_getElem_zero_eq_head, ← l.toList_getElem_zero_eq_head, Ideal.under_def]
have : l.toList[0] = (algebraMap R S).specComap L.toList[0] := by
rw [List.getElem_map_rev (algebraMap R S).specComap, List.getElem_of_eq spec.symm _]
rwa [RingHom.specComap, PrimeSpectrum.ext_iff] at this
obtain ⟨Q, Qlt, hQ, Qlo⟩ := Ideal.exists_ideal_lt_liesOver_of_lt L.head.asIdeal lt
use L.cons ⟨Q, hQ⟩ Qlt
simp only [RelSeries.cons_length, add_left_inj, RelSeries.last_cons]
exact ⟨len, last, by simpa [spec] using PrimeSpectrum.ext_iff.mpr Qlo.over.symm⟩
