English
A functor preserving cokernels preserves coequalizers of morphisms.
Русский
Функтор, сохраняющий cokernels, сохраняет коэквалент (коэкал) морфизмов.
LaTeX
$$PreservesCoequalizers_of_preservesCokernels F$$
Lean4
/-- A functor between preadditive categories preserves the coequalizer of two
morphisms if it preserves all cokernels. -/
theorem preservesCoequalizer_of_preservesCokernels [∀ {X Y} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F]
{X Y : C} (f g : X ⟶ Y) : PreservesColimit (parallelPair f g) F :=
by
letI := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
haveI := additive_of_preservesBinaryBiproducts F
constructor
intro c i
let c' := isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
dsimp only [cokernelCoforkOfCofork_ofπ] at c'
let iFc := isColimitCoforkMapOfIsColimit' F _ c'
constructor
apply IsColimit.ofIsoColimit _ ((Cocones.functoriality _ F).mapIso (Cofork.isoCoforkOfπ c).symm)
apply (isColimitMapCoconeCoforkEquiv F (Cofork.condition c)).invFun
let p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
parallelPair.ext (Iso.refl _) (Iso.refl _) (by simp) (by simp)
exact
IsColimit.ofIsoColimit (isColimitCoforkOfCokernelCofork ((IsColimit.precomposeHomEquiv p.symm _).symm iFc))
(Cofork.ext (Iso.refl _) (by simp [p]))
