le_kernelSubobject — Mathlib

English

If A is a subobject of X with A.arrow ≫ f = 0, then A ≤ kernelSubobject f in the subobject order.

Русский

Если A является подпроизведением X и A.arrow ≫ f = 0, то A ≤ kernelSubobject f в порядке подобъектов.

LaTeX

$$$$ A \\le kernelSubobject f $$$$

Lean4

theorem le_kernelSubobject (A : Subobject X) (h : A.arrow ≫ f = 0) : A ≤ kernelSubobject f :=
  Subobject.le_mk_of_comm (kernel.lift f A.arrow h) (by simp)

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