Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-05 07:50 147a81a2

View on Github →

chore(category_theory/limits): preserving coequalizers (#5212) dualise stuff from before

Estimated changes

Modified src/category_theory/limits/preserves/shapes/equalizers.lean

added def category_theory.limits.is_colimit_cofork_map_of_is_colimit

added def category_theory.limits.is_colimit_map_cocone_cofork_equiv

added def category_theory.limits.is_colimit_of_has_coequalizer_of_preserves_colimit

added def category_theory.limits.is_colimit_of_is_colimit_cofork_map

added def category_theory.limits.of_iso_comparison

added def category_theory.limits.preserves_coequalizer.iso

added theorem category_theory.limits.preserves_coequalizer.iso_hom

Modified src/category_theory/limits/shapes/equalizers.lean