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).

Similarly, we define the right Kan extension functor L.ran : (C ⥤ H) ⥤ (D ⥤ H) which sends a functor F : C ⥤ H to its right Kan extension along L.

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_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] (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.lanObjObjIsoColimit {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] (X : D) : (L.lan.obj F).obj X ≅ CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L X).comp F)

If a left Kan extension is pointwise, then evaluating it at an object is isomorphic to taking a colimit.

Equations

• L.lanObjObjIsoColimit F X = (L.isPointwiseLeftKanExtensionLanUnit F X).isoColimit

@[simp]

theorem CategoryTheory.Functor.ι_lanObjObjIsoColimit_inv {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] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] (X : D) (f : CategoryTheory.CostructuredArrow L X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L X).comp F) f) (L.lanObjObjIsoColimit F X).inv = CategoryTheory.CategoryStruct.comp ((L.lanUnit.app F).app f.left) ((L.lan.obj F).map f.hom)

@[simp]

theorem CategoryTheory.Functor.ι_lanObjObjIsoColimit_inv_assoc {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] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] (X : D) (f : CategoryTheory.CostructuredArrow L X) {Z : H} (h : (L.lan.obj F).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L X).comp F) f) (CategoryTheory.CategoryStruct.comp (L.lanObjObjIsoColimit F X).inv h) = CategoryTheory.CategoryStruct.comp ((L.lanUnit.app F).app f.left) (CategoryTheory.CategoryStruct.comp ((L.lan.obj F).map f.hom) h)

@[simp]

theorem CategoryTheory.Functor.ι_lanObjObjIsoColimit_hom {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] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] (X : D) (f : CategoryTheory.CostructuredArrow L X) : CategoryTheory.CategoryStruct.comp ((L.lanUnit.app F).app f.left) (CategoryTheory.CategoryStruct.comp ((L.lan.obj F).map f.hom) (L.lanObjObjIsoColimit F X).hom) = CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L X).comp F) f

@[simp]

theorem CategoryTheory.Functor.ι_lanObjObjIsoColimit_hom_assoc {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] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] (X : D) (f : CategoryTheory.CostructuredArrow L X) {Z : H} (h : CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L X).comp F) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((L.lanUnit.app F).app f.left) (CategoryTheory.CategoryStruct.comp ((L.lan.obj F).map f.hom) (CategoryTheory.CategoryStruct.comp (L.lanObjObjIsoColimit F X).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L X).comp F) f) h

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 {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_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_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)

@[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

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))

noncomputable def CategoryTheory.Functor.lanCompColimIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) [∀ (G : CategoryTheory.Functor C H), L.HasLeftKanExtension G] [CategoryTheory.Limits.HasColimitsOfShape C H] [CategoryTheory.Limits.HasColimitsOfShape D H] : L.lan.comp CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.colim

Composing the left Kan extension of L : C ⥤ D with colim on shapes D is isomorphic to colim on shapes C.

Equations

• L.lanCompColimIso = (CategoryTheory.NatIso.ofComponents (fun (G : CategoryTheory.Functor C H) => ((L.lan.obj G).colimitIsoOfIsLeftKanExtension (L.lanUnit.app G)).symm) ⋯).symm

@[simp]

theorem CategoryTheory.Functor.lanCompColimIso_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) [∀ (G : CategoryTheory.Functor C H), L.HasLeftKanExtension G] [CategoryTheory.Limits.HasColimitsOfShape C H] [CategoryTheory.Limits.HasColimitsOfShape D H] (X : CategoryTheory.Functor C H) : L.lanCompColimIso.hom.app X = ((L.lan.obj X).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X)).hom

@[simp]

theorem CategoryTheory.Functor.lanCompColimIso_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) [∀ (G : CategoryTheory.Functor C H), L.HasLeftKanExtension G] [CategoryTheory.Limits.HasColimitsOfShape C H] [CategoryTheory.Limits.HasColimitsOfShape D H] (X : CategoryTheory.Functor C H) : L.lanCompColimIso.inv.app X = ((L.lan.obj X).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X)).inv

instance CategoryTheory.Functor.instIsIsoAppLanUnit {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] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H) (X : C) [L.HasPointwiseLeftKanExtension F] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension 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_6, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_5, u_3} H] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension 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_6, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_5, u_3} H] [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_6, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_5, u_3} H] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension 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_6, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{u_5, u_3} H] [L.Full] [L.Faithful] [∀ (F : CategoryTheory.Functor C H), L.HasPointwiseLeftKanExtension F] : CategoryTheory.IsIso (L.lanAdjunction H).unit

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Functor.ran {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.HasRightKanExtension F] : CategoryTheory.Functor (CategoryTheory.Functor C H) (CategoryTheory.Functor D H)

