Theorems · Theorem · commutative algebra

Ideal.exists_ideal_over_maximal_of_isIntegral

∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] (P : Ideal R) [P_max : P.IsMaximal],
  RingHom.ker (algebraMap R S) ≤ P → ∃ Q, Q.IsMaximal ∧ Ideal.comap (algebraMap R S) Q = P

comap (algebraMap R S) is a surjection from the max spec of S to max spec of R. hP : (algebraMap R S).ker ≤ P is a slight generalization of the extension being injective

Defined in

Mathlib.RingTheory.Ideal.GoingUp

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraAlgebra.IsIntegralIdeal.IsMaximal