English
If zero morphism is the kernel of f, then f is mono.
Русский
Если нулевой морфизм является ядром f, то f — моно.
LaTeX
$$$\text{KernelFork.ofι}(0) \to X \Rightarrow Mono f$$$
Lean4
/-- If a zero morphism is a kernel of `f`, then `f` is a monomorphism. -/
theorem mono_of_zero_kernel {X Y : C} (f : X ⟶ Y) (Z : C)
(l : IsLimit (KernelFork.ofι (0 : Z ⟶ X) (show 0 ≫ f = 0 by simp))) : Mono f :=
⟨fun u v huv => by
obtain ⟨W, w, hw, hl⟩ := normalEpiOfEpi (coequalizer.π u v)
obtain ⟨m, hm⟩ := coequalizer.desc' f huv
have reassoced {W : C} (h : coequalizer u v ⟶ W) : w ≫ coequalizer.π u v ≫ h = 0 ≫ h := by
rw [← Category.assoc, eq_whisker hw]
have hwf : w ≫ f = 0 := by rw [← hm, reassoced, zero_comp]
obtain ⟨n, hn⟩ := KernelFork.IsLimit.lift' l _ hwf
rw [Fork.ι_ofι, HasZeroMorphisms.comp_zero] at hn
have : IsIso (coequalizer.π u v) := by apply isIso_colimit_cocone_parallelPair_of_eq hn.symm hl
apply (cancel_mono (coequalizer.π u v)).1
exact coequalizer.condition _ _⟩
