From cdb13984c07c6c90483670c9ef83eebde02e96f6 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Thu, 10 Dec 2020 17:02:33 +0000 Subject: [PATCH] feat(category_theory/limits): any functor preserves split coequalizers (#5246) Once #5230 merges, the only diff in this PR should be in `src/category_theory/limits/preserves/shapes/equalizers.lean` --- .../limits/preserves/shapes/equalizers.lean | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/category_theory/limits/preserves/shapes/equalizers.lean b/src/category_theory/limits/preserves/shapes/equalizers.lean index a68af7c7610b4..00d6dbb5f1182 100644 --- a/src/category_theory/limits/preserves/shapes/equalizers.lean +++ b/src/category_theory/limits/preserves/shapes/equalizers.lean @@ -3,7 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Bhavik Mehta -/ -import category_theory.limits.shapes.equalizers +import category_theory.limits.shapes.split_coequalizer import category_theory.limits.preserves.basic /-! @@ -179,6 +179,16 @@ begin apply_instance end +/-- Any functor preserves coequalizers of split pairs. -/ +@[priority 1] +instance preserves_split_coequalizers (f g : X ⟶ Y) [has_split_coequalizer f g] : + preserves_colimit (parallel_pair f g) G := +begin + apply preserves_colimit_of_preserves_colimit_cocone + ((has_split_coequalizer.is_split_coequalizer f g).is_coequalizer), + apply (is_colimit_map_cocone_cofork_equiv G _).symm + ((has_split_coequalizer.is_split_coequalizer f g).map G).is_coequalizer, +end end coequalizers end category_theory.limits