Kernels of scalar multiples of the identity #
In an R-linear category, the inclusion of any kernel fork of m • 𝟙 X is killed by m
(CategoryTheory.Limits.KernelFork.smul_ι_eq_zero).
@[simp]
theorem
CategoryTheory.Limits.KernelFork.smul_ι_eq_zero
{R : Type u_1}
[Semiring R]
{C : Type u_2}
[Category.{u_3, u_2} C]
[Preadditive C]
[Linear R C]
{X : C}
{m : R}
(c : KernelFork (m • CategoryStruct.id X))
:
The inclusion of a kernel fork of m • 𝟙 X is killed by m.