English
In an Abelian category, pushing out along a mono yields a mono on the corresponding inr map: mono_pushout_of_mono_f.
Русский
В абелевой категории, взятие пушаута вдоль моно-стрелки сохраняет моноc оставшейся стороны: моно pushout_inr.
LaTeX
$$$\\\\forall f,g \\\\in \\\\mathrm{Hom}, [Mono f] \\\\Rightarrow \\\\mathrm{Mono}(pushout.inr f g).$$$
Lean4
instance mono_pushout_of_mono_f [Mono f] : Mono (pushout.inr _ _ : Z ⟶ pushout f g) :=
mono_of_cancel_zero _ fun {R} e h => by
let u := biprod.lift (0 : R ⟶ Y) e
have hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0 := by simpa [u]
have := monoIsKernelOfCokernel _ (BiproductToPushoutIsCokernel.isColimitBiproductToPushout f g)
obtain ⟨d, hd⟩ := KernelFork.IsLimit.lift' this u hu
dsimp at d
dsimp [u] at hd
have : d ≫ f = 0 :=
calc
d ≫ f = d ≫ biprod.lift f (-g) ≫ biprod.fst := by rw [biprod.lift_fst]
_ = u ≫ biprod.fst := by rw [← Category.assoc, hd]
_ = 0 := biprod.lift_fst _ _
have : d = 0 := (cancel_mono f).1 (by simpa)
calc
e = biprod.lift (0 : R ⟶ Y) e ≫ biprod.snd := by rw [biprod.lift_snd]
_ = (d ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [← hd]
_ = (0 ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [this]
_ = 0 ≫ biprod.lift f (-g) ≫ biprod.snd := by rw [Category.assoc]
_ = 0 := zero_comp
