English
The map r A is a monomorphism: r A is mono.
Русский
Отображение r A является мономорфизмом.
LaTeX
$$$\\operatorname{Mono}(\\mathrm{r}\\ A)$$$
Lean4
instance mono_r {A : C} : Mono (r A) :=
by
let hl : IsLimit (KernelFork.ofι (diag A) (cokernel.condition (diag A))) :=
monoIsKernelOfCokernel _ (colimit.isColimit _)
apply NormalEpiCategory.mono_of_cancel_zero
intro Z x hx
have hxx : (x ≫ prod.lift (𝟙 A) (0 : A ⟶ A)) ≫ cokernel.π (diag A) = 0 := by rw [Category.assoc, hx]
obtain ⟨y, hy⟩ := KernelFork.IsLimit.lift' hl _ hxx
rw [KernelFork.ι_ofι] at hy
have hyy : y = 0 := by
erw [← Category.comp_id y, ← Limits.prod.lift_snd (𝟙 A) (𝟙 A), ← Category.assoc, hy, Category.assoc, prod.lift_snd,
HasZeroMorphisms.comp_zero]
haveI : Mono (prod.lift (𝟙 A) (0 : A ⟶ A)) := mono_of_mono_fac (prod.lift_fst _ _)
apply (cancel_mono (prod.lift (𝟙 A) (0 : A ⟶ A))).1
rw [← hy, hyy, zero_comp, zero_comp]
