Documentation

Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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.

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

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

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

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

      Equations
        Instances For
          source
          instance CategoryTheory.Functor.instIsLeftKanExtensionObjLanAppLanUnit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasLeftKanExtension F] (F : Functor C H) :
          (L.lan.obj F).IsLeftKanExtension (L.lanUnit.app F)
          source
          noncomputable def CategoryTheory.Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] :
          (LeftExtension.mk (L.leftKanExtension F) (L.leftKanExtensionUnit 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
            Instances For
              source
              noncomputable def CategoryTheory.Functor.leftKanExtensionObjIsoColimit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] [L.HasLeftKanExtension F] (X : D) :
              (L.leftKanExtension F).obj X ≅ Limits.colimit ((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
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_inv {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] [L.HasLeftKanExtension F] (X : D) (f : CostructuredArrow L X) :
                  CategoryStruct.comp (Limits.colimit.ι ((CostructuredArrow.proj L X).comp F) f) (L.leftKanExtensionObjIsoColimit F X).inv = CategoryStruct.comp ((L.leftKanExtensionUnit F).app f.left) ((L.leftKanExtension F).map f.hom)
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_inv_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] [L.HasLeftKanExtension F] (X : D) (f : CostructuredArrow L X) {Z : H} (h : (L.leftKanExtension F).obj X ⟶ Z) :
                  CategoryStruct.comp (Limits.colimit.ι ((CostructuredArrow.proj L X).comp F) f) (CategoryStruct.comp (L.leftKanExtensionObjIsoColimit F X).inv h) = CategoryStruct.comp ((L.leftKanExtensionUnit F).app f.left) (CategoryStruct.comp ((L.leftKanExtension F).map f.hom) h)
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_hom {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] (X : D) (f : CostructuredArrow L X) :
                  CategoryStruct.comp ((L.leftKanExtensionUnit F).app f.left) (CategoryStruct.comp ((L.leftKanExtension F).map f.hom) (L.leftKanExtensionObjIsoColimit F X).hom) = Limits.colimit.ι ((CostructuredArrow.proj L X).comp F) f
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_hom_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] (X : D) (f : CostructuredArrow L X) {Z : H} (h : Limits.colimit ((CostructuredArrow.proj L X).comp F) ⟶ Z) :
                  CategoryStruct.comp ((L.leftKanExtensionUnit F).app f.left) (CategoryStruct.comp ((L.leftKanExtension F).map f.hom) (CategoryStruct.comp (L.leftKanExtensionObjIsoColimit F X).hom h)) = CategoryStruct.comp (Limits.colimit.ι ((CostructuredArrow.proj L X).comp F) f) h
                  source
                  theorem CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] (X : D) (f : CostructuredArrow L X) :
                  CategoryStruct.comp ((L.leftKanExtensionUnit F).app f.left) (CategoryStruct.comp ((L.leftKanExtension F).map f.hom) (L.leftKanExtensionObjIsoColimit F X).hom) = Limits.colimit.ι ((CostructuredArrow.proj L X).comp F) f
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_4, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] (X : C) :
                  CategoryStruct.comp ((L.leftKanExtensionUnit F).app X) (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom = Limits.colimit.ι ((CostructuredArrow.proj L (L.obj X)).comp F) (CostructuredArrow.mk (CategoryStruct.id (L.obj X)))
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom_assoc {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_4, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] (X : C) {Z : H} (h : Limits.colimit ((CostructuredArrow.proj L (L.obj X)).comp F) ⟶ Z) :
                  CategoryStruct.comp ((L.leftKanExtensionUnit F).app X) (CategoryStruct.comp (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom h) = CategoryStruct.comp (Limits.colimit.ι ((CostructuredArrow.proj L (L.obj X)).comp F) (CostructuredArrow.mk (CategoryStruct.id (L.obj X)))) h
                  source
                  instance CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] {X Y : D} (f : X ⟶ Y) :
                  Limits.HasColimit (comp ((CostructuredArrow.functor L).map f) ((Grothendieck.ι (CostructuredArrow.functor L) Y).comp ((CostructuredArrow.grothendieckProj L).comp F)))
                  source
                  @[deprecated CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj (since := "2025-07-27")]
                  theorem CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grotendieckProj {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] {X Y : D} (f : X ⟶ Y) :
                  Limits.HasColimit (comp ((CostructuredArrow.functor L).map f) ((Grothendieck.ι (CostructuredArrow.functor L) Y).comp ((CostructuredArrow.grothendieckProj L).comp F)))

                  Alias of CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj.

                  source
                  noncomputable def CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] [L.HasLeftKanExtension F] :
                  L.leftKanExtension F ≅ Limits.fiberwiseColimit ((CostructuredArrow.grothendieckProj L).comp F)

                  The left Kan extension of F : C ⥤ H along a functor L : C ⥤ D is isomorphic to the fiberwise colimit of the projection functor on the Grothendieck construction of the costructured arrow category composed with F.

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] [L.HasLeftKanExtension F] (X : D) :
                      (L.leftKanExtensionIsoFiberwiseColimit F).hom.app X = CategoryStruct.comp (L.leftKanExtensionObjIsoColimit F X).hom (Limits.HasColimit.isoOfNatIso (isoWhiskerRight (CostructuredArrow.ιCompGrothendieckProj L X) F)).inv
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] [L.HasLeftKanExtension F] (X : D) :
                      (L.leftKanExtensionIsoFiberwiseColimit F).inv.app X = CategoryStruct.comp (Limits.HasColimit.isoOfNatIso (isoWhiskerRight (CostructuredArrow.ιCompGrothendieckProj L X) F)).hom (L.leftKanExtensionObjIsoColimit F X).inv
                      source
                      noncomputable def CategoryTheory.Functor.lanAdjunction {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) (H : Type u_3) [Category.{u_6, u_3} H] [∀ (F : Functor C H), L.HasLeftKanExtension F] :
                      L.lan ⊣ (whiskeringLeft C D H).obj L

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

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.Functor.lanAdjunction_unit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) (H : Type u_3) [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasLeftKanExtension F] :
                          (L.lanAdjunction H).unit = L.lanUnit
                          source
                          theorem CategoryTheory.Functor.lanAdjunction_counit_app {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasLeftKanExtension F] (G : Functor D H) :
                          (L.lanAdjunction H).counit.app G = (L.lan.obj (L.comp G)).descOfIsLeftKanExtension (L.lanUnit.app (L.comp G)) G (CategoryStruct.id (L.comp G))
                          source
                          @[simp]
                          theorem CategoryTheory.Functor.lanUnit_app_whiskerLeft_lanAdjunction_counit_app {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasLeftKanExtension F] (G : Functor D H) :
                          CategoryStruct.comp (L.lanUnit.app (L.comp G)) (L.whiskerLeft ((L.lanAdjunction H).counit.app G)) = CategoryStruct.id (L.comp G)
                          source
                          @[simp]
                          theorem CategoryTheory.Functor.lanUnit_app_whiskerLeft_lanAdjunction_counit_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasLeftKanExtension F] (G : Functor D H) {Z : Functor C H} (h : L.comp G ⟶ Z) :
                          CategoryStruct.comp (L.lanUnit.app (L.comp G)) (CategoryStruct.comp (L.whiskerLeft ((L.lanAdjunction H).counit.app G)) h) = h
                          source
                          @[simp]
                          theorem CategoryTheory.Functor.lanUnit_app_app_lanAdjunction_counit_app_app {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasLeftKanExtension F] (G : Functor D H) (X : C) :
                          CategoryStruct.comp ((L.lanUnit.app (L.comp G)).app X) (((L.lanAdjunction H).counit.app G).app (L.obj X)) = CategoryStruct.id (((Functor.id (Functor C H)).obj (L.comp G)).obj X)
                          source
                          @[simp]
                          theorem CategoryTheory.Functor.lanUnit_app_app_lanAdjunction_counit_app_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasLeftKanExtension F] (G : Functor D H) (X : C) {Z : H} (h : G.obj (L.obj X) ⟶ Z) :
                          CategoryStruct.comp ((L.lanUnit.app (L.comp G)).app X) (CategoryStruct.comp (((L.lanAdjunction H).counit.app G).app (L.obj X)) h) = h
                          source
                          theorem CategoryTheory.Functor.isIso_lanAdjunction_counit_app_iff {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasLeftKanExtension F] (G : Functor D H) :
                          IsIso ((L.lanAdjunction H).counit.app G) ↔ G.IsLeftKanExtension (CategoryStruct.id (L.comp G))
                          source
                          noncomputable def CategoryTheory.Functor.lanCompColimIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] [∀ (F : Functor C H), L.HasLeftKanExtension F] [Limits.HasColimitsOfShape C H] [Limits.HasColimitsOfShape D H] :
                          L.lan.comp Limits.colim ≅ Limits.colim

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

                          Equations
                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.Functor.lanCompColimIso_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] [∀ (F : Functor C H), L.HasLeftKanExtension F] [Limits.HasColimitsOfShape C H] [Limits.HasColimitsOfShape D H] (X : Functor C H) :
                              L.lanCompColimIso.hom.app X = ((L.lan.obj X).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X)).hom
                              source
                              @[simp]
                              theorem CategoryTheory.Functor.lanCompColimIso_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] [∀ (F : Functor C H), L.HasLeftKanExtension F] [Limits.HasColimitsOfShape C H] [Limits.HasColimitsOfShape D H] (X : Functor C H) :
                              L.lanCompColimIso.inv.app X = ((L.lan.obj X).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X)).inv
                              source
                              instance CategoryTheory.Functor.instHasColimitGrothendieckFunctorCompGrothendieckProj {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (G : Functor C H) [L.HasPointwiseLeftKanExtension G] [Limits.HasColimitsOfShape D H] :
                              Limits.HasColimit ((CostructuredArrow.grothendieckProj L).comp G)
                              source
                              noncomputable def CategoryTheory.Functor.colimitIsoColimitGrothendieck {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (G : Functor C H) [L.HasPointwiseLeftKanExtension G] [Limits.HasColimitsOfShape D H] [Limits.HasColimitsOfShape C H] :
                              Limits.colimit G ≅ Limits.colimit ((CostructuredArrow.grothendieckProj L).comp G)

                              If G : C ⥤ H admits a left Kan extension along a functor L : C ⥤ D and H has colimits of shape C and D, then the colimit of G is isomorphic to the colimit of a canonical functor Grothendieck (CostructuredArrow.functor L) ⥤ H induced by L and G.

                              Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (G : Functor C H) [L.HasPointwiseLeftKanExtension G] [Limits.HasColimitsOfShape D H] [Limits.HasColimitsOfShape C H] (X : Grothendieck (CostructuredArrow.functor L)) :
                                  CategoryStruct.comp (Limits.colimit.ι ((CostructuredArrow.grothendieckProj L).comp G) X) (L.colimitIsoColimitGrothendieck G).inv = Limits.colimit.ι G ((CostructuredArrow.proj L X.base).obj X.fiber)
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv_assoc {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] (G : Functor C H) [L.HasPointwiseLeftKanExtension G] [Limits.HasColimitsOfShape D H] [Limits.HasColimitsOfShape C H] (X : Grothendieck (CostructuredArrow.functor L)) {Z : H} (h : Limits.colimit G ⟶ Z) :
                                  CategoryStruct.comp (Limits.colimit.ι ((CostructuredArrow.grothendieckProj L).comp G) X) (CategoryStruct.comp (L.colimitIsoColimitGrothendieck G).inv h) = CategoryStruct.comp (Limits.colimit.ι G ((CostructuredArrow.proj L X.base).obj X.fiber)) h
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_4, u_3} H] (G : Functor C H) [L.HasPointwiseLeftKanExtension G] [Limits.HasColimitsOfShape D H] [Limits.HasColimitsOfShape C H] (X : C) :
                                  CategoryStruct.comp (Limits.colimit.ι G X) (L.colimitIsoColimitGrothendieck G).hom = Limits.colimit.ι ((CostructuredArrow.grothendieckProj L).comp G) { base := L.obj X, fiber := CostructuredArrow.mk (CategoryStruct.id (L.obj X)) }
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom_assoc {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_4, u_3} H] (G : Functor C H) [L.HasPointwiseLeftKanExtension G] [Limits.HasColimitsOfShape D H] [Limits.HasColimitsOfShape C H] (X : C) {Z : H} (h : Limits.colimit ((CostructuredArrow.grothendieckProj L).comp G) ⟶ Z) :
                                  CategoryStruct.comp (Limits.colimit.ι G X) (CategoryStruct.comp (L.colimitIsoColimitGrothendieck G).hom h) = CategoryStruct.comp (Limits.colimit.ι ((CostructuredArrow.grothendieckProj L).comp G) { base := L.obj X, fiber := CostructuredArrow.mk (CategoryStruct.id (L.obj X)) }) h
                                  source
                                  instance CategoryTheory.Functor.instIsIsoAppLanUnit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [L.Full] [L.Faithful] (F : Functor C H) (X : C) [L.HasPointwiseLeftKanExtension F] [∀ (F : Functor C H), L.HasLeftKanExtension F] :
                                  IsIso ((L.lanUnit.app F).app X)
                                  source
                                  instance CategoryTheory.Functor.instIsIsoAppLanUnit_1 {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [L.Full] [L.Faithful] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] [∀ (F : Functor C H), L.HasLeftKanExtension F] :
                                  IsIso (L.lanUnit.app F)
                                  source
                                  instance CategoryTheory.Functor.coreflective {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [L.Full] [L.Faithful] [∀ (F : Functor C H), L.HasPointwiseLeftKanExtension F] :
                                  IsIso L.lanUnit
                                  source
                                  instance CategoryTheory.Functor.instIsIsoAppUnitLanAdjunctionOfHasPointwiseLeftKanExtension {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [L.Full] [L.Faithful] (F : Functor C H) [L.HasPointwiseLeftKanExtension F] [∀ (F : Functor C H), L.HasLeftKanExtension F] :
                                  IsIso ((L.lanAdjunction H).unit.app F)
                                  source
                                  instance CategoryTheory.Functor.coreflective' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [L.Full] [L.Faithful] [∀ (F : Functor C H), L.HasPointwiseLeftKanExtension F] :
                                  IsIso (L.lanAdjunction H).unit
                                  source
                                  noncomputable def CategoryTheory.Functor.ran {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] :
                                  Functor (Functor C H) (Functor D H)

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

                                  Equations
                                    Instances For
                                      source
                                      noncomputable def CategoryTheory.Functor.ranCounit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] :
                                      L.ran.comp ((whiskeringLeft C D H).obj L) ⟶ Functor.id (Functor C H)

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

                                      Equations
                                        Instances For
                                          source
                                          instance CategoryTheory.Functor.instIsRightKanExtensionObjRanAppRanCounit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (F : Functor C H) :
                                          (L.ran.obj F).IsRightKanExtension (L.ranCounit.app F)
                                          source
                                          noncomputable def CategoryTheory.Functor.isPointwiseRightKanExtensionRanCounit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (F : Functor C H) [L.HasPointwiseRightKanExtension F] :
                                          (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
                                            Instances For
                                              source
                                              noncomputable def CategoryTheory.Functor.ranObjObjIsoLimit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_6, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (F : Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) :
                                              (L.ran.obj F).obj X ≅ Limits.limit ((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
                                                Instances For
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.ranObjObjIsoLimit_hom_π {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (F : Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) (f : StructuredArrow X L) :
                                                  CategoryStruct.comp (L.ranObjObjIsoLimit F X).hom (Limits.limit.π ((StructuredArrow.proj X L).comp F) f) = CategoryStruct.comp ((L.ran.obj F).map f.hom) ((L.ranCounit.app F).app f.right)
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.ranObjObjIsoLimit_hom_π_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (F : Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) (f : StructuredArrow X L) {Z : H} (h : F.obj ((StructuredArrow.proj X L).obj f) ⟶ Z) :
                                                  CategoryStruct.comp (L.ranObjObjIsoLimit F X).hom (CategoryStruct.comp (Limits.limit.π ((StructuredArrow.proj X L).comp F) f) h) = CategoryStruct.comp ((L.ran.obj F).map f.hom) (CategoryStruct.comp ((L.ranCounit.app F).app f.right) h)
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.ranObjObjIsoLimit_inv_π {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (F : Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) (f : StructuredArrow X L) :
                                                  CategoryStruct.comp (L.ranObjObjIsoLimit F X).inv (CategoryStruct.comp ((L.ran.obj F).map f.hom) ((L.ranCounit.app F).app f.right)) = Limits.limit.π ((StructuredArrow.proj X L).comp F) f
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.ranObjObjIsoLimit_inv_π_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (F : Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) (f : StructuredArrow X L) {Z : H} (h : F.obj f.right ⟶ Z) :
                                                  CategoryStruct.comp (L.ranObjObjIsoLimit F X).inv (CategoryStruct.comp ((L.ran.obj F).map f.hom) (CategoryStruct.comp ((L.ranCounit.app F).app f.right) h)) = CategoryStruct.comp (Limits.limit.π ((StructuredArrow.proj X L).comp F) f) h
                                                  source
                                                  noncomputable def CategoryTheory.Functor.ranAdjunction {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (L : Functor C D) (H : Type u_3) [Category.{u_6, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] :
                                                  (whiskeringLeft C D H).obj L ⊣ L.ran

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

                                                  Equations
                                                    Instances For
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Functor.ranAdjunction_counit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) (H : Type u_3) [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] :
                                                      (L.ranAdjunction H).counit = L.ranCounit
                                                      source
                                                      theorem CategoryTheory.Functor.ranAdjunction_unit_app {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (G : Functor D H) :
                                                      (L.ranAdjunction H).unit.app G = (L.ran.obj (L.comp G)).liftOfIsRightKanExtension (L.ranCounit.app (L.comp G)) G (CategoryStruct.id (L.comp G))
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Functor.ranCounit_app_whiskerLeft_ranAdjunction_unit_app {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (G : Functor D H) :
                                                      CategoryStruct.comp (L.whiskerLeft ((L.ranAdjunction H).unit.app G)) (L.ranCounit.app (L.comp G)) = CategoryStruct.id (L.comp G)
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Functor.ranCounit_app_whiskerLeft_ranAdjunction_unit_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (G : Functor D H) {Z : Functor C H} (h : L.comp G ⟶ Z) :
                                                      CategoryStruct.comp (L.whiskerLeft ((L.ranAdjunction H).unit.app G)) (CategoryStruct.comp (L.ranCounit.app (L.comp G)) h) = h
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Functor.ranCounit_app_app_ranAdjunction_unit_app_app {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (G : Functor D H) (X : C) :
                                                      CategoryStruct.comp (((L.ranAdjunction H).unit.app G).app (L.obj X)) ((L.ranCounit.app (L.comp G)).app X) = CategoryStruct.id (((Functor.id (Functor D H)).obj G).obj (L.obj X))
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Functor.ranCounit_app_app_ranAdjunction_unit_app_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (G : Functor D H) (X : C) {Z : H} (h : G.obj (L.obj X) ⟶ Z) :
                                                      CategoryStruct.comp (((L.ranAdjunction H).unit.app G).app (L.obj X)) (CategoryStruct.comp ((L.ranCounit.app (L.comp G)).app X) h) = h
                                                      source
                                                      theorem CategoryTheory.Functor.isIso_ranAdjunction_unit_app_iff {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [∀ (F : Functor C H), L.HasRightKanExtension F] (G : Functor D H) :
                                                      IsIso ((L.ranAdjunction H).unit.app G) ↔ G.IsRightKanExtension (CategoryStruct.id (L.comp G))
                                                      source
                                                      noncomputable def CategoryTheory.Functor.ranCompLimIso {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {H : Type u_3} [Category.{u_6, u_3} H] (L : Functor C D) [∀ (G : Functor C H), L.HasRightKanExtension G] [Limits.HasLimitsOfShape C H] [Limits.HasLimitsOfShape D H] :
                                                      L.ran.comp Limits.lim ≅ Limits.lim

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

                                                      Equations
                                                        Instances For
                                                          source
                                                          @[simp]
                                                          theorem CategoryTheory.Functor.ranCompLimIso_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {H : Type u_3} [Category.{u_6, u_3} H] (L : Functor C D) [∀ (G : Functor C H), L.HasRightKanExtension G] [Limits.HasLimitsOfShape C H] [Limits.HasLimitsOfShape D H] (X : Functor C H) :
                                                          L.ranCompLimIso.inv.app X = ((L.ran.obj X).limitIsoOfIsRightKanExtension (L.ranCounit.app X)).inv
                                                          source
                                                          @[simp]
                                                          theorem CategoryTheory.Functor.ranCompLimIso_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {H : Type u_3} [Category.{u_6, u_3} H] (L : Functor C D) [∀ (G : Functor C H), L.HasRightKanExtension G] [Limits.HasLimitsOfShape C H] [Limits.HasLimitsOfShape D H] (X : Functor C H) :
                                                          L.ranCompLimIso.hom.app X = ((L.ran.obj X).limitIsoOfIsRightKanExtension (L.ranCounit.app X)).hom
                                                          source
                                                          instance CategoryTheory.Functor.instIsIsoAppRanCounit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [L.Full] [L.Faithful] (F : Functor C H) (X : C) [L.HasPointwiseRightKanExtension F] [∀ (F : Functor C H), L.HasRightKanExtension F] :
                                                          IsIso ((L.ranCounit.app F).app X)
                                                          source
                                                          instance CategoryTheory.Functor.instIsIsoAppRanCounit_1 {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [L.Full] [L.Faithful] (F : Functor C H) [L.HasPointwiseRightKanExtension F] [∀ (F : Functor C H), L.HasRightKanExtension F] :
                                                          IsIso (L.ranCounit.app F)
                                                          source
                                                          instance CategoryTheory.Functor.reflective {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [L.Full] [L.Faithful] [∀ (F : Functor C H), L.HasPointwiseRightKanExtension F] :
                                                          IsIso L.ranCounit
                                                          source
                                                          instance CategoryTheory.Functor.instIsIsoAppCounitRanAdjunctionOfHasPointwiseRightKanExtension {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [L.Full] [L.Faithful] (F : Functor C H) [L.HasPointwiseRightKanExtension F] [∀ (F : Functor C H), L.HasRightKanExtension F] :
                                                          IsIso ((L.ranAdjunction H).counit.app F)
                                                          source
                                                          instance CategoryTheory.Functor.reflective' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] (L : Functor C D) {H : Type u_3} [Category.{u_5, u_3} H] [L.Full] [L.Faithful] [∀ (F : Functor C H), L.HasPointwiseRightKanExtension F] :
                                                          IsIso (L.ranAdjunction H).counit