instHasKernelSnd — Mathlib

English

In any category with binary biproducts X ⊞ Y, the second projection biprod.snd : X ⊞ Y → Y has a kernel, namely the canonical kernel fork associated to the first summand.

Русский

В любой категории, где существуют бинарные биобразные произведения X ⊞ Y, у проекции второго компонента biprod.snd : X ⊞ Y → Y имеется ядро, равное каноническому Fork-ядру, соответствующему первому компоненту.

LaTeX

$$$\operatorname{HasKernel}(\mathrm{biprod.snd}: X\oplus Y \to Y).$$$

Lean4

instance : HasKernel (biprod.snd : X ⊞ Y ⟶ Y) :=
  HasLimit.mk ⟨_, biprod.isKernelSndKernelFork X Y⟩

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