isZero_of_mono — Mathlib

English

The kernel of a morphism is zero if the morphism is zero and the fork is limit.

Русский

Ядро морфизма равно нулю, если морфизм нулевой и вилочный предел существует.

LaTeX

$$$\\operatorname{isZero}\\bigl(\\ker f\\bigr)$, если $f$ нуль-моноим, где $c$ — ядровая вилка.$$

Lean4

theorem isZero_of_mono {X Y : C} {f : X ⟶ Y} {c : KernelFork f} (hc : IsLimit c) [Mono f] : IsZero c.pt :=
  by
  have := Fork.IsLimit.mono hc
  rw [IsZero.iff_id_eq_zero, ← cancel_mono c.ι, ← cancel_mono f, Category.assoc, Category.assoc, c.condition, comp_zero,
    zero_comp]

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