mapKer — Mathlib

English

A natural map between extensions induces a map between their kernels, respecting linear structure and scalar action.

Русский

Натуральный отображение между расширениями индуцирует отображение их ядер, учитывающее линейность и скалярное действие.

LaTeX

$$$\\text{mapKer}(f) : P.ker \\to_{P.Ring} P'.ker$$$

Lean4

/-- A map between extensions induce a map between kernels. -/
@[simps]
def mapKer (f : P.Hom P') [alg : Algebra P.Ring P'.Ring] (halg : algebraMap P.Ring P'.Ring = f.toRingHom) :
    P.ker →ₗ[P.Ring] P'.ker
    where
  toFun x := ⟨f.toRingHom x, by simp [show algebraMap P.Ring S x = 0 from x.2]⟩
  map_add' _ _ := Subtype.ext (map_add _ _ _)
  map_smul' := by simp [Algebra.smul_def, ← halg]

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