English
There is an injective map between certain quotient structures arising from a polynomial ideal; the square diagram commutes.
Русский
Существует инъективное отображение между определёнными аquotient-построениями, полученными из идеала над полиномами; диаграмма квадратная коммутирует.
LaTeX
$$$\text{Theorem: }\text{injective quotient map }(P: \text{Ideal } R[X]) : \text{...}$ (formal statement involves quotient maps and commutativity of a square diagram).$$
Lean4
/-- 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`.
-/
theorem quotient_mk_maps_eq (P : Ideal R[X]) :
((Quotient.mk (map (mapRingHom (Quotient.mk (P.comap (C : R →+* R[X])))) P)).comp C).comp
(Quotient.mk (P.comap (C : R →+* R[X]))) =
(Ideal.quotientMap (map (mapRingHom (Quotient.mk (P.comap (C : R →+* R[X])))) P)
(mapRingHom (Quotient.mk (P.comap (C : R →+* R[X])))) le_comap_map).comp
((Quotient.mk P).comp C) :=
by
refine RingHom.ext fun x => ?_
repeat' rw [RingHom.coe_comp, Function.comp_apply]
rw [quotientMap_mk, coe_mapRingHom, map_C]
