ker_map — Mathlib

English

For a ring hom f, the kernel of the polynomial map MvPolynomial.map f equals the ideal map of ker f by the constant map.

Русский

Для кольцевого гомоморфа f ядро отображения MvPolynomial.map f равно образу ядра f через константное отображение.

LaTeX

$$$\ker(\mathrm{MvPolynomial.map} f) = \operatorname{Ideal.map}(\mathrm{C} : R \to \mathrm{MvPolynomial}(\sigma, R)) (\ker f)$$$

Lean4

theorem ker_map (f : R →+* S) :
    RingHom.ker (map f : MvPolynomial σ R →+* MvPolynomial σ S) =
      Ideal.map (C : R →+* MvPolynomial σ R) (RingHom.ker f) :=
  by
  ext
  rw [MvPolynomial.mem_map_C_iff, RingHom.mem_ker, MvPolynomial.ext_iff]
  simp_rw [coeff_map, coeff_zero, RingHom.mem_ker]

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