Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-19 19:33 f1200764

View on Github →

feat(category_theory): (co)equalizers and (co)kernels when composing with monos/epis (#12828)

Estimated changes

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

added theorem category_theory.limits.has_coequalizer_epi_comp

added theorem category_theory.limits.has_equalizer_comp_mono

added def category_theory.limits.is_coequalizer_epi_comp

added def category_theory.limits.is_equalizer_comp_mono

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

added def category_theory.limits.is_cokernel_epi_comp

added def category_theory.limits.is_kernel_comp_mono