# mathlibdocumentation

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.

## TODO #

• Dualise to pushouts
• Generalise to wide pullbacks
def category_theory.limits.is_limit_map_cone_pullback_cone_equiv {C : Type u₁} {D : Type u₂} (G : C D) {W X Y Z : C} {f : X Z} {g : Y Z} {h : W X} {k : W Y} (comm : h f = k g) :

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
def category_theory.limits.is_limit_pullback_cone_map_of_is_limit {C : Type u₁} {D : Type u₂} (G : C D) {W X Y Z : C} {f : X Z} {g : Y Z} {h : W X} {k : W Y} (comm : h f = k g)  :

The property of preserving pullbacks expressed in terms of binary fans.

Equations
def category_theory.limits.is_limit_of_is_limit_pullback_cone_map {C : Type u₁} {D : Type u₂} (G : C D) {W X Y Z : C} {f : X Z} {g : Y Z} {h : W X} {k : W Y} (comm : h f = k g) (l : category_theory.limits.is_limit (G.map k) _)) :

The property of reflecting pullbacks expressed in terms of binary fans.

Equations
def category_theory.limits.is_limit_of_has_pullback_of_preserves_limit {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} (f : X Z) (g : Y Z)  :

If G preserves pullbacks and C has them, then the pullback cone constructed of the mapped morphisms of the pullback cone is a limit.

Equations
def category_theory.limits.preserves_pullback.of_iso_comparison {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} (f : X Z) (g : Y Z) [ (G.map g)]  :

If the pullback comparison map for G at (f,g) is an isomorphism, then G preserves the pullback of (f,g).

Equations
def category_theory.limits.preserves_pullback.iso {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} (f : X Z) (g : Y Z) [ (G.map g)]  :
(G.map g)

If G preserves the pullback of (f,g), then the pullback comparison map for G at (f,g) is an isomorphism.

Equations
@[simp]
theorem category_theory.limits.preserves_pullback.iso_hom {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} (f : X Z) (g : Y Z) [ (G.map g)]  :
@[instance]
def category_theory.limits.pullback_comparison.category_theory.is_iso {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} (f : X Z) (g : Y Z) [ (G.map g)]  :