ker_mapAlgHom — Mathlib

English

The kernel of the polynomial map induced by an algebra hom f equals the ideal map of ker f under the polynomial constant embedding.

Русский

Ядро отображения, индуцированного алгебраическим гомоморфом f, равно образу ядра f через константное вложение полиномов.

LaTeX

$$$\ker(\mathrm{MvPolynomial.mapAlgHom}(f)) = \operatorname{Ideal.map}(\mathrm{C}) (\ker f)$$$

Lean4

theorem ker_mapAlgHom {S₁ S₂ σ : Type*} [CommRing S₁] [CommRing S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :
    RingHom.ker (MvPolynomial.mapAlgHom (σ := σ) f) = Ideal.map MvPolynomial.C (RingHom.ker f) :=
  MvPolynomial.ker_map (f.toRingHom : S₁ →+* S₂)

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