mathlib3 documentation

category_theory.limits.kan_extension

Kan extensions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

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₃} [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
noncomputable def category_theory.Ran.loc {S : Type u₁} {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
noncomputable def category_theory.Ran.equiv {S : Type u₁} {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

The right Kan extension of a functor.

Equations
@[reducible]

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₃} [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
noncomputable def category_theory.Lan.loc {S : Type u₁} {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
noncomputable def category_theory.Lan.equiv {S : Type u₁} {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