mathlib3
7f5a5ddd - feat(category_theory/limits): split coequalizers (#5230)

Commit
5 years ago
feat(category_theory/limits): split coequalizers (#5230) Define what it means for a triple of morphisms `f g : X ⟶ Y`, `π : Y ⟶ Z` to be a split coequalizer, and show that every split coequalizer is a coequalizer and absolute. Define split pairs and `G`-split pairs. These definitions and constructions are useful in particular for the monadicity theorems.
Author
Parents
Loading