Documentation

Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Pointwise Kan extensions #

In this file, we define the notion of pointwise (left) Kan extension. Given two functors L : C ⥤ D and F : C ⥤ H, and E : LeftExtension L F, we introduce a cocone E.coconeAt Y for the functor CostructuredArrow.proj L Y ⋙ F : CostructuredArrow L Y ⥤ H the point of which is E.right.obj Y, and the type E.IsPointwiseLeftKanExtensionAt Y which expresses that E.coconeAt Y is colimit. When this holds for all Y : D, we may say that E is a pointwise left Kan extension (E.IsPointwiseLeftKanExtension).

Conversely, when CostructuredArrow.proj L Y ⋙ F has a colimit, we say that F has a pointwise left Kan extension at Y : D (HasPointwiseLeftKanExtensionAt L F Y), and if this holds for all Y : D, we construct a functor pointwiseLeftKanExtension L F : D ⥤ H and show it is a pointwise Kan extension.

A dual API for pointwise right Kan extension is also formalized.

References #

@[reducible, inline]

The condition that a functor F has a pointwise left Kan extension along L at Y. It means that the functor CostructuredArrow.proj L Y ⋙ F : CostructuredArrow L Y ⥤ H has a colimit.

Equations
Instances For
    @[reducible, inline]

    The condition that a functor F has a pointwise left Kan extension along L: it means that it has a pointwise left Kan extension at any object.

    Equations
    • L.HasPointwiseLeftKanExtension F = ∀ (Y : D), L.HasPointwiseLeftKanExtensionAt F Y
    Instances For
      @[reducible, inline]

      The condition that a functor F has a pointwise right Kan extension along L at Y. It means that the functor StructuredArrow.proj Y L ⋙ F : StructuredArrow Y L ⥤ H has a limit.

      Equations
      Instances For
        @[reducible, inline]

        The condition that a functor F has a pointwise right Kan extension along L: it means that it has a pointwise right Kan extension at any object.

        Equations
        • L.HasPointwiseRightKanExtension F = ∀ (Y : D), L.HasPointwiseRightKanExtensionAt F Y
        Instances For
          @[simp]
          theorem CategoryTheory.Functor.LeftExtension.coconeAt_pt {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F) (Y : D) :
          (E.coconeAt Y).pt = E.right.obj Y
          @[simp]
          theorem CategoryTheory.Functor.LeftExtension.coconeAt_ι_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F) (Y : D) (g : CategoryTheory.CostructuredArrow L Y) :
          (E.coconeAt Y).app g = CategoryTheory.CategoryStruct.comp (E.hom.app g.left) (E.right.map g.hom)

          The cocone for CostructuredArrow.proj L Y ⋙ F attached to E : LeftExtension L F. The point of this cocone is E.right.obj Y

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.Functor.LeftExtension.coconeAtFunctor_map_hom {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) {E : L.LeftExtension F} {E' : L.LeftExtension F} (φ : E E') :
            ((CategoryTheory.Functor.LeftExtension.coconeAtFunctor L F Y).map φ).hom = φ.right.app Y

            The cocones for CostructuredArrow.proj L Y ⋙ F, as a functor from LeftExtension L F.

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

              A left extension E : LeftExtension L F is a pointwise left Kan extension at Y when E.coconeAt Y is a colimit cocone.

              Equations
              Instances For
                theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.hasPointwiseLeftKanExtensionAt {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) :
                L.HasPointwiseLeftKanExtensionAt F Y
                theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isIso_hom_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F) {X : C} (h : E.IsPointwiseLeftKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] :
                CategoryTheory.IsIso (E.hom.app X)
                @[reducible, inline]

                A left extension E : LeftExtension L F is a pointwise left Kan extension when it is a pointwise left Kan extension at any object.

                Equations
                • E.IsPointwiseLeftKanExtension = ((Y : D) → E.IsPointwiseLeftKanExtensionAt Y)
                Instances For
                  def CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtEquivOfIso {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {E' : L.LeftExtension F} (e : E E') (Y : D) :
                  E.IsPointwiseLeftKanExtensionAt Y E'.IsPointwiseLeftKanExtensionAt Y

                  If two left extensions E and E' are isomorphic, E is a pointwise left Kan extension at Y iff E' is.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionEquivOfIso {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {E' : L.LeftExtension F} (e : E E') :
                    E.IsPointwiseLeftKanExtension E'.IsPointwiseLeftKanExtension

                    If two left extensions E and E' are isomorphic, E is a pointwise left Kan extension iff E' is.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) :
                      L.HasPointwiseLeftKanExtension F
                      def CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.homFrom {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) (G : L.LeftExtension F) :
                      E G

                      The (unique) morphism from a pointwise left Kan extension.

                      Equations
                      Instances For
                        theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hom_ext {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) {G : L.LeftExtension F} {f₁ : E G} {f₂ : E G} :
                        f₁ = f₂

                        A pointwise left Kan extension is universal, i.e. it is a left Kan extension.

                        Equations
                        Instances For
                          theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) :
                          E.right.IsLeftKanExtension E.hom
                          @[simp]
                          theorem CategoryTheory.Functor.RightExtension.coneAt_pt {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.RightExtension F) (Y : D) :
                          (E.coneAt Y).pt = E.left.obj Y
                          @[simp]
                          theorem CategoryTheory.Functor.RightExtension.coneAt_π_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.RightExtension F) (Y : D) (g : CategoryTheory.StructuredArrow Y L) :
                          (E.coneAt Y).app g = CategoryTheory.CategoryStruct.comp (E.left.map g.hom) (E.hom.app g.right)

                          The cone for StructuredArrow.proj Y L ⋙ F attached to E : RightExtension L F. The point of this cone is E.left.obj Y

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem CategoryTheory.Functor.RightExtension.coneAtFunctor_map_hom {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) {E : L.RightExtension F} {E' : L.RightExtension F} (φ : E E') :
                            ((CategoryTheory.Functor.RightExtension.coneAtFunctor L F Y).map φ).hom = φ.left.app Y

                            The cones for StructuredArrow.proj Y L ⋙ F, as a functor from RightExtension L F.

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

                              A right extension E : RightExtension L F is a pointwise right Kan extension at Y when E.coneAt Y is a limit cone.

                              Equations
                              Instances For
                                theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.hasPointwiseRightKanExtensionAt {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) :
                                L.HasPointwiseRightKanExtensionAt F Y
                                theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isIso_hom_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.RightExtension F) {X : C} (h : E.IsPointwiseRightKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] :
                                CategoryTheory.IsIso (E.hom.app X)
                                @[reducible, inline]

                                A right extension E : RightExtension L F is a pointwise right Kan extension when it is a pointwise right Kan extension at any object.

                                Equations
                                • E.IsPointwiseRightKanExtension = ((Y : D) → E.IsPointwiseRightKanExtensionAt Y)
                                Instances For
                                  def CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtEquivOfIso {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {E' : L.RightExtension F} (e : E E') (Y : D) :
                                  E.IsPointwiseRightKanExtensionAt Y E'.IsPointwiseRightKanExtensionAt Y

                                  If two right extensions E and E' are isomorphic, E is a pointwise right Kan extension at Y iff E' is.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionEquivOfIso {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {E' : L.RightExtension F} (e : E E') :
                                    E.IsPointwiseRightKanExtension E'.IsPointwiseRightKanExtension

                                    If two right extensions E and E' are isomorphic, E is a pointwise right Kan extension iff E' is.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasPointwiseRightKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} (h : E.IsPointwiseRightKanExtension) :
                                      L.HasPointwiseRightKanExtension F
                                      def CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.homTo {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} (h : E.IsPointwiseRightKanExtension) (G : L.RightExtension F) :
                                      G E

                                      The (unique) morphism to a pointwise right Kan extension.

                                      Equations
                                      Instances For
                                        theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hom_ext {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} (h : E.IsPointwiseRightKanExtension) {G : L.RightExtension F} {f₁ : G E} {f₂ : G E} :
                                        f₁ = f₂

                                        A pointwise right Kan extension is universal, i.e. it is a right Kan extension.

                                        Equations
                                        Instances For
                                          theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isRightKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} (h : E.IsPointwiseRightKanExtension) :
                                          E.left.IsRightKanExtension E.hom
                                          @[simp]
                                          theorem CategoryTheory.Functor.pointwiseLeftKanExtension_map {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] {Y₁ : D} {Y₂ : D} (f : Y₁ Y₂) :

                                          The constructed pointwise left Kan extension when HasPointwiseLeftKanExtension L F holds.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            noncomputable def CategoryTheory.Functor.pointwiseLeftKanExtensionUnit {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] :
                                            F L.comp (L.pointwiseLeftKanExtension F)

                                            The unit of the constructed pointwise left Kan extension when HasPointwiseLeftKanExtension L F holds.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              noncomputable def CategoryTheory.Functor.pointwiseLeftKanExtensionIsPointwiseLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] :
                                              (CategoryTheory.Functor.LeftExtension.mk (L.pointwiseLeftKanExtension F) (L.pointwiseLeftKanExtensionUnit F)).IsPointwiseLeftKanExtension

                                              The functor pointwiseLeftKanExtension L F is a pointwise left Kan extension of F along L.

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

                                                The functor pointwiseLeftKanExtension L F is a left Kan extension of F along L.

                                                Equations
                                                • L.pointwiseLeftKanExtensionIsUniversal F = (L.pointwiseLeftKanExtensionIsPointwiseLeftKanExtension F).isUniversal
                                                Instances For
                                                  instance CategoryTheory.Functor.instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] :
                                                  (L.pointwiseLeftKanExtension F).IsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F)
                                                  Equations
                                                  • =
                                                  instance CategoryTheory.Functor.instHasLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] :
                                                  L.HasLeftKanExtension F
                                                  Equations
                                                  • =
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.costructuredArrowMapCocone_pt {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor D H) (α : F L.comp G) (Y : D) :
                                                  (L.costructuredArrowMapCocone F G α Y).pt = G.obj Y
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.costructuredArrowMapCocone_ι_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor D H) (α : F L.comp G) (Y : D) (f : CategoryTheory.CostructuredArrow L Y) :
                                                  (L.costructuredArrowMapCocone F G α Y).app f = CategoryTheory.CategoryStruct.comp (α.app f.left) (G.map f.hom)

                                                  An auxiliary cocone used in the lemma pointwiseLeftKanExtension_desc_app

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] (G : CategoryTheory.Functor D H) (α : F L.comp G) (Y : D) :
                                                    ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj L Y).comp F) (L.costructuredArrowMapCocone F G α Y)
                                                    noncomputable def CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} [L.HasPointwiseLeftKanExtension F] (F' : CategoryTheory.Functor D H) (α : F L.comp F') [F'.IsLeftKanExtension α] :
                                                    (CategoryTheory.Functor.LeftExtension.mk F' α).IsPointwiseLeftKanExtension

                                                    If F admits a pointwise left Kan extension along L, then any left Kan extension of F along L is a pointwise left Kan extension.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[simp]
                                                      @[simp]
                                                      theorem CategoryTheory.Functor.pointwiseRightKanExtension_map {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] {Y₁ : D} {Y₂ : D} (f : Y₁ Y₂) :
                                                      (L.pointwiseRightKanExtension F).map f = CategoryTheory.Limits.limit.lift ((CategoryTheory.StructuredArrow.proj Y₂ L).comp F) { pt := CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y₁ L).comp F), π := { app := fun (g : CategoryTheory.StructuredArrow Y₂ L) => CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y₁ L).comp F) ((CategoryTheory.StructuredArrow.map f).obj g), naturality := } }

                                                      The constructed pointwise right Kan extension when HasPointwiseRightKanExtension L F holds.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        noncomputable def CategoryTheory.Functor.pointwiseRightKanExtensionCounit {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] :
                                                        L.comp (L.pointwiseRightKanExtension F) F

                                                        The counit of the constructed pointwise right Kan extension when HasPointwiseRightKanExtension L F holds.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          noncomputable def CategoryTheory.Functor.pointwiseRightKanExtensionIsPointwiseRightKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] :
                                                          (CategoryTheory.Functor.RightExtension.mk (L.pointwiseRightKanExtension F) (L.pointwiseRightKanExtensionCounit F)).IsPointwiseRightKanExtension

                                                          The functor pointwiseRightKanExtension L F is a pointwise right Kan extension of F along L.

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

                                                            The functor pointwiseRightKanExtension L F is a right Kan extension of F along L.

                                                            Equations
                                                            • L.pointwiseRightKanExtensionIsUniversal F = (L.pointwiseRightKanExtensionIsPointwiseRightKanExtension F).isUniversal
                                                            Instances For
                                                              instance CategoryTheory.Functor.instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] :
                                                              (L.pointwiseRightKanExtension F).IsRightKanExtension (L.pointwiseRightKanExtensionCounit F)
                                                              Equations
                                                              • =
                                                              instance CategoryTheory.Functor.instHasRightKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] :
                                                              L.HasRightKanExtension F
                                                              Equations
                                                              • =
                                                              @[simp]
                                                              theorem CategoryTheory.Functor.structuredArrowMapCone_π_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor D H) (α : L.comp G F) (Y : D) (f : CategoryTheory.StructuredArrow Y L) :
                                                              (L.structuredArrowMapCone F G α Y).app f = CategoryTheory.CategoryStruct.comp (G.map f.hom) (α.app f.right)
                                                              @[simp]
                                                              theorem CategoryTheory.Functor.structuredArrowMapCone_pt {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor D H) (α : L.comp G F) (Y : D) :
                                                              (L.structuredArrowMapCone F G α Y).pt = G.obj Y

                                                              An auxiliary cocone used in the lemma pointwiseRightKanExtension_lift_app

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[simp]
                                                                theorem CategoryTheory.Functor.pointwiseRightKanExtension_lift_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (G : CategoryTheory.Functor D H) (α : L.comp G F) (Y : D) :
                                                                ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y = CategoryTheory.Limits.limit.lift ((CategoryTheory.StructuredArrow.proj Y L).comp F) (L.structuredArrowMapCone F G α Y)
                                                                noncomputable def CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsRightKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} [L.HasPointwiseRightKanExtension F] (F' : CategoryTheory.Functor D H) (α : L.comp F' F) [F'.IsRightKanExtension α] :
                                                                (CategoryTheory.Functor.RightExtension.mk F' α).IsPointwiseRightKanExtension

                                                                If F admits a pointwise right Kan extension along L, then any right Kan extension of F along L is a pointwise right Kan extension.

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