English
In an Abelian category, pushing out along a morphism g yields a mono on the corresponding inl map when g is mono.
Русский
В абелевой категории пушоут вдоль моно-стрелки g сохраняет моно на векторной части inl.
LaTeX
$$$\\\\forall f,g \\\\in \\\\mathrm{Hom}, [Mono g] \\\\Rightarrow \\\\mathrm{Mono}(pushout.inl f g).$$$
Lean4
instance mono_pushout_of_mono_g [Mono g] : Mono (pushout.inl f g) :=
mono_of_cancel_zero _ fun {R} e h => by
let u := biprod.lift e (0 : R ⟶ Z)
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 ≫ (-g) = 0 :=
calc
d ≫ (-g) = d ≫ biprod.lift f (-g) ≫ biprod.snd := by rw [biprod.lift_snd]
_ = biprod.lift e (0 : R ⟶ Z) ≫ biprod.snd := by rw [← Category.assoc, hd]
_ = 0 := biprod.lift_snd _ _
have : d = 0 := (cancel_mono (-g)).1 (by simpa)
calc
e = biprod.lift e (0 : R ⟶ Z) ≫ biprod.fst := by rw [biprod.lift_fst]
_ = (d ≫ biprod.lift f (-g)) ≫ biprod.fst := by rw [← hd]
_ = (0 ≫ biprod.lift f (-g)) ≫ biprod.fst := by rw [this]
_ = 0 ≫ biprod.lift f (-g) ≫ biprod.fst := by rw [Category.assoc]
_ = 0 := zero_comp
