# Documentation

Mathlib.CategoryTheory.Limits.KanExtension

# 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]
abbrev CategoryTheory.Ran.diagram {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) (F : ) (x : L) :

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

Instances For
def CategoryTheory.Ran.cone {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] {ι : } {F : } {G : } (x : L) (f : ) :

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

Instances For
@[simp]
theorem CategoryTheory.Ran.loc_map {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) (F : ) [h : ∀ (x : L), ] {X : L} {Y : L} (f : X Y) :
@[simp]
theorem CategoryTheory.Ran.loc_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) (F : ) [h : ∀ (x : L), ] (x : L) :
().obj x =
def CategoryTheory.Ran.loc {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) (F : ) [h : ∀ (x : L), ] :

An auxiliary definition used to define Ran.

Instances For
@[simp]
theorem CategoryTheory.Ran.equiv_apply_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) (F : ) [h : ∀ (x : L), ] (G : ) (f : ) (x : S) :
(↑() f).app x = CategoryTheory.CategoryStruct.comp (f.app (ι.obj x)) (CategoryTheory.Limits.limit.π (CategoryTheory.Ran.diagram ι F (ι.obj x)) ())
@[simp]
theorem CategoryTheory.Ran.equiv_symm_apply_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) (F : ) [h : ∀ (x : L), ] (G : ) (f : (().obj ι).obj G F) (x : L) :
(().symm f).app x =
def CategoryTheory.Ran.equiv {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) (F : ) [h : ∀ (x : L), ] (G : ) :
() ((().obj ι).obj G F)

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

Instances For
@[simp]
theorem CategoryTheory.ran_obj_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) [∀ (X : L), ] (G : ) (x : L) :
(().obj G).obj x =
@[simp]
theorem CategoryTheory.ran_obj_map {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) [∀ (X : L), ] (G : ) {X : L} {Y : L} (f : X Y) :
(().obj G).map f =
@[simp]
theorem CategoryTheory.ran_map_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) [∀ (X : L), ] {Y : } {Y' : } (g : Y Y') (x : L) :
def CategoryTheory.ran {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) [∀ (X : L), ] :

The right Kan extension of a functor.

Instances For
def CategoryTheory.Ran.adjunction {S : Type u₁} {L : Type u₂} (D : Type u₃) [] [] [] (ι : ) [∀ (X : L), ] :
().obj ι

The adjunction associated to Ran.

Instances For
theorem CategoryTheory.Ran.reflective {S : Type u₁} {L : Type u₂} (D : Type u₃) [] [] [] (ι : ) [∀ (X : L), ] :
@[inline, reducible]
abbrev CategoryTheory.Lan.diagram {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) (F : ) (x : L) :

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

Instances For
def CategoryTheory.Lan.cocone {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] {ι : } {F : } {G : } (x : L) (f : ) :

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

Instances For
@[simp]
theorem CategoryTheory.Lan.loc_map {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) (F : ) [I : ∀ (x : L), ] {x : L} {y : L} (f : x y) :
@[simp]
theorem CategoryTheory.Lan.loc_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) (F : ) [I : ∀ (x : L), ] (x : L) :
().obj x =
def CategoryTheory.Lan.loc {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) (F : ) [I : ∀ (x : L), ] :

An auxiliary definition used to define Lan.

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

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

Instances For
@[simp]
theorem CategoryTheory.lan_obj_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) [] (F : ) (x : L) :
(().obj F).obj x =
@[simp]
theorem CategoryTheory.lan_obj_map {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) [] (F : ) {x : L} {y : L} (f : x y) :
(().obj F).map f =
@[simp]
theorem CategoryTheory.lan_map_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) [] {X : } {X' : } (f : X X') (x : L) :
def CategoryTheory.lan {S : Type u₁} {L : Type u₂} {D : Type u₃} [] [] [] (ι : ) [] :

The left Kan extension of a functor.

Instances For
def CategoryTheory.Lan.adjunction {S : Type u₁} {L : Type u₂} (D : Type u₃) [] [] [] (ι : ) [] :
().obj ι

The adjunction associated to Lan.

Instances For
theorem CategoryTheory.Lan.coreflective {S : Type u₁} {L : Type u₂} (D : Type u₃) [] [] [] (ι : ) [] :