toKernelSubobject — Mathlib

English

There is a canonical linear map from ker f.hom to the kernelSubobject f.

Русский

Существует каноническое линейное отображение от ядра $f$ к kernelSubobject $f$.

LaTeX

$$$\text{toKernelSubobject}: \ker f_{\mathrm{hom}} \to \kerSubobject f$$$

Lean4

/-- Bundle an element `m : M` such that `f m = 0` as a term of `kernelSubobject f`. -/
noncomputable def toKernelSubobject {M N : ModuleCat.{v} R} {f : M ⟶ N} : LinearMap.ker f.hom →ₗ[R] kernelSubobject f :=
  (kernelSubobjectIso f ≪≫ ModuleCat.kernelIsoKer f).inv.hom

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