English
In the constructed map range setting, only the zero constant remains; i.e., if C x lies in the image of I under the map, then x = 0.
Русский
В данной конфигурации диапазона отображения остаётся только нулевой констант; если C x лежит в образе I под отображением, то x = 0.
LaTeX
$$$x = 0$ under the hypothesis that $C x \\in I.map (Polynomial.map)\\,.$$$
Lean4
/-- Given any ring `R` and an ideal `I` of `R[X]`, we get a map `R → R[x] → R[x]/I`.
If we let `R` be the image of `R` in `R[x]/I` then we also have a map `R[x] → R'[x]`.
In particular we can map `I` across this map, to get `I'` and a new map `R' → R'[x] → R'[x]/I`.
This theorem shows `I'` will not contain any non-zero constant polynomials. -/
theorem eq_zero_of_polynomial_mem_map_range (I : Ideal R[X]) (x : ((Quotient.mk I).comp C).range)
(hx : C x ∈ I.map (Polynomial.mapRingHom ((Quotient.mk I).comp C).rangeRestrict)) : x = 0 :=
by
let i := ((Quotient.mk I).comp C).rangeRestrict
have hi' : RingHom.ker (Polynomial.mapRingHom i) ≤ I :=
by
refine fun f hf => polynomial_mem_ideal_of_coeff_mem_ideal I f fun n => ?_
rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
rw [RingHom.mem_ker, coe_mapRingHom] at hf
replace hf := congr_arg (fun f : Polynomial _ => f.coeff n) hf
simp only [coeff_map, coeff_zero] at hf
rwa [Subtype.ext_iff, RingHom.coe_rangeRestrict] at hf
obtain ⟨x, hx'⟩ := x
obtain ⟨y, rfl⟩ := RingHom.mem_range.1 hx'
refine Subtype.eq ?_
simp only [RingHom.comp_apply, Quotient.eq_zero_iff_mem, ZeroMemClass.coe_zero]
suffices C (i y) ∈ I.map (Polynomial.mapRingHom i)
by
obtain ⟨f, hf⟩ :=
mem_image_of_mem_map_of_surjective (Polynomial.mapRingHom i)
(Polynomial.map_surjective _ (RingHom.rangeRestrict_surjective ((Quotient.mk I).comp C))) this
refine sub_add_cancel (C y) f ▸ I.add_mem (hi' ?_ : C y - f ∈ I) hf.1
rw [RingHom.mem_ker, RingHom.map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]
exact hx
