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 #

The map of a pullback cone is a limit iff the fork consisting of the mapped morphisms is a limit. This essentially lets us commute pullback_cone.mk with functor.map_cone.

Equations

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

Equations

The map of a pushout cocone is a colimit iff the cofork consisting of the mapped morphisms is a colimit. This essentially lets us commute pushout_cocone.mk with functor.map_cocone.

Equations

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

Equations