Lemmas about LTSeries in the prime spectrum

Main results

• PrimeSpectrum.exist_ltSeries_mem_one_of_mem_last: 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 PrimeSpectrum.exist_mem_one_of_mem_maximal_ideal {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {p₁ p₀ : PrimeSpectrum R} (h₀ : p₀ < p₁) (h₁ : p₁ < IsLocalRing.closedPoint R) {x : R} (hx : x ∈ IsLocalRing.maximalIdeal R) : ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < IsLocalRing.maximalIdeal R

theorem PrimeSpectrum.exist_mem_one_of_mem_two {R : Type u_1} [CommRing R] [IsNoetherianRing R] {p₁ p₀ p₂ : PrimeSpectrum R} (h₀ : p₀ < p₁) (h₁ : p₁ < p₂) {x : R} (hx : x ∈ p₂.asIdeal) : ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂

theorem PrimeSpectrum.exist_ltSeries_mem_one_of_mem_last {R : Type u_1} [CommRing R] [IsNoetherianRing R] (p : LTSeries (PrimeSpectrum R)) {x : R} (hx : x ∈ (RelSeries.last p).asIdeal) : ∃ (q : LTSeries (PrimeSpectrum R)), x ∈ (q.toFun 1).asIdeal ∧ p.length = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q

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$.