English
If f is mono, then Abelian.factorThruCoimage f is an isomorphism.
Русский
Если f мономорфизм, то Abelian.factorThruCoimage f — изоморфизм.
LaTeX
$$$\\text{Mono}(f) \\Rightarrow \\operatorname{IsIso}(\\mathrm{Abelian.factorThruCoimage}\\, f)$$$
Lean4
/-- The map `p : P ⟶ image f` is an epimorphism -/
instance : Epi (Abelian.factorThruImage f) :=
let I := Abelian.image f
let p := Abelian.factorThruImage f
let i :=
kernel.ι
(cokernel.π f)
-- It will suffice to consider some g : I ⟶ R such that p ≫ g = 0 and show that g = 0.
NormalMonoCategory.epi_of_zero_cancel _ fun R (g : I ⟶ R) (hpg : p ≫ g = 0) => by
-- Since C is abelian, u := ker g ≫ i is the kernel of some morphism h.
let u := kernel.ι g ≫ i
haveI hu := normalMonoOfMono u
let h := hu.g
obtain ⟨t, ht⟩ := kernel.lift' g p hpg
have fh : f ≫ h = 0 :=
calc
f ≫ h = (p ≫ i) ≫ h := (Abelian.image.fac f).symm ▸ rfl
_ = ((t ≫ kernel.ι g) ≫ i) ≫ h := (ht ▸ rfl)
_ = t ≫ u ≫ h := by simp only [u, Category.assoc]
_ = t ≫ 0 := (hu.w ▸ rfl)
_ = 0 :=
HasZeroMorphisms.comp_zero _
_
-- h factors through the cokernel of f via some l.
obtain ⟨l, hl⟩ := cokernel.desc' f h fh
have hih : i ≫ h = 0 :=
calc
i ≫ h = i ≫ cokernel.π f ≫ l := hl ▸ rfl
_ = 0 ≫ l := by rw [← Category.assoc, kernel.condition]
_ = 0 := zero_comp
obtain ⟨s, hs⟩ := NormalMono.lift' u i hih
have hs' : (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i := by rw [Category.assoc, hs, Category.id_comp]
haveI : Epi (kernel.ι g) :=
epi_of_epi_fac
((cancel_mono _).1 hs')
-- ker g is an epimorphism, but ker g ≫ g = 0 = ker g ≫ 0, so g = 0 as required.
exact zero_of_epi_comp _ (kernel.condition g)
