mathlib3 documentation


Preserving (co)equalizers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Constructions to relate the notions of preserving (co)equalizers and reflecting (co)equalizers to concrete (co)forks.

In particular, we show that equalizer_comparison f g G is an isomorphism iff G preserves the limit of the parallel pair f,g, as well as the dual result.