Theorems · Theorem · commutative algebra

Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert

∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {q p : Ideal R} [q.IsPrime],
  q < p →
    ∀ (x : R) (s : Set R),
      p ∈ (Ideal.span (insert x s)).minimalPrimes →
        ∀ t ⊆ ↑q, s ⊆ ↑(Ideal.span (insert x t)).radical → q ∈ (Ideal.span t).minimalPrimes

If q < p are prime ideals such that p is minimal over span (s ∪ {x}) and t is a set contained in q such that s ⊆ √span (t ∪ {x}), then q is minimal over span t. This is used in the induction step for the proof of Krull's height theorem.

Defined in

Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsNoetherianRingIdeal.IsPrime