# mathlibdocumentation

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.

@[reducible]
def category_theory.Ran.diagram {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : 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 u₁} {L : Type u₂} {D : Type u₃} {ι : 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
noncomputable def category_theory.Ran.loc {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) (F : S D) [∀ (x : L), ] :
L D

An auxiliary definition used to define Ran.

Equations
@[simp]
theorem category_theory.Ran.loc_map {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) (F : S D) [∀ (x : L), ] (x y : L) (f : x y) :
@[simp]
theorem category_theory.Ran.loc_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) (F : S D) [∀ (x : L), ] (x : L) :
@[simp]
theorem category_theory.Ran.equiv_symm_apply_app {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) (F : S D) [∀ (x : L), ] (G : L D) (f : D).obj ι).obj G F) (x : L) :
( G).symm) f).app x =
noncomputable def category_theory.Ran.equiv {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) (F : S D) [∀ (x : L), ] (G : L D) :
(G D).obj ι).obj G F)

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

Equations
@[simp]
theorem category_theory.Ran.equiv_apply_app {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) (F : S D) [∀ (x : L), ] (G : L D) (f : G ) (x : S) :
@[simp]
theorem category_theory.Ran_obj_map {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) [∀ (X : L), ] (G : S D) (x y : L) (f : x y) :
noncomputable def category_theory.Ran {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) [∀ (X : L), ] :
(S D) L D

The right Kan extension of a functor.

Equations
@[simp]
theorem category_theory.Ran_obj_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) [∀ (X : L), ] (G : S D) (x : L) :
.obj G).obj x =
@[simp]
theorem category_theory.Ran_map_app {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) [∀ (X : L), ] (Y Y' : S D) (g : Y Y') (x : L) :
noncomputable def category_theory.Ran.adjunction {S : Type u₁} {L : Type u₂} (D : Type u₃) (ι : S L) [∀ (X : L), ] :

The adjunction associated to Ran.

Equations
theorem category_theory.Ran.reflective {S : Type u₁} {L : Type u₂} (D : Type u₃) (ι : S L) [∀ (X : L), ] :
@[reducible]
def category_theory.Lan.diagram {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : 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 u₁} {L : Type u₂} {D : Type u₃} {ι : 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
@[simp]
theorem category_theory.Lan.loc_map {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) (F : S D) [I : ∀ (x : L), ] (x y : L) (f : x y) :
@[simp]
theorem category_theory.Lan.loc_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) (F : S D) [I : ∀ (x : L), ] (x : L) :
noncomputable def category_theory.Lan.loc {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) (F : S D) [I : ∀ (x : L), ] :
L D

An auxiliary definition used to define Lan.

Equations
@[simp]
theorem category_theory.Lan.equiv_symm_apply_app {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) (F : S D) [I : ∀ (x : L), ] (G : L D) (f : F D).obj ι).obj G) (x : L) :
( G).symm) f).app x =
noncomputable def category_theory.Lan.equiv {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) (F : S D) [I : ∀ (x : L), ] (G : L D) :
G) (F D).obj ι).obj G)

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

Equations
@[simp]
theorem category_theory.Lan.equiv_apply_app {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) (F : S D) [I : ∀ (x : L), ] (G : L D) (f : G) (x : S) :
@[simp]
theorem category_theory.Lan_obj_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) [∀ (X : L), ] (F : S D) (x : L) :
.obj F).obj x =
@[simp]
theorem category_theory.Lan_map_app {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) [∀ (X : L), ] (X X' : S D) (f : X X') (x : L) :
noncomputable def category_theory.Lan {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) [∀ (X : L), ] :
(S D) L D

The left Kan extension of a functor.

Equations
Instances for category_theory.Lan
@[simp]
theorem category_theory.Lan_obj_map {S : Type u₁} {L : Type u₂} {D : Type u₃} (ι : S L) [∀ (X : L), ] (F : S D) (x y : L) (f : x y) :
noncomputable def category_theory.Lan.adjunction {S : Type u₁} {L : Type u₂} (D : Type u₃) (ι : S L) [∀ (X : L), ] :

The adjunction associated to Lan.

Equations
theorem category_theory.Lan.coreflective {S : Type u₁} {L : Type u₂} (D : Type u₃) (ι : S L) [∀ (X : L), ] :