Theorems · Theorem · commutative algebra

Ideal.exists_ltSeries_of_hasGoingDown

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.HasGoingDown R S] (l : LTSeries (PrimeSpectrum R)) (P : Ideal S) [inst_4 : P.IsPrime]
  [lo : P.LiesOver (RelSeries.last l).asIdeal],
  ∃ L,
    L.length = l.length ∧
      RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = RelSeries.toList l

Defined in

Mathlib.RingTheory.Ideal.GoingDown

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraAlgebra.HasGoingDownIdeal.IsPrimeIdeal.LiesOver