mathlib3 documentation

category_theory.limits.full_subcategory

Limits in full subcategories #

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

We introduce the notion of a property closed under taking limits and show that if P is closed under taking limits, then limits in full_subcategory P can be constructed from limits in C. More precisely, the inclusion creates such limits.

We say that a property is closed under limits of shape J if whenever all objects in a J-shaped diagram have the property, any limit of this diagram also has the property.

Equations

We say that a property is closed under colimits of shape J if whenever all objects in a J-shaped diagram have the property, any colimit of this diagram also has the property.

Equations