mathlib documentation

category_theory.limits.preserves.shapes.equalizers

Preserving (co)equalizers #

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.