mono_of_isZero_kernel' — Mathlib

English

If the kernel fork c of f is a limit and c.pt is zero, then f is mono.

Русский

Если ядро ядра kernel f образует ограничение с нулевой точкой, то f является моно.

LaTeX

$$$\text{IsLimit}(c) \land \text{IsZero}(c.pt) \Rightarrow \operatorname{Mono}(f)$$$

Lean4

theorem mono_of_isZero_kernel' {X Y : C} {f : X ⟶ Y} (c : KernelFork f) (hc : IsLimit c) (h : IsZero c.pt) : Mono f :=
  mono_of_cancel_zero _
    (fun g hg => by
      obtain ⟨a, ha⟩ := KernelFork.IsLimit.lift' hc _ hg
      rw [← ha, h.eq_of_tgt a 0, Limits.zero_comp])

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