English
In an abelian category, the pullback of an epimorphism along any morphism has the left projection epi: pullback.fst f g is epi when g is epi.
Русский
В абелевой категории прообраз эпиморфизма вдоль любой стрелки имеет слева направленную метрку эпиморфизма: pullback.fst f g — эпиморфизм, если g — эпиморфизм.
LaTeX
$$$\\\\forall C \\\\[CategoryTheory.Abelian C],\\\\forall X,Y,Z \\\\in C, \\\\forall f: X \\\\to Z, g: Y \\\\to Z, [Epi g], \\\\mathrm{Epi}(\\\\mathrm{pullback.fst} \\\\ f \\\\ g).$$$
Lean4
/-- In an abelian category, the pullback of an epimorphism is an epimorphism. -/
instance epi_pullback_of_epi_g [Epi g] : Epi (pullback.fst f g) :=
-- It will suffice to consider some morphism e : X ⟶ R such that
-- pullback.fst f g ≫ e = 0 and show that e = 0.
epi_of_cancel_zero _ fun {R} e h => by
-- Consider the morphism u := (e, 0) : X ⊞ Y ⟶ R.
let u :=
biprod.desc e
(0 : Y ⟶ R)
-- The composite pullback f g ⟶ X ⊞ Y ⟶ R is zero by assumption.
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 : (-g) ≫ d = 0 :=
calc
(-g) ≫ d = (biprod.inr ≫ biprod.desc f (-g)) ≫ d := by rw [biprod.inr_desc]
_ = biprod.inr ≫ u := by rw [Category.assoc, hd]
_ = 0 :=
biprod.inr_desc _
_
-- But g is an epimorphism, thus so is -g, so d = 0...
have : d = 0 :=
(cancel_epi (-g)).1
(by simpa)
-- ...or, in other words, e = 0.
calc
e = biprod.inl ≫ biprod.desc e (0 : Y ⟶ R) := by rw [biprod.inl_desc]
_ = biprod.inl ≫ biprod.desc f (-g) ≫ d := by rw [← hd]
_ = biprod.inl ≫ biprod.desc f (-g) ≫ 0 := by rw [this]
_ = (biprod.inl ≫ biprod.desc f (-g)) ≫ 0 := by rw [← Category.assoc]
_ = 0 := HasZeroMorphisms.comp_zero _ _
