Right Kan extensions

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

The main definition is Ran ι, where ι : S ⥤ L is a functor. Namely, Ran ι : (S ⥤ D) ⥤ (L ⥤ D) is the right Kan extension.

To access the adjunction associated to this, use Ran.adjunction.

TODO

• refactor Ran so that it relies on the general API for Kan extensions of functors, similarly as the left Kan extension adjunction is defined in CategoryTheory.Functor.KanExtension.Adjunction.

Projects

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

@[reducible, inline]

abbrev CategoryTheory.Ran.diagram {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) (x : L) : CategoryTheory.Functor (CategoryTheory.StructuredArrow x ι) D

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

Equations

• CategoryTheory.Ran.diagram ι F x = (CategoryTheory.StructuredArrow.proj x ι).comp F

def CategoryTheory.Ran.cone {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] {ι : CategoryTheory.Functor S L} {F : CategoryTheory.Functor S D} {G : CategoryTheory.Functor L D} (x : L) (f : ι.comp G ⟶ F) : CategoryTheory.Limits.Cone (CategoryTheory.Ran.diagram ι F x)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Ran.loc_map {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [h : ∀ (x : L), CategoryTheory.Limits.HasLimit (CategoryTheory.Ran.diagram ι F x)] {X : L} {Y : L} (f : X ⟶ Y) : (CategoryTheory.Ran.loc ι F).map f = CategoryTheory.Limits.limit.pre (CategoryTheory.Ran.diagram ι F X) (CategoryTheory.StructuredArrow.map f)

@[simp]

theorem CategoryTheory.Ran.loc_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [h : ∀ (x : L), CategoryTheory.Limits.HasLimit (CategoryTheory.Ran.diagram ι F x)] (x : L) : (CategoryTheory.Ran.loc ι F).obj x = CategoryTheory.Limits.limit (CategoryTheory.Ran.diagram ι F x)

def CategoryTheory.Ran.loc {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [h : ∀ (x : L), CategoryTheory.Limits.HasLimit (CategoryTheory.Ran.diagram ι F x)] : CategoryTheory.Functor L D

An auxiliary definition used to define Ran.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Ran.equiv_apply_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [h : ∀ (x : L), CategoryTheory.Limits.HasLimit (CategoryTheory.Ran.diagram ι F x)] (G : CategoryTheory.Functor L D) (f : G ⟶ CategoryTheory.Ran.loc ι F) (x : S) : ((CategoryTheory.Ran.equiv ι F G) f).app x = CategoryTheory.CategoryStruct.comp (f.app (ι.obj x)) (CategoryTheory.Limits.limit.π (CategoryTheory.Ran.diagram ι F (ι.obj x)) (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (ι.obj x))))

@[simp]

theorem CategoryTheory.Ran.equiv_symm_apply_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [h : ∀ (x : L), CategoryTheory.Limits.HasLimit (CategoryTheory.Ran.diagram ι F x)] (G : CategoryTheory.Functor L D) (f : ((CategoryTheory.whiskeringLeft S L D).obj ι).obj G ⟶ F) (x : L) : ((CategoryTheory.Ran.equiv ι F G).symm f).app x = CategoryTheory.Limits.limit.lift (CategoryTheory.Ran.diagram ι F x) (CategoryTheory.Ran.cone x f)

def CategoryTheory.Ran.equiv {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) (F : CategoryTheory.Functor S D) [h : ∀ (x : L), CategoryTheory.Limits.HasLimit (CategoryTheory.Ran.diagram ι F x)] (G : CategoryTheory.Functor L D) : (G ⟶ CategoryTheory.Ran.loc ι F) ≃ (((CategoryTheory.whiskeringLeft S L D).obj ι).obj G ⟶ F)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ran_map_app {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (X : L), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X ι) D] {Y : CategoryTheory.Functor S D} {Y' : CategoryTheory.Functor S D} (g : Y ⟶ Y') (x : L) : ((CategoryTheory.ran ι).map g).app x = CategoryTheory.Limits.limit.lift (CategoryTheory.Ran.diagram ι Y' x) { pt := CategoryTheory.Limits.limit (CategoryTheory.Ran.diagram ι Y x), π := { app := fun (i : CategoryTheory.StructuredArrow x ι) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.pre (CategoryTheory.Ran.diagram ι Y x) (CategoryTheory.StructuredArrow.map i.hom)) (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Ran.equiv ι Y (CategoryTheory.Ran.loc ι Y)) (CategoryTheory.CategoryStruct.id (CategoryTheory.Ran.loc ι Y))).app i.right) (g.app i.right)), naturality := ⋯ } }

@[simp]

theorem CategoryTheory.ran_obj_obj {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (X : L), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X ι) D] (G : CategoryTheory.Functor S D) (x : L) : ((CategoryTheory.ran ι).obj G).obj x = CategoryTheory.Limits.limit (CategoryTheory.Ran.diagram ι G x)

@[simp]

theorem CategoryTheory.ran_obj_map {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (X : L), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X ι) D] (G : CategoryTheory.Functor S D) {X : L} {Y : L} (f : X ⟶ Y) : ((CategoryTheory.ran ι).obj G).map f = CategoryTheory.Limits.limit.pre (CategoryTheory.Ran.diagram ι G X) (CategoryTheory.StructuredArrow.map f)

def CategoryTheory.ran {S : Type u₁} {L : Type u₂} {D : Type u₃} [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (X : L), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X ι) D] : CategoryTheory.Functor (CategoryTheory.Functor S D) (CategoryTheory.Functor L D)

The right Kan extension of a functor.

Equations

• CategoryTheory.ran ι = CategoryTheory.Adjunction.rightAdjointOfEquiv (fun (F : CategoryTheory.Functor L D) (G : CategoryTheory.Functor S D) => (CategoryTheory.Ran.equiv ι G F).symm) ⋯

def CategoryTheory.Ran.adjunction {S : Type u₁} {L : Type u₂} (D : Type u₃) [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [∀ (X : L), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X ι) D] : (CategoryTheory.whiskeringLeft S L D).obj ι ⊣ CategoryTheory.ran ι

The adjunction associated to Ran.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Ran.reflective {S : Type u₁} {L : Type u₂} (D : Type u₃) [CategoryTheory.Category.{v₁, u₁} S] [CategoryTheory.Category.{v₂, u₂} L] [CategoryTheory.Category.{v₃, u₃} D] (ι : CategoryTheory.Functor S L) [ι.Full] [ι.Faithful] [∀ (X : L), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X ι) D] : CategoryTheory.IsIso (CategoryTheory.Ran.adjunction D ι).counit