The right 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.ranCounit {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.HasRightKanExtension F] : L.ran.comp ((CategoryTheory.whiskeringLeft C D H).obj L) ⟶ CategoryTheory.Functor.id (CategoryTheory.Functor C H)

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

Equations

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

instance CategoryTheory.Functor.instIsRightKanExtensionObjRanAppRanCounit {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.HasRightKanExtension F] (F : CategoryTheory.Functor C H) : (L.ran.obj F).IsRightKanExtension (L.ranCounit.app F)

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Functor.isPointwiseRightKanExtensionRanCounit {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.HasRightKanExtension F] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] : (CategoryTheory.Functor.RightExtension.mk (L.ran.obj F) (L.ranCounit.app F)).IsPointwiseRightKanExtension

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

Equations

• L.isPointwiseRightKanExtensionRanCounit F = CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsRightKanExtension (L.ran.obj F) (L.ranCounit.app F)

noncomputable def CategoryTheory.Functor.ranObjObjIsoLimit {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.HasRightKanExtension F] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) : (L.ran.obj F).obj X ≅ CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj X L).comp F)

If a right Kan extension is pointwise, then evaluating it at an object is isomorphic to taking a limit.

Equations

• L.ranObjObjIsoLimit F X = (L.isPointwiseRightKanExtensionRanCounit F X).isoLimit

@[simp]

theorem CategoryTheory.Functor.ranObjObjIsoLimit_hom_π {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.HasRightKanExtension F] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) (f : CategoryTheory.StructuredArrow X L) : CategoryTheory.CategoryStruct.comp (L.ranObjObjIsoLimit F X).hom (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj X L).comp F) f) = CategoryTheory.CategoryStruct.comp ((L.ran.obj F).map f.hom) ((L.ranCounit.app F).app f.right)

@[simp]

theorem CategoryTheory.Functor.ranObjObjIsoLimit_hom_π_assoc {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.HasRightKanExtension F] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) (f : CategoryTheory.StructuredArrow X L) {Z : H} (h : F.obj ((CategoryTheory.StructuredArrow.proj X L).obj f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (L.ranObjObjIsoLimit F X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj X L).comp F) f) h) = CategoryTheory.CategoryStruct.comp ((L.ran.obj F).map f.hom) (CategoryTheory.CategoryStruct.comp ((L.ranCounit.app F).app f.right) h)

@[simp]

theorem CategoryTheory.Functor.ranObjObjIsoLimit_inv_π {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.HasRightKanExtension F] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) (f : CategoryTheory.StructuredArrow X L) : CategoryTheory.CategoryStruct.comp (L.ranObjObjIsoLimit F X).inv (CategoryTheory.CategoryStruct.comp ((L.ran.obj F).map f.hom) ((L.ranCounit.app F).app f.right)) = CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj X L).comp F) f

@[simp]

theorem CategoryTheory.Functor.ranObjObjIsoLimit_inv_π_assoc {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.HasRightKanExtension F] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) (f : CategoryTheory.StructuredArrow X L) {Z : H} (h : F.obj f.right ⟶ Z) : CategoryTheory.CategoryStruct.comp (L.ranObjObjIsoLimit F X).inv (CategoryTheory.CategoryStruct.comp ((L.ran.obj F).map f.hom) (CategoryTheory.CategoryStruct.comp ((L.ranCounit.app F).app f.right) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj X L).comp F) f) h

noncomputable def CategoryTheory.Functor.ranAdjunction {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.HasRightKanExtension F] : (CategoryTheory.whiskeringLeft C D H).obj L ⊣ L.ran

The right Kan extension functor L.ran is right adjoint to the precomposition by L.

Equations

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

@[simp]

theorem CategoryTheory.Functor.ranAdjunction_counit {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.HasRightKanExtension F] : (L.ranAdjunction H).counit = L.ranCounit

theorem CategoryTheory.Functor.ranAdjunction_unit_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.HasRightKanExtension F] (G : CategoryTheory.Functor D H) : (L.ranAdjunction H).unit.app G = (L.ran.obj (L.comp G)).liftOfIsRightKanExtension (L.ranCounit.app (L.comp G)) G (CategoryTheory.CategoryStruct.id (L.comp G))

@[simp]

