Structures · Category theory

CategoryTheory.CreatesLimit

Definition 3.3.1 of [Riehl]. We say that F creates limits of K if, given any limit cone c for K ⋙ F (i.e. below) we can lift it to a cone "above", and further that F reflects limits for K. If F reflects isomorphisms, it suffices to show only that the lifted cone is a limit - see createsLimitOfReflectsIso.

Defined in

Mathlib.CategoryTheory.Limits.Creates

Shape

2 explicit arguments · adds lifts