Theorems · Theorem · commutative algebra

Ideal.comap_eq_of_scalar_tower_quotient

∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {p : Ideal R} {P : Ideal S}
  [inst_2 : Algebra R S] [inst_3 : Algebra (R ⧸ p) (S ⧸ P)] [IsScalarTower R (R ⧸ p) (S ⧸ P)],
  Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P)) → Ideal.comap (algebraMap R S) P = p

If there is an injective map R/p → S/P such that the following diagram commutes: `` R → S ↓ ↓ R/p → S/P ` then P lies over p`.

Defined in

Mathlib.RingTheory.Ideal.Over

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraAlgebraIsScalarTower