Documentation

Mathlib.CategoryTheory.Functor.KanExtension.Basic

Kan extensions #

The basic definitions for Kan extensions of functors is introduced in this file. Part of API is parallel to the definitions for bicategories (see CategoryTheory.Bicategory.Kan.IsKan). (The bicategory API cannot be used directly here because it would not allow the universe polymorphism which is necessary for some applications.)

Given a natural transformation α : L ⋙ F' ⟶ F, we define the property F'.IsRightKanExtension α which expresses that (F', α) is a right Kan extension of F along L, i.e. that it is a terminal object in a category RightExtension L F of costructured arrows. The condition F'.IsLeftKanExtension α for α : F ⟶ L ⋙ F' is defined similarly.

We also introduce typeclasses HasRightKanExtension L F and HasLeftKanExtension L F which assert the existence of a right or left Kan extension, and chosen Kan extensions are obtained as leftKanExtension L F and rightKanExtension L F.

References #

@[reducible, inline]

Given two functors L : C ⥤ D and F : C ⥤ H, this is the category of functors F' : H ⥤ D equipped with a natural transformation L ⋙ F' ⟶ F.

Equations
Instances For
    @[reducible, inline]

    Given two functors L : C ⥤ D and F : C ⥤ H, this is the category of functors F' : H ⥤ D equipped with a natural transformation F ⟶ L ⋙ F'.

    Equations
    Instances For

      Given α : L ⋙ F' ⟶ F, the property F'.IsRightKanExtension α asserts that (F', α) is a terminal object in the category RightExtension L F, i.e. that (F', α) is a right Kan extension of F along L.

      Instances

        If (F', α) is a right Kan extension of F along L, then (F', α) is a terminal object in the category RightExtension L F.

        Equations
        • F'.isUniversalOfIsRightKanExtension α = .some
        Instances For
          noncomputable def CategoryTheory.Functor.liftOfIsRightKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) [F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H) (β : L.comp G F) :
          G F'

          If (F', α) is a right Kan extension of F along L and β : L ⋙ G ⟶ F is a natural transformation, this is the induced morphism G ⟶ F'.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.Functor.liftOfIsRightKanExtension_fac {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) [F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H) (β : L.comp G F) :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L (F'.liftOfIsRightKanExtension α G β)) α = β
            @[simp]
            theorem CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app_assoc {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) [F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H) (β : L.comp G F) (X : C) {Z : H} (h : F.obj X Z) :
            CategoryTheory.CategoryStruct.comp ((F'.liftOfIsRightKanExtension α G β).app (L.obj X)) (CategoryTheory.CategoryStruct.comp (α.app X) h) = CategoryTheory.CategoryStruct.comp (β.app X) h
            @[simp]
            theorem CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) [F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H) (β : L.comp G F) (X : C) :
            CategoryTheory.CategoryStruct.comp ((F'.liftOfIsRightKanExtension α G β).app (L.obj X)) (α.app X) = β.app X
            noncomputable def CategoryTheory.Functor.homEquivOfIsRightKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) [F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H) :
            (G F') (L.comp G F)

            If (F', α) is a right Kan extension of F along L, then this is the induced bijection (G ⟶ F') ≃ (L ⋙ G ⟶ F) for all G.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem CategoryTheory.Functor.isRightKanExtension_of_iso {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] {F' : CategoryTheory.Functor D H} {F'' : CategoryTheory.Functor D H} (e : F' F'') {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) (α' : L.comp F'' F) (comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L e.hom) α' = α) [F'.IsRightKanExtension α] :
              F''.IsRightKanExtension α'
              theorem CategoryTheory.Functor.isRightKanExtension_iff_of_iso {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] {F' : CategoryTheory.Functor D H} {F'' : CategoryTheory.Functor D H} (e : F' F'') {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) (α' : L.comp F'' F) (comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L e.hom) α' = α) :
              F'.IsRightKanExtension α F''.IsRightKanExtension α'
              @[simp]
              theorem CategoryTheory.Functor.rightKanExtensionUniqueOfIso_inv {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) [F'.IsRightKanExtension α] {G : CategoryTheory.Functor C H} (i : F G) (G' : CategoryTheory.Functor D H) (β : L.comp G' G) [G'.IsRightKanExtension β] :
              (F'.rightKanExtensionUniqueOfIso α i G' β).inv = F'.liftOfIsRightKanExtension α G' (CategoryTheory.CategoryStruct.comp β i.inv)
              @[simp]
              theorem CategoryTheory.Functor.rightKanExtensionUniqueOfIso_hom {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) [F'.IsRightKanExtension α] {G : CategoryTheory.Functor C H} (i : F G) (G' : CategoryTheory.Functor D H) (β : L.comp G' G) [G'.IsRightKanExtension β] :
              (F'.rightKanExtensionUniqueOfIso α i G' β).hom = G'.liftOfIsRightKanExtension β F' (CategoryTheory.CategoryStruct.comp α i.hom)
              noncomputable def CategoryTheory.Functor.rightKanExtensionUniqueOfIso {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) [F'.IsRightKanExtension α] {G : CategoryTheory.Functor C H} (i : F G) (G' : CategoryTheory.Functor D H) (β : L.comp G' G) [G'.IsRightKanExtension β] :
              F' G'

              Right Kan extensions of isomorphic functors are isomorphic.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.Functor.rightKanExtensionUnique_hom {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) [F'.IsRightKanExtension α] (F'' : CategoryTheory.Functor D H) (α' : L.comp F'' F) [F''.IsRightKanExtension α'] :
                (F'.rightKanExtensionUnique α F'' α').hom = F''.liftOfIsRightKanExtension α' F' α
                @[simp]
                theorem CategoryTheory.Functor.rightKanExtensionUnique_inv {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) [F'.IsRightKanExtension α] (F'' : CategoryTheory.Functor D H) (α' : L.comp F'' F) [F''.IsRightKanExtension α'] :
                (F'.rightKanExtensionUnique α F'' α').inv = F'.liftOfIsRightKanExtension α F'' α'
                noncomputable def CategoryTheory.Functor.rightKanExtensionUnique {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) [F'.IsRightKanExtension α] (F'' : CategoryTheory.Functor D H) (α' : L.comp F'' F) [F''.IsRightKanExtension α'] :
                F' F''

                Two right Kan extensions are (canonically) isomorphic.

                Equations
                Instances For
                  theorem CategoryTheory.Functor.isRightKanExtension_iff_isIso {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] {F' : CategoryTheory.Functor D H} {F'' : CategoryTheory.Functor D H} (φ : F'' F') {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) (α' : L.comp F'' F) (comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L φ) α = α') [F'.IsRightKanExtension α] :
                  F''.IsRightKanExtension α' CategoryTheory.IsIso φ

                  Given α : F ⟶ L ⋙ F', the property F'.IsLeftKanExtension α asserts that (F', α) is an initial object in the category LeftExtension L F, i.e. that (F', α) is a left Kan extension of F along L.

                  Instances

                    If (F', α) is a left Kan extension of F along L, then (F', α) is an initial object in the category LeftExtension L F.

                    Equations
                    • F'.isUniversalOfIsLeftKanExtension α = .some
                    Instances For
                      noncomputable def CategoryTheory.Functor.descOfIsLeftKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') [F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H) (β : F L.comp G) :
                      F' G

                      If (F', α) is a left Kan extension of F along L and β : F ⟶ L ⋙ G is a natural transformation, this is the induced morphism F' ⟶ G.

                      Equations
                      Instances For
                        @[simp]
                        theorem CategoryTheory.Functor.descOfIsLeftKanExtension_fac {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') [F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H) (β : F L.comp G) :
                        CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L (F'.descOfIsLeftKanExtension α G β)) = β
                        @[simp]
                        theorem CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app_assoc {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') [F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H) (β : F L.comp G) (X : C) {Z : H} (h : G.obj (L.obj X) Z) :
                        CategoryTheory.CategoryStruct.comp (α.app X) (CategoryTheory.CategoryStruct.comp ((F'.descOfIsLeftKanExtension α G β).app (L.obj X)) h) = CategoryTheory.CategoryStruct.comp (β.app X) h
                        @[simp]
                        theorem CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') [F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H) (β : F L.comp G) (X : C) :
                        CategoryTheory.CategoryStruct.comp (α.app X) ((F'.descOfIsLeftKanExtension α G β).app (L.obj X)) = β.app X
                        noncomputable def CategoryTheory.Functor.homEquivOfIsLeftKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') [F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H) :
                        (F' G) (F L.comp G)

                        If (F', α) is a left Kan extension of F along L, then this is the induced bijection (F' ⟶ G) ≃ (F ⟶ L ⋙ G) for all G.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem CategoryTheory.Functor.isLeftKanExtension_of_iso {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] {F' : CategoryTheory.Functor D H} {F'' : CategoryTheory.Functor D H} (e : F' F'') {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') (α' : F L.comp F'') (comm : CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L e.hom) = α') [F'.IsLeftKanExtension α] :
                          F''.IsLeftKanExtension α'
                          theorem CategoryTheory.Functor.isLeftKanExtension_iff_of_iso {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] {F' : CategoryTheory.Functor D H} {F'' : CategoryTheory.Functor D H} (e : F' F'') {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') (α' : F L.comp F'') (comm : CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L e.hom) = α') :
                          F'.IsLeftKanExtension α F''.IsLeftKanExtension α'
                          @[simp]
                          theorem CategoryTheory.Functor.leftKanExtensionUniqueOfIso_hom {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') [F'.IsLeftKanExtension α] {G : CategoryTheory.Functor C H} (i : F G) (G' : CategoryTheory.Functor D H) (β : G L.comp G') [G'.IsLeftKanExtension β] :
                          (F'.leftKanExtensionUniqueOfIso α i G' β).hom = F'.descOfIsLeftKanExtension α G' (CategoryTheory.CategoryStruct.comp i.hom β)
                          @[simp]
                          theorem CategoryTheory.Functor.leftKanExtensionUniqueOfIso_inv {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') [F'.IsLeftKanExtension α] {G : CategoryTheory.Functor C H} (i : F G) (G' : CategoryTheory.Functor D H) (β : G L.comp G') [G'.IsLeftKanExtension β] :
                          (F'.leftKanExtensionUniqueOfIso α i G' β).inv = G'.descOfIsLeftKanExtension β F' (CategoryTheory.CategoryStruct.comp i.inv α)
                          noncomputable def CategoryTheory.Functor.leftKanExtensionUniqueOfIso {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') [F'.IsLeftKanExtension α] {G : CategoryTheory.Functor C H} (i : F G) (G' : CategoryTheory.Functor D H) (β : G L.comp G') [G'.IsLeftKanExtension β] :
                          F' G'

                          Left Kan extensions of isomorphic functors are isomorphic.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem CategoryTheory.Functor.leftKanExtensionUnique_hom {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') [F'.IsLeftKanExtension α] (F'' : CategoryTheory.Functor D H) (α' : F L.comp F'') [F''.IsLeftKanExtension α'] :
                            (F'.leftKanExtensionUnique α F'' α').hom = F'.descOfIsLeftKanExtension α F'' α'
                            @[simp]
                            theorem CategoryTheory.Functor.leftKanExtensionUnique_inv {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') [F'.IsLeftKanExtension α] (F'' : CategoryTheory.Functor D H) (α' : F L.comp F'') [F''.IsLeftKanExtension α'] :
                            (F'.leftKanExtensionUnique α F'' α').inv = F''.descOfIsLeftKanExtension α' F' α
                            noncomputable def CategoryTheory.Functor.leftKanExtensionUnique {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') [F'.IsLeftKanExtension α] (F'' : CategoryTheory.Functor D H) (α' : F L.comp F'') [F''.IsLeftKanExtension α'] :
                            F' F''

                            Two left Kan extensions are (canonically) isomorphic.

                            Equations
                            Instances For
                              theorem CategoryTheory.Functor.isLeftKanExtension_iff_isIso {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] {F' : CategoryTheory.Functor D H} {F'' : CategoryTheory.Functor D H} (φ : F' F'') {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') (α' : F L.comp F'') (comm : CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L φ) = α') [F'.IsLeftKanExtension α] :
                              F''.IsLeftKanExtension α' CategoryTheory.IsIso φ
                              @[reducible, inline]

                              This property HasRightKanExtension L F holds when the functor F has a right Kan extension along L.

                              Equations
                              Instances For
                                theorem CategoryTheory.Functor.HasRightKanExtension.mk {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : L.comp F' F) [F'.IsRightKanExtension α] :
                                L.HasRightKanExtension F
                                @[reducible, inline]

                                This property HasLeftKanExtension L F holds when the functor F has a left Kan extension along L.

                                Equations
                                Instances For
                                  theorem CategoryTheory.Functor.HasLeftKanExtension.mk {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (α : F L.comp F') [F'.IsLeftKanExtension α] :
                                  L.HasLeftKanExtension F

                                  A chosen right Kan extension when [HasRightKanExtension L F] holds.

                                  Equations
                                  • L.rightKanExtension F = (⊤_ L.RightExtension F).left
                                  Instances For
                                    noncomputable def CategoryTheory.Functor.rightKanExtensionCounit {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasRightKanExtension F] :
                                    L.comp (L.rightKanExtension F) F

                                    The counit of the chosen right Kan extension rightKanExtension L F.

                                    Equations
                                    • L.rightKanExtensionCounit F = (⊤_ L.RightExtension F).hom
                                    Instances For
                                      instance CategoryTheory.Functor.instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasRightKanExtension F] :
                                      (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F)
                                      Equations
                                      • =
                                      theorem CategoryTheory.Functor.rightKanExtension_hom_ext_iff {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} [L.HasRightKanExtension F] {G : CategoryTheory.Functor D H} {γ₁ : G L.rightKanExtension F} {γ₂ : G L.rightKanExtension F} :
                                      γ₁ = γ₂ CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L γ₁) (L.rightKanExtensionCounit F) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L γ₂) (L.rightKanExtensionCounit F)
                                      theorem CategoryTheory.Functor.rightKanExtension_hom_ext {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasRightKanExtension F] {G : CategoryTheory.Functor D H} (γ₁ : G L.rightKanExtension F) (γ₂ : G L.rightKanExtension F) (hγ : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L γ₁) (L.rightKanExtensionCounit F) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L γ₂) (L.rightKanExtensionCounit F)) :
                                      γ₁ = γ₂

                                      A chosen left Kan extension when [HasLeftKanExtension L F] holds.

                                      Equations
                                      • L.leftKanExtension F = (⊥_ L.LeftExtension F).right
                                      Instances For
                                        noncomputable def CategoryTheory.Functor.leftKanExtensionUnit {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasLeftKanExtension F] :
                                        F L.comp (L.leftKanExtension F)

                                        The unit of the chosen left Kan extension leftKanExtension L F.

                                        Equations
                                        • L.leftKanExtensionUnit F = (⊥_ L.LeftExtension F).hom
                                        Instances For
                                          instance CategoryTheory.Functor.instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasLeftKanExtension F] :
                                          (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F)
                                          Equations
                                          • =
                                          theorem CategoryTheory.Functor.leftKanExtension_hom_ext_iff {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} [L.HasLeftKanExtension F] {G : CategoryTheory.Functor D H} {γ₁ : L.leftKanExtension F G} {γ₂ : L.leftKanExtension F G} :
                                          γ₁ = γ₂ CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit F) (CategoryTheory.whiskerLeft L γ₁) = CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit F) (CategoryTheory.whiskerLeft L γ₂)
                                          theorem CategoryTheory.Functor.leftKanExtension_hom_ext {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasLeftKanExtension F] {G : CategoryTheory.Functor D H} (γ₁ : L.leftKanExtension F G) (γ₂ : L.leftKanExtension F G) (hγ : CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit F) (CategoryTheory.whiskerLeft L γ₁) = CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit F) (CategoryTheory.whiskerLeft L γ₂)) :
                                          γ₁ = γ₂

                                          The functor RightExtension L' F ⥤ RightExtension L F induced by a natural transformation L ⋙ G ⟶ L'.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            theorem CategoryTheory.Functor.hasLeftExtension_iff_postcomp₁ {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_8, u_1} C] [CategoryTheory.Category.{u_10, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_7, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} {G : CategoryTheory.Functor D D'} [G.IsEquivalence] (e : L.comp G L') (F : CategoryTheory.Functor C H) :
                                            L'.HasLeftKanExtension F L.HasLeftKanExtension F
                                            theorem CategoryTheory.Functor.hasRightExtension_iff_postcomp₁ {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_8, u_1} C] [CategoryTheory.Category.{u_10, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_7, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} {G : CategoryTheory.Functor D D'} [G.IsEquivalence] (e : L.comp G L') (F : CategoryTheory.Functor C H) :
                                            L'.HasRightKanExtension F L.HasRightKanExtension F

                                            Given an isomorphism e : L ⋙ G ≅ L', a left extension of F along L' is universal iff the corresponding left extension of L along L is.

                                            Equations
                                            Instances For

                                              Given an isomorphism e : L ⋙ G ≅ L', a right extension of F along L' is universal iff the corresponding right extension of L along L is.

                                              Equations
                                              Instances For
                                                theorem CategoryTheory.Functor.isLeftKanExtension_iff_postcomp₁ {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_8, u_1} C] [CategoryTheory.Category.{u_7, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] [CategoryTheory.Category.{u_9, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') [G.IsEquivalence] (e : L.comp G L') {F : CategoryTheory.Functor C H} {F' : CategoryTheory.Functor D' H} (α : F L'.comp F') :
                                                F'.IsLeftKanExtension α (G.comp F').IsLeftKanExtension (CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight e.inv F') (L.associator G F').hom))
                                                theorem CategoryTheory.Functor.isRightKanExtension_iff_postcomp₁ {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_8, u_1} C] [CategoryTheory.Category.{u_7, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] [CategoryTheory.Category.{u_9, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') [G.IsEquivalence] (e : L.comp G L') {F : CategoryTheory.Functor C H} {F' : CategoryTheory.Functor D' H} (α : L'.comp F' F) :
                                                F'.IsRightKanExtension α (G.comp F').IsRightKanExtension (CategoryTheory.CategoryStruct.comp (L.associator G F').inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight e.hom F') α))

                                                The functor LeftExtension L F ⥤ LeftExtension (G ⋙ L) (G ⋙ F) obtained by precomposition.

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

                                                  The functor RightExtension L F ⥤ RightExtension (G ⋙ L) (G ⋙ F) obtained by precomposition.

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

                                                    The equivalence RightExtension L F ≌ RightExtension L' F induced by a natural isomorphism L ≅ L'.

                                                    Equations
                                                    Instances For

                                                      The equivalence LeftExtension L F ≌ LeftExtension L' F induced by a natural isomorphism L ≅ L'.

                                                      Equations
                                                      Instances For

                                                        The equivalence RightExtension L F ≌ RightExtension L F' induced by a natural isomorphism F ≅ F'.

                                                        Equations
                                                        Instances For

                                                          The equivalence LeftExtension L F ≌ LeftExtension L F' induced by a natural isomorphism F ≅ F'.

                                                          Equations
                                                          Instances For

                                                            When two left extensions α₁ : LeftExtension L F₁ and α₂ : LeftExtension L F₂ are essentially the same via an isomorphism of functors F₁ ≅ F₂, then α₁ is universal iff α₂ is.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              theorem CategoryTheory.Functor.isLeftKanExtension_iff_of_iso₂ {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] {L : CategoryTheory.Functor C D} {F₁ : CategoryTheory.Functor C H} {F₂ : CategoryTheory.Functor C H} {F₁' : CategoryTheory.Functor D H} {F₂' : CategoryTheory.Functor D H} (α₁ : F₁ L.comp F₁') (α₂ : F₂ L.comp F₂') (e : F₁ F₂) (e' : F₁' F₂') (h : CategoryTheory.CategoryStruct.comp α₁ (CategoryTheory.whiskerLeft L e'.hom) = CategoryTheory.CategoryStruct.comp e.hom α₂) :
                                                              F₁'.IsLeftKanExtension α₁ F₂'.IsLeftKanExtension α₂

                                                              When two right extensions α₁ : RightExtension L F₁ and α₂ : RightExtension L F₂ are essentially the same via an isomorphism of functors F₁ ≅ F₂, then α₁ is universal iff α₂ is.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                theorem CategoryTheory.Functor.isRightKanExtension_iff_of_iso₂ {C : Type u_1} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_7, u_5} D] {L : CategoryTheory.Functor C D} {F₁ : CategoryTheory.Functor C H} {F₂ : CategoryTheory.Functor C H} {F₁' : CategoryTheory.Functor D H} {F₂' : CategoryTheory.Functor D H} (α₁ : L.comp F₁' F₁) (α₂ : L.comp F₂' F₂) (e : F₁ F₂) (e' : F₁' F₂') (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L e'.hom) α₂ = CategoryTheory.CategoryStruct.comp α₁ e.hom) :
                                                                F₁'.IsRightKanExtension α₁ F₂'.IsRightKanExtension α₂