mathlib documentation


Preserving pullbacks #

Constructions to relate the notions of preserving pullbacks and reflecting pullbacks to concrete pullback cones.

In particular, we show that pullback_comparison G f g is an isomorphism iff G preserves the pullback of f and g.

The dual is also given.


If F preserves the pushout of f, g, it also preserves the pushout of g, f.