Kan extensions #

This file defines the right and left Kan extensions of a functor. They exist under the assumption that the target category has enough limits resp. colimits.

The main definitions are Ran ι and Lan ι, where ι : S ⥤ L is a functor. Namely, Ran ι is the right Kan extension, while Lan ι is the left Kan extension, both as functors (S ⥤ D) ⥤ (L ⥤ D).

To access the right resp. left adjunction associated to these, use Ran.adjunction resp. Lan.adjunction.

Projects #

A lot of boilerplate could be generalized by defining and working with pseudofunctors.

@[inline, reducible]

The diagram indexed by Ran.index ι x used to define Ran.

Instances For
    @[inline, reducible]

    The diagram indexed by Lan.index ι x used to define Lan.

    Instances For