kernelSubobject_zero — Mathlib

English

For any category with zero morphisms, kernelSubobject (0 : A ⟶ B) is the top subobject of A.

Русский

В категории с нулевыми морфизмами kernelSubobject(0) сопоставимому A является верхним подобъектом.

LaTeX

$$$$ kernelSubobject (0 : A \\to B) = \\top $$$$

Lean4

@[simp]
theorem kernelSubobject_zero {A B : C} : kernelSubobject (0 : A ⟶ B) = ⊤ :=
  (isIso_iff_mk_eq_top _).mp (by infer_instance)

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