mathlib

mathlib copied to clipboard

Following on from #6820 and the discussion in https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/Simplicial.20stuff.

We have a construction for Kan extensions from the existence of certain (co)limits over (co)structured arrow categories, but Kan extensions can still exist (and can be talked about) without the assumption that any limits exist, see eg https://ncatlab.org/nlab/show/Kan+extension#LocalKanExtensions or https://ncatlab.org/nlab/show/Kan+extension#pointwiseVsWeak. To this end, it could be useful to have a structure is_left_Kan_extension similar to is_limit which expresses that a functor and its natural transformation satisfy the property of a left Kan extension, and a (Prop-valued) class has_left_Kan_extension expressing that such a functor and transformation exist. From here, the existing constructions in terms of limits can be used to give instances asserting that certain Kan extensions exist provided the relevant limits exist.