Theorems · Theorem · algebraic geometry

PrimeSpectrum.exist_ltSeries_mem_one_of_mem_last

∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : LTSeries (PrimeSpectrum R)) {x : R},
  x ∈ (RelSeries.last p).asIdeal →
    ∃ q,
      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$.

Defined in

Mathlib.RingTheory.Spectrum.Prime.LTSeries

Cited by

1 results in Mathlib

Foundations

Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsNoetherianRing