mathlib3 documentation

category_theory.limits.comma

Limits and colimits in comma categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We build limits in the comma category comma L R provided that the two source categories have limits and R preserves them. This is used to construct limits in the arrow category, structured arrow category and under category, and show that the appropriate forgetful functors create limits.

The duals of all the above are also given.

If R preserves the appropriate limit, then given a cone for F ⋙ fst L R : J ⥤ L and a limit cone for F ⋙ snd L R : J ⥤ R we can build a cone for F which will turn out to be a limit cone.

Equations

If L preserves the appropriate colimit, then given a colimit cocone for F ⋙ fst L R : J ⥤ L and a cocone for F ⋙ snd L R : J ⥤ R we can build a cocone for F which will turn out to be a colimit cocone.

Equations