theorem CategoryTheory.Functor.ranCounit_app_whiskerLeft_ranAdjunction_unit_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.HasRightKanExtension F] (G : CategoryTheory.Functor D H) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L ((L.ranAdjunction H).unit.app G)) (L.ranCounit.app (L.comp G)) = CategoryTheory.CategoryStruct.id (L.comp G)

@[simp]

theorem CategoryTheory.Functor.ranCounit_app_whiskerLeft_ranAdjunction_unit_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.HasRightKanExtension F] (G : CategoryTheory.Functor D H) {Z : CategoryTheory.Functor C H} (h : L.comp G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L ((L.ranAdjunction H).unit.app G)) (CategoryTheory.CategoryStruct.comp (L.ranCounit.app (L.comp G)) h) = h

@[simp]

theorem CategoryTheory.Functor.ranCounit_app_app_ranAdjunction_unit_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.HasRightKanExtension F] (G : CategoryTheory.Functor D H) (X : C) : CategoryTheory.CategoryStruct.comp (((L.ranAdjunction H).unit.app G).app (L.obj X)) ((L.ranCounit.app (L.comp G)).app X) = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (CategoryTheory.Functor D H)).obj G).obj (L.obj X))

@[simp]

theorem CategoryTheory.Functor.ranCounit_app_app_ranAdjunction_unit_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.HasRightKanExtension F] (G : CategoryTheory.Functor D H) (X : C) {Z : H} (h : G.obj (L.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (((L.ranAdjunction H).unit.app G).app (L.obj X)) (CategoryTheory.CategoryStruct.comp ((L.ranCounit.app (L.comp G)).app X) h) = h

theorem CategoryTheory.Functor.isIso_ranAdjunction_unit_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.HasRightKanExtension F] (G : CategoryTheory.Functor D H) : CategoryTheory.IsIso ((L.ranAdjunction H).unit.app G) ↔ G.IsRightKanExtension (CategoryTheory.CategoryStruct.id (L.comp G))

noncomputable def CategoryTheory.Functor.ranCompLimIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) [∀ (G : CategoryTheory.Functor C H), L.HasRightKanExtension G] [CategoryTheory.Limits.HasLimitsOfShape C H] [CategoryTheory.Limits.HasLimitsOfShape D H] : L.ran.comp CategoryTheory.Limits.lim ≅ CategoryTheory.Limits.lim

Composing the right Kan extension of L : C ⥤ D with lim on shapes D is isomorphic to lim on shapes C.

Equations

• L.ranCompLimIso = CategoryTheory.NatIso.ofComponents (fun (G : CategoryTheory.Functor C H) => (L.ran.obj G).limitIsoOfIsRightKanExtension (L.ranCounit.app G)) ⋯

@[simp]

theorem CategoryTheory.Functor.ranCompLimIso_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) [∀ (G : CategoryTheory.Functor C H), L.HasRightKanExtension G] [CategoryTheory.Limits.HasLimitsOfShape C H] [CategoryTheory.Limits.HasLimitsOfShape D H] (X : CategoryTheory.Functor C H) : L.ranCompLimIso.hom.app X = ((L.ran.obj X).limitIsoOfIsRightKanExtension (L.ranCounit.app X)).hom

@[simp]

theorem CategoryTheory.Functor.ranCompLimIso_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {H : Type u_3} [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) [∀ (G : CategoryTheory.Functor C H), L.HasRightKanExtension G] [CategoryTheory.Limits.HasLimitsOfShape C H] [CategoryTheory.Limits.HasLimitsOfShape D H] (X : CategoryTheory.Functor C H) : L.ranCompLimIso.inv.app X = ((L.ran.obj X).limitIsoOfIsRightKanExtension (L.ranCounit.app X)).inv

instance CategoryTheory.Functor.instIsIsoAppRanCounit {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] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H) (X : C) [L.HasPointwiseRightKanExtension F] [∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] : CategoryTheory.IsIso ((L.ranCounit.app F).app X)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instIsIsoAppRanCounit_1 {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] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] [∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] : CategoryTheory.IsIso (L.ranCounit.app F)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.reflective {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] [L.Full] [L.Faithful] [∀ (F : CategoryTheory.Functor C H), L.HasPointwiseRightKanExtension F] : CategoryTheory.IsIso L.ranCounit

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension {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] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] [∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] : CategoryTheory.IsIso ((L.ranAdjunction H).counit.app F)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.reflective' {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] [L.Full] [L.Faithful] [∀ (F : CategoryTheory.Functor C H), L.HasPointwiseRightKanExtension F] : CategoryTheory.IsIso (L.ranAdjunction H).counit

Equations

• ⋯ = ⋯