Theorems · Theorem · commutative algebra

Ideal.map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes

∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] {I p : Ideal R}
  {P : Ideal S} [P.IsPrime] [P.LiesOver p],
  p ∈ I.minimalPrimes →
    ∀ {J : Ideal S},
      J ≤ P →
        Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) P ∈
            (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) J).minimalPrimes →
          P ∈ (Ideal.map (algebraMap R S) I ⊔ J).minimalPrimes

If P lies over p, p is a minimal prime over I and the image of P is a minimal prime over the image of J in S ⧸ p S, then P is a minimal prime over I S ⊔ J.

Defined in

Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommRingAlgebraIdeal.IsPrimeIdeal.LiesOver