mathlib3 documentation


Preserving pullbacks #

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

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.