ker_mapRingHom — Mathlib

English

The kernel of the polynomial map mapRingHom f: R[X] → S[X] is exactly the ideal in R[X] obtained by mapping the kernel of f via the embedding C: R → R[X].

Русский

Ядро отображения mapRingHom f равно образу (через C) ядра f на R[X].

LaTeX

$$$\\mathrm{ker}(\\mathrm{Polynomial.mapRingHom} f) = (\\mathrm{ker} f).map(\\mathcal{C})$$$

Lean4

theorem _root_.Polynomial.ker_mapRingHom (f : R →+* S) :
    RingHom.ker (Polynomial.mapRingHom f) = (RingHom.ker f).map (C : R →+* R[X]) :=
  by
  ext
  simp only [RingHom.mem_ker, coe_mapRingHom]
  rw [mem_map_C_iff, Polynomial.ext_iff]
  simp [RingHom.mem_ker]

Похожие утверждения