Documentation

Mathlib.CategoryTheory.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 pullbackComparison G f g is an isomorphism iff G preserves the pullback of f and g.

The dual is also given.

TODO #

@[reducible, inline]

The image of a pullback cone by a functor.

Equations

The map (as a cone) of a pullback cone is limit iff the map (as a pullback cone) is limit.

Equations
  • One or more equations did not get rendered due to their size.

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.

Equations

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

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.
def CategoryTheory.Limits.PullbackCone.isLimitCoyonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) (c : CategoryTheory.Limits.PullbackCone f g) :
CategoryTheory.Limits.IsLimit c ((X_1 : Cᵒᵖ) → CategoryTheory.Limits.IsLimit (c.map (CategoryTheory.coyoneda.obj X_1)))

A pullback cone in C is limit iff if it is so after the application of coyoneda.obj X for all X : Cᵒᵖ.

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

The image of a pullback cone by a functor.

Equations

The map (as a cocone) of a pushout cocone is colimit iff the map (as a pushout cocone) is limit.

Equations
  • One or more equations did not get rendered due to their size.

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.

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.
def CategoryTheory.Limits.PushoutCocone.isColimitYonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (c : CategoryTheory.Limits.PushoutCocone f g) :
CategoryTheory.Limits.IsColimit c ((X_1 : C) → CategoryTheory.Limits.IsLimit (c.op.map (CategoryTheory.yoneda.obj X_1)))

A pushout cocone in C is colimit iff it becomes limit after the application of yoneda.obj X for all X : C.

Equations
  • One or more equations did not get rendered due to their size.