English
For all X, the morphism diag X followed by σ is zero: diag X ≫ σ = 0.
Русский
Для каждого X композиция диагонали с σ равна нулю: diag X ≫ σ = 0.
LaTeX
$$$\\forall X,\\ \\operatorname{diag}(X) \\;\\circ\\; \\sigma = 0$$$
Lean4
/-- The canonical morphism `i : coimage f ⟶ Q` is a monomorphism -/
instance : Mono (Abelian.factorThruCoimage f) :=
let I := Abelian.coimage f
let i := Abelian.factorThruCoimage f
let p := cokernel.π (kernel.ι f)
NormalEpiCategory.mono_of_cancel_zero _ fun R (g : R ⟶ I) (hgi : g ≫ i = 0) => by
-- Since C is abelian, u := p ≫ coker g is the cokernel of some morphism h.
let u := p ≫ cokernel.π g
haveI hu := normalEpiOfEpi u
let h := hu.g
obtain ⟨t, ht⟩ := cokernel.desc' g i hgi
have hf : h ≫ f = 0 :=
calc
h ≫ f = h ≫ p ≫ i := (Abelian.coimage.fac f).symm ▸ rfl
_ = h ≫ p ≫ cokernel.π g ≫ t := (ht ▸ rfl)
_ = h ≫ u ≫ t := by simp only [u, Category.assoc]
_ = 0 ≫ t := by rw [← Category.assoc, hu.w]
_ = 0 := zero_comp
obtain ⟨l, hl⟩ := kernel.lift' f h hf
have hhp : h ≫ p = 0 :=
calc
h ≫ p = (l ≫ kernel.ι f) ≫ p := hl ▸ rfl
_ = l ≫ 0 := by rw [Category.assoc, cokernel.condition]
_ = 0 := comp_zero
obtain ⟨s, hs⟩ := NormalEpi.desc' u p hhp
have hs' : p ≫ cokernel.π g ≫ s = p ≫ 𝟙 I := by rw [← Category.assoc, hs, Category.comp_id]
haveI : Mono (cokernel.π g) :=
mono_of_mono_fac
((cancel_epi _).1 hs')
-- coker g is a monomorphism, but g ≫ coker g = 0 = 0 ≫ coker g, so g = 0 as required.
exact zero_of_comp_mono _ (cokernel.condition g)
