English
In an abelian category, the pullback of an epimorphism is an epimorphism. If f: X → Z is epi, then the second projection pullback.snd f g: Pullback f g → Y is epi.
Русский
В абелевой категории прообраз (pullback) эпиморфизма является эпиморфизмом. Если f: X → Z — эпиморфизм, тогда проекция pullback.snd f g: Pullback f g → Y — эпиморфизм.
LaTeX
$$$\\\\forall C \\\\[CategoryTheory.Abelian C],\\\\forall X,Y,Z \\\\in C, \\\\forall f: X \\\\to Z, g: Y \\\\to Z, [Epi f], \\\\mathrm{Epi}(\\\\mathrm{pullback.snd} \\\\ f \\\\ g).$$$
Lean4
/-- In an abelian category, the pullback of an epimorphism is an epimorphism.
Proof from [aluffi2016, IX.2.3], cf. [borceux-vol2, 1.7.6] -/
instance epi_pullback_of_epi_f [Epi f] : Epi (pullback.snd f g) :=
-- It will suffice to consider some morphism e : Y ⟶ R such that
-- pullback.snd f g ≫ e = 0 and show that e = 0.
epi_of_cancel_zero _ fun {R} e h => by
-- Consider the morphism u := (0, e) : X ⊞ Y⟶ R.
let u := biprod.desc (0 : X ⟶ R) e
have hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0 := by
simpa [u]
-- pullbackToBiproduct f g is a kernel of (f, -g), so (f, -g) is a
-- cokernel of pullbackToBiproduct f g
have :=
epiIsCokernelOfKernel _
(PullbackToBiproductIsKernel.isLimitPullbackToBiproduct f g)
-- We use this fact to obtain a factorization of u through (f, -g) via some d : Z ⟶ R.
obtain ⟨d, hd⟩ := CokernelCofork.IsColimit.desc' this u hu
dsimp at d; dsimp [u] at hd
have : f ≫ d = 0 :=
calc
f ≫ d = (biprod.inl ≫ biprod.desc f (-g)) ≫ d := by rw [biprod.inl_desc]
_ = biprod.inl ≫ u := by rw [Category.assoc, hd]
_ = 0 :=
biprod.inl_desc _
_
-- But f is an epimorphism, so d = 0...
have : d = 0 :=
(cancel_epi f).1
(by simpa)
-- ...or, in other words, e = 0.
calc
e = biprod.inr ≫ biprod.desc (0 : X ⟶ R) e := by rw [biprod.inr_desc]
_ = biprod.inr ≫ biprod.desc f (-g) ≫ d := by rw [← hd]
_ = biprod.inr ≫ biprod.desc f (-g) ≫ 0 := by rw [this]
_ = (biprod.inr ≫ biprod.desc f (-g)) ≫ 0 := by rw [← Category.assoc]
_ = 0 := HasZeroMorphisms.comp_zero _ _
