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