mathlib documentation

category_theory.limits.preserves.shapes.pullbacks

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.

TODO #

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

Equations