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 G f is an isomorphism iff G preserves the limit of f as well as the dual.