English
A functor that preserves pushouts and binary coproducts also preserves coequalizers.
Русский
Функтор, сохраняющий пушауты и бинарные копроизведения, сохраняет коэквалайзеры.
LaTeX
$$$\text{PreservesColimitsOfShape WalkingParallelPair } G$$$
Lean4
/-- A functor that preserves pushouts and binary coproducts also presrves coequalizers. -/
theorem preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts [HasBinaryCoproducts C] [HasPushouts C]
[PreservesColimitsOfShape (Discrete WalkingPair) G] [PreservesColimitsOfShape WalkingSpan G] :
PreservesColimitsOfShape WalkingParallelPair G :=
⟨fun {K} =>
preservesColimit_of_preserves_colimit_cocone (coequalizerCoconeIsColimit K) <|
{ desc := fun c => by
refine (PreservesPushout.iso _ _ _).inv ≫ pushout.desc ?_ ?_ ?_
· exact c.ι.app WalkingParallelPair.one
· exact c.ι.app WalkingParallelPair.one
apply (mapIsColimitOfPreservesOfIsColimit G _ _ (coprodIsCoprod _ _)).hom_ext
rintro (_ | _)
· simp only [BinaryCofan.ι_app_left, BinaryCofan.mk_inl, ← G.map_comp_assoc, coprod.inl_desc]
· simp only [BinaryCofan.ι_app_right, BinaryCofan.mk_inr, ← G.map_comp_assoc, coprod.inr_desc]
exact (c.ι.naturality WalkingParallelPairHom.left).trans (c.ι.naturality WalkingParallelPairHom.right).symm
fac := fun c j =>
by
rcases j with (_ | _) <;>
simp only [Functor.mapCocone_ι_app, Cocone.ofCofork_ι, Category.id_comp, eqToHom_refl, Category.assoc,
Functor.map_comp, Cofork.ofπ_ι_app, pushout.inl_desc, PreservesPushout.inl_iso_inv_assoc]
exact (c.ι.naturality WalkingParallelPairHom.left).trans (Category.comp_id _)
uniq := fun s m h => by
rw [Iso.eq_inv_comp]
have := h WalkingParallelPair.one
dsimp [coequalizerCocone] at this
ext <;>
simp only [PreservesPushout.inl_iso_hom_assoc, Category.id_comp, pushout.inl_desc, pushout.inr_desc,
PreservesPushout.inr_iso_hom_assoc, ← pushoutInl_eq_pushout_inr, ← this] }⟩
