mathlib documentation

category_theory.limits.kan_extension

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.

def category_theory.Ran.diagram {S : Type v} {L : Type u₂} {D : Type u₃} [category_theory.category S] [category_theory.category L] [category_theory.category D] (ι : S L) (F : S D) (x : L) :

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

@[simp]
def category_theory.Ran.cone {S : Type v} {L : Type u₂} {D : Type u₃} [category_theory.category S] [category_theory.category L] [category_theory.category D] {ι : S L} {F : S D} {G : L D} (x : L) (f : ι G F) :

A cone over Ran.diagram ι F x used to define Ran.

Equations
def category_theory.Ran.loc {S : Type v} {L : Type u₂} {D : Type u₃} [category_theory.category S] [category_theory.category L] [category_theory.category D] (ι : S L) (F : S D) [∀ (x : L), category_theory.limits.has_limit (category_theory.Ran.diagram ι F x)] :
L D

An auxiliary definition used to define Ran.

Equations
def category_theory.Ran.equiv {S : Type v} {L : Type u₂} {D : Type u₃} [category_theory.category S] [category_theory.category L] [category_theory.category D] (ι : S L) (F : S D) [∀ (x : L), category_theory.limits.has_limit (category_theory.Ran.diagram ι F x)] (G : L D) :

An auxiliary definition used to define Ran and Ran.adjunction.

Equations
def category_theory.Ran {S : Type v} {L : Type u₂} {D : Type u₃} [category_theory.category S] [category_theory.category L] [category_theory.category D] (ι : S L) [∀ (X : L), category_theory.limits.has_limits_of_shape (category_theory.structured_arrow X ι) D] :
(S D) L D

The right Kan extension of a functor.

Equations
def category_theory.Lan.diagram {S : Type v} {L : Type u₂} {D : Type u₃} [category_theory.category S] [category_theory.category L] [category_theory.category D] (ι : S L) (F : S D) (x : L) :

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

@[simp]
def category_theory.Lan.cocone {S : Type v} {L : Type u₂} {D : Type u₃} [category_theory.category S] [category_theory.category L] [category_theory.category D] {ι : S L} {F : S D} {G : L D} (x : L) (f : F ι G) :

A cocone over Lan.diagram ι F x used to define Lan.

Equations
def category_theory.Lan.loc {S : Type v} {L : Type u₂} {D : Type u₃} [category_theory.category S] [category_theory.category L] [category_theory.category D] (ι : S L) (F : S D) [I : ∀ (x : L), category_theory.limits.has_colimit (category_theory.Lan.diagram ι F x)] :
L D

An auxiliary definition used to define Lan.

Equations
def category_theory.Lan.equiv {S : Type v} {L : Type u₂} {D : Type u₃} [category_theory.category S] [category_theory.category L] [category_theory.category D] (ι : S L) (F : S D) [I : ∀ (x : L), category_theory.limits.has_colimit (category_theory.Lan.diagram ι F x)] (G : L D) :

An auxiliary definition used to define Lan and Lan.adjunction.

Equations

The left Kan extension of a functor.

Equations