The Kan extension functor

Given a functor L : C ⥤ D, we define the left Kan extension functor L.lan : (C ⥤ H) ⥤ (D ⥤ H) which sends a functor F : C ⥤ H to its left Kan extension along L. This is defined if all F have such a left Kan extension. It is shown that L.lan is the left adjoint to the functor (D ⥤ H) ⥤ (C ⥤ H) given by the precomposition with L (see Functor.lanAdjunction).

TODO

• dualize the results for right Kan extensions
• refactor the file CategoryTheory.Limits.KanExtension so that the definitions of Lan and Ran in that file (which rely on the existence of (co)limits) are replaced by the new definition Functor.lan which is based on Kan extensions API.

noncomputable def CategoryTheory.Functor.lan {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] : CategoryTheory.Functor (CategoryTheory.Functor C H) (CategoryTheory.Functor D H)

The left Kan extension functor (C ⥤ H) ⥤ (D ⥤ H) along a functor C ⥤ D.

Equations

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

noncomputable def CategoryTheory.Functor.lanUnit {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] : CategoryTheory.Functor.id (CategoryTheory.Functor C H) ⟶ L.lan.comp ((CategoryTheory.whiskeringLeft C D H).obj L)

The natural transformation F ⟶ L ⋙ (L.lan).obj G.

Equations

• L.lanUnit = { app := fun (F : CategoryTheory.Functor C H) => L.leftKanExtensionUnit F, naturality := ⋯ }

instance CategoryTheory.Functor.instIsLeftKanExtensionObjLanAppLanUnit {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] (F : CategoryTheory.Functor C H) : (L.lan.obj F).IsLeftKanExtension (L.lanUnit.app F)

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Functor.isPointwiseLeftKanExtensionLanUnit {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] : (CategoryTheory.Functor.LeftExtension.mk (L.lan.obj F) (L.lanUnit.app F)).IsPointwiseLeftKanExtension

If there exists a pointwise left Kan extension of F along L, then L.lan.obj G is a pointwise left Kan extension of F.

Equations

• L.isPointwiseLeftKanExtensionLanUnit F = CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension (L.lan.obj F) (L.lanUnit.app F)

noncomputable def CategoryTheory.Functor.lanAdjunction {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (H : Type u_3) [CategoryTheory.Category.{u_6, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] : L.lan ⊣ (CategoryTheory.whiskeringLeft C D H).obj L

The left Kan extension functor L.Lan is left adjoint to the precomposition by L.

Equations

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

@[simp]

theorem CategoryTheory.Functor.lanAdjunction_unit {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] (L : CategoryTheory.Functor C D) (H : Type u_3) [CategoryTheory.Category.{u_5, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] : (L.lanAdjunction H).unit = L.lanUnit

theorem CategoryTheory.Functor.lanAdjunction_counit_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_5, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] (G : CategoryTheory.Functor D H) : (L.lanAdjunction H).counit.app G = (L.lan.obj (L.comp G)).descOfIsLeftKanExtension (L.lanUnit.app (L.comp G)) G (CategoryTheory.CategoryStruct.id (L.comp G))

@[simp]

theorem CategoryTheory.Functor.lanUnit_app_whiskerLeft_lanAdjunction_counit_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_5, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] (G : CategoryTheory.Functor D H) {Z : CategoryTheory.Functor C H} (h : L.comp G ⟶ Z) : CategoryTheory.CategoryStruct.comp (L.lanUnit.app (L.comp G)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L ((L.lanAdjunction H).counit.app G)) h) = h

@[simp]

theorem CategoryTheory.Functor.lanUnit_app_whiskerLeft_lanAdjunction_counit_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_5, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] (G : CategoryTheory.Functor D H) : CategoryTheory.CategoryStruct.comp (L.lanUnit.app (L.comp G)) (CategoryTheory.whiskerLeft L ((L.lanAdjunction H).counit.app G)) = CategoryTheory.CategoryStruct.id (L.comp G)

@[simp]

theorem CategoryTheory.Functor.lanUnit_app_app_lanAdjunction_counit_app_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_5, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] (G : CategoryTheory.Functor D H) (X : C) {Z : H} (h : G.obj (L.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((L.lanUnit.app (L.comp G)).app X) (CategoryTheory.CategoryStruct.comp (((L.lanAdjunction H).counit.app G).app (L.obj X)) h) = h

@[simp]

theorem CategoryTheory.Functor.lanUnit_app_app_lanAdjunction_counit_app_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_5, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] (G : CategoryTheory.Functor D H) (X : C) : CategoryTheory.CategoryStruct.comp ((L.lanUnit.app (L.comp G)).app X) (((L.lanAdjunction H).counit.app G).app (L.obj X)) = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (CategoryTheory.Functor C H)).obj (L.comp G)).obj X)

theorem CategoryTheory.Functor.isIso_lanAdjunction_counit_app_iff {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_5, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] (G : CategoryTheory.Functor D H) : CategoryTheory.IsIso ((L.lanAdjunction H).counit.app G) ↔ G.IsLeftKanExtension (CategoryTheory.CategoryStruct.id (L.comp G))

instance CategoryTheory.Functor.instIsIsoAppLanUnit {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H) (X : C) [L.HasPointwiseLeftKanExtension F] : CategoryTheory.IsIso ((L.lanUnit.app F).app X)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instIsIsoAppLanUnit_1 {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] : CategoryTheory.IsIso (L.lanUnit.app F)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.coreflective {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] [L.Full] [L.Faithful] [∀ (F : CategoryTheory.Functor C H), L.HasPointwiseLeftKanExtension F] : CategoryTheory.IsIso L.lanUnit

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instIsIsoAppUnitLanAdjunctionOfHasPointwiseLeftKanExtension {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] : CategoryTheory.IsIso ((L.lanAdjunction H).unit.app F)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.coreflective' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] [L.Full] [L.Faithful] [∀ (F : CategoryTheory.Functor C H), L.HasPointwiseLeftKanExtension F] : CategoryTheory.IsIso (L.lanAdjunction H).unit

Equations

• ⋯ = ⋯