Preserving pullbacks #
Constructions to relate the notions of preserving pullbacks and reflecting pullbacks to concrete pullback cones.
In particular, we show that pullbackComparison G f g
is an isomorphism iff G
preserves
the pullback of f
and g
.
The dual is also given.
TODO #
- Generalise to wide pullbacks
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 PullbackCone.mk
with Functor.mapCone
.
Instances For
The property of preserving pullbacks expressed in terms of binary fans.
Instances For
The property of reflecting pullbacks expressed in terms of binary fans.
Instances For
If G
preserves pullbacks and C
has them, then the pullback cone constructed of the mapped
morphisms of the pullback cone is a limit.
Instances For
If F
preserves the pullback of f, g
, it also preserves the pullback of g, f
.
Instances For
If G
preserves the pullback of (f,g)
, then the pullback comparison map for G
at (f,g)
is
an isomorphism.
Instances For
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 PushoutCocone.mk
with Functor.mapCocone
.
Instances For
The property of preserving pushouts expressed in terms of binary cofans.
Instances For
The property of reflecting pushouts expressed in terms of binary cofans.
Instances For
If G
preserves pushouts and C
has them, then the pushout cocone constructed of the mapped
morphisms of the pushout cocone is a colimit.
Instances For
If F
preserves the pushout of f, g
, it also preserves the pushout of g, f
.
Instances For
If G
preserves the pushout of (f,g)
, then the pushout comparison map for G
at (f,g)
is
an isomorphism.
Instances For
If the pullback comparison map for G
at (f,g)
is an isomorphism, then G
preserves the
pullback of (f,g)
.
Instances For
If the pushout comparison map for G
at (f,g)
is an isomorphism, then G
preserves the
pushout of (f,g)
.