Theorems · Theorem · commutative algebra

Ideal.quotient_mk_maps_eq

∀ {R : Type u_1} [inst : CommRing R] (P : Ideal (Polynomial R)),
  ((Ideal.Quotient.mk (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)).comp
          Polynomial.C).comp
      (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) =
    (Ideal.quotientMap (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)
          (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) ⋯).comp
      ((Ideal.Quotient.mk P).comp Polynomial.C)

The identity in this lemma asserts that the "obvious" square `` R → (R / (P ∩ R)) ↓ ↓ R[x] / P → (R / (P ∩ R))[x] / (P / (P ∩ R)) ` commutes. It is used, for instance, in the proof of quotient_mk_comp_C_is_integral_of_jacobson, in the file Mathlib/RingTheory/Jacobson/Polynomial.lean`.

Defined in

Mathlib.RingTheory.Ideal.GoingUp

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing