Kan extensions

The basic definitions for Kan extensions of functors are 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

• https://ncatlab.org/nlab/show/Kan+extension

@[reducible, inline]

abbrev CategoryTheory.Functor.RightExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) : Type (max (max (max (max u_3 u_4) v_3) v_4) u_1 v_3)

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

@[reducible, inline]

abbrev CategoryTheory.Functor.LeftExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) : Type (max (max (max (max u_3 u_4) v_3) v_4) u_1 v_3)

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

def CategoryTheory.Functor.RightExtension.mk {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) : L.RightExtension F

Constructor for objects of the category Functor.RightExtension L F.

@[simp]

theorem CategoryTheory.Functor.RightExtension.mk_right_as {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) : (mk F' α).right.as = PUnit.unit

@[simp]

theorem CategoryTheory.Functor.RightExtension.mk_hom {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) : (mk F' α).hom = α

@[simp]

theorem CategoryTheory.Functor.RightExtension.mk_left {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) : (mk F' α).left = F'

def CategoryTheory.Functor.LeftExtension.mk {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') : L.LeftExtension F

Constructor for objects of the category Functor.LeftExtension L F.

@[simp]

theorem CategoryTheory.Functor.LeftExtension.mk_left_as {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') : (mk F' α).left.as = PUnit.unit

@[simp]

theorem CategoryTheory.Functor.LeftExtension.mk_hom {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') : (mk F' α).hom = α

@[simp]

theorem CategoryTheory.Functor.LeftExtension.mk_right {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') : (mk F' α).right = F'

class CategoryTheory.Functor.IsRightKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) : Prop

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.

• nonempty_isUniversal : Nonempty (CostructuredArrow.IsUniversal (RightExtension.mk F' α))

noncomputable def CategoryTheory.Functor.isUniversalOfIsRightKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] : CostructuredArrow.IsUniversal (RightExtension.mk F' α)

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

noncomputable def CategoryTheory.Functor.liftOfIsRightKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (G : 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'.

@[simp]

theorem CategoryTheory.Functor.liftOfIsRightKanExtension_fac {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (G : Functor D H) (β : L.comp G ⟶ F) : CategoryStruct.comp (L.whiskerLeft (F'.liftOfIsRightKanExtension α G β)) α = β

@[simp]

theorem CategoryTheory.Functor.liftOfIsRightKanExtension_fac_assoc {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (G : Functor D H) (β : L.comp G ⟶ F) {Z : Functor C H} (h : F ⟶ Z) : CategoryStruct.comp (L.whiskerLeft (F'.liftOfIsRightKanExtension α G β)) (CategoryStruct.comp α h) = CategoryStruct.comp β h

@[simp]

theorem CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (G : Functor D H) (β : L.comp G ⟶ F) (X : C) : CategoryStruct.comp ((F'.liftOfIsRightKanExtension α G β).app (L.obj X)) (α.app X) = β.app X

@[simp]

theorem CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app_assoc {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (G : Functor D H) (β : L.comp G ⟶ F) (X : C) {Z : H} (h : F.obj X ⟶ Z) : CategoryStruct.comp ((F'.liftOfIsRightKanExtension α G β).app (L.obj X)) (CategoryStruct.comp (α.app X) h) = CategoryStruct.comp (β.app X) h

theorem CategoryTheory.Functor.hom_ext_of_isRightKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] {G : Functor D H} (γ₁ γ₂ : G ⟶ F') (hγ : CategoryStruct.comp (L.whiskerLeft γ₁) α = CategoryStruct.comp (L.whiskerLeft γ₂) α) : γ₁ = γ₂

noncomputable def CategoryTheory.Functor.homEquivOfIsRightKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (G : 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.

@[simp]

theorem CategoryTheory.Functor.homEquivOfIsRightKanExtension_symm_apply {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (G : Functor D H) (β : L.comp G ⟶ F) : (F'.homEquivOfIsRightKanExtension α G).symm β = F'.liftOfIsRightKanExtension α G β

@[simp]

theorem CategoryTheory.Functor.homEquivOfIsRightKanExtension_apply_app {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (G : Functor D H) (β : G ⟶ F') (X : C) : ((F'.homEquivOfIsRightKanExtension α G) β).app X = CategoryStruct.comp (β.app (L.obj X)) (α.app X)

theorem CategoryTheory.Functor.isRightKanExtension_of_iso {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {F' F'' : Functor D H} (e : F' ≅ F'') {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) (α' : L.comp F'' ⟶ F) (comm : CategoryStruct.comp (L.whiskerLeft e.hom) α' = α) [F'.IsRightKanExtension α] : F''.IsRightKanExtension α'

theorem CategoryTheory.Functor.isRightKanExtension_iff_of_iso {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {F' F'' : Functor D H} (e : F' ≅ F'') {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) (α' : L.comp F'' ⟶ F) (comm : CategoryStruct.comp (L.whiskerLeft e.hom) α' = α) : F'.IsRightKanExtension α ↔ F''.IsRightKanExtension α'

noncomputable def CategoryTheory.Functor.rightKanExtensionUniqueOfIso {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] {G : Functor C H} (i : F ≅ G) (G' : Functor D H) (β : L.comp G' ⟶ G) [G'.IsRightKanExtension β] : F' ≅ G'

Right Kan extensions of isomorphic functors are isomorphic.

@[simp]

theorem CategoryTheory.Functor.rightKanExtensionUniqueOfIso_inv {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] {G : Functor C H} (i : F ≅ G) (G' : Functor D H) (β : L.comp G' ⟶ G) [G'.IsRightKanExtension β] : (F'.rightKanExtensionUniqueOfIso α i G' β).inv = F'.liftOfIsRightKanExtension α G' (CategoryStruct.comp β i.inv)

@[simp]

theorem CategoryTheory.Functor.rightKanExtensionUniqueOfIso_hom {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] {G : Functor C H} (i : F ≅ G) (G' : Functor D H) (β : L.comp G' ⟶ G) [G'.IsRightKanExtension β] : (F'.rightKanExtensionUniqueOfIso α i G' β).hom = G'.liftOfIsRightKanExtension β F' (CategoryStruct.comp α i.hom)

noncomputable def CategoryTheory.Functor.rightKanExtensionUnique {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (F'' : Functor D H) (α' : L.comp F'' ⟶ F) [F''.IsRightKanExtension α'] : F' ≅ F''

Two right Kan extensions are (canonically) isomorphic.

@[simp]

theorem CategoryTheory.Functor.rightKanExtensionUnique_inv {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (F'' : Functor D H) (α' : L.comp F'' ⟶ F) [F''.IsRightKanExtension α'] : (F'.rightKanExtensionUnique α F'' α').inv = F'.liftOfIsRightKanExtension α F'' α'

@[simp]

theorem CategoryTheory.Functor.rightKanExtensionUnique_hom {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (F'' : Functor D H) (α' : L.comp F'' ⟶ F) [F''.IsRightKanExtension α'] : (F'.rightKanExtensionUnique α F'' α').hom = F''.liftOfIsRightKanExtension α' F' α

theorem CategoryTheory.Functor.isRightKanExtension_iff_isIso {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {F' F'' : Functor D H} (φ : F'' ⟶ F') {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) (α' : L.comp F'' ⟶ F) (comm : CategoryStruct.comp (L.whiskerLeft φ) α = α') [F'.IsRightKanExtension α] : F''.IsRightKanExtension α' ↔ IsIso φ

class CategoryTheory.Functor.IsLeftKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') : Prop

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.

• nonempty_isUniversal : Nonempty (StructuredArrow.IsUniversal (LeftExtension.mk F' α))

noncomputable def CategoryTheory.Functor.isUniversalOfIsLeftKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] : StructuredArrow.IsUniversal (LeftExtension.mk F' α)

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

noncomputable def CategoryTheory.Functor.descOfIsLeftKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (G : 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.

@[simp]

theorem CategoryTheory.Functor.descOfIsLeftKanExtension_fac {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (G : Functor D H) (β : F ⟶ L.comp G) : CategoryStruct.comp α (L.whiskerLeft (F'.descOfIsLeftKanExtension α G β)) = β

@[simp]

theorem CategoryTheory.Functor.descOfIsLeftKanExtension_fac_assoc {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (G : Functor D H) (β : F ⟶ L.comp G) {Z : Functor C H} (h : L.comp G ⟶ Z) : CategoryStruct.comp α (CategoryStruct.comp (L.whiskerLeft (F'.descOfIsLeftKanExtension α G β)) h) = CategoryStruct.comp β h

@[simp]

theorem CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (G : Functor D H) (β : F ⟶ L.comp G) (X : C) : CategoryStruct.comp (α.app X) ((F'.descOfIsLeftKanExtension α G β).app (L.obj X)) = β.app X

@[simp]

theorem CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app_assoc {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (G : Functor D H) (β : F ⟶ L.comp G) (X : C) {Z : H} (h : G.obj (L.obj X) ⟶ Z) : CategoryStruct.comp (α.app X) (CategoryStruct.comp ((F'.descOfIsLeftKanExtension α G β).app (L.obj X)) h) = CategoryStruct.comp (β.app X) h

theorem CategoryTheory.Functor.hom_ext_of_isLeftKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] {G : Functor D H} (γ₁ γ₂ : F' ⟶ G) (hγ : CategoryStruct.comp α (L.whiskerLeft γ₁) = CategoryStruct.comp α (L.whiskerLeft γ₂)) : γ₁ = γ₂

noncomputable def CategoryTheory.Functor.homEquivOfIsLeftKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (G : 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.

@[simp]

theorem CategoryTheory.Functor.homEquivOfIsLeftKanExtension_symm_apply {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (G : Functor D H) (β : F ⟶ L.comp G) : (F'.homEquivOfIsLeftKanExtension α G).symm β = F'.descOfIsLeftKanExtension α G β

@[simp]

theorem CategoryTheory.Functor.homEquivOfIsLeftKanExtension_apply_app {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (G : Functor D H) (β : F' ⟶ G) (X : C) : ((F'.homEquivOfIsLeftKanExtension α G) β).app X = CategoryStruct.comp (α.app X) (β.app (L.obj X))

theorem CategoryTheory.Functor.isLeftKanExtension_of_iso {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {F' F'' : Functor D H} (e : F' ≅ F'') {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') (α' : F ⟶ L.comp F'') (comm : CategoryStruct.comp α (L.whiskerLeft e.hom) = α') [F'.IsLeftKanExtension α] : F''.IsLeftKanExtension α'

theorem CategoryTheory.Functor.isLeftKanExtension_iff_of_iso {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {F' F'' : Functor D H} (e : F' ≅ F'') {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') (α' : F ⟶ L.comp F'') (comm : CategoryStruct.comp α (L.whiskerLeft e.hom) = α') : F'.IsLeftKanExtension α ↔ F''.IsLeftKanExtension α'

noncomputable def CategoryTheory.Functor.leftKanExtensionUniqueOfIso {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] {G : Functor C H} (i : F ≅ G) (G' : Functor D H) (β : G ⟶ L.comp G') [G'.IsLeftKanExtension β] : F' ≅ G'

Left Kan extensions of isomorphic functors are isomorphic.

@[simp]

theorem CategoryTheory.Functor.leftKanExtensionUniqueOfIso_inv {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] {G : Functor C H} (i : F ≅ G) (G' : Functor D H) (β : G ⟶ L.comp G') [G'.IsLeftKanExtension β] : (F'.leftKanExtensionUniqueOfIso α i G' β).inv = G'.descOfIsLeftKanExtension β F' (CategoryStruct.comp i.inv α)

@[simp]

theorem CategoryTheory.Functor.leftKanExtensionUniqueOfIso_hom {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] {G : Functor C H} (i : F ≅ G) (G' : Functor D H) (β : G ⟶ L.comp G') [G'.IsLeftKanExtension β] : (F'.leftKanExtensionUniqueOfIso α i G' β).hom = F'.descOfIsLeftKanExtension α G' (CategoryStruct.comp i.hom β)

noncomputable def CategoryTheory.Functor.leftKanExtensionUnique {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (F'' : Functor D H) (α' : F ⟶ L.comp F'') [F''.IsLeftKanExtension α'] : F' ≅ F''

Two left Kan extensions are (canonically) isomorphic.

@[simp]

theorem CategoryTheory.Functor.leftKanExtensionUnique_hom {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (F'' : 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_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (F'' : Functor D H) (α' : F ⟶ L.comp F'') [F''.IsLeftKanExtension α'] : (F'.leftKanExtensionUnique α F'' α').inv = F''.descOfIsLeftKanExtension α' F' α

theorem CategoryTheory.Functor.isLeftKanExtension_iff_isIso {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {F' F'' : Functor D H} (φ : F' ⟶ F'') {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') (α' : F ⟶ L.comp F'') (comm : CategoryStruct.comp α (L.whiskerLeft φ) = α') [F'.IsLeftKanExtension α] : F''.IsLeftKanExtension α' ↔ IsIso φ

@[reducible, inline]

abbrev CategoryTheory.Functor.HasRightKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) : Prop

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

theorem CategoryTheory.Functor.HasRightKanExtension.mk {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] : L.HasRightKanExtension F

@[reducible, inline]

abbrev CategoryTheory.Functor.HasLeftKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) : Prop

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

theorem CategoryTheory.Functor.HasLeftKanExtension.mk {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] : L.HasLeftKanExtension F

noncomputable def CategoryTheory.Functor.rightKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) [L.HasRightKanExtension F] : Functor D H

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

noncomputable def CategoryTheory.Functor.rightKanExtensionCounit {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) [L.HasRightKanExtension F] : L.comp (L.rightKanExtension F) ⟶ F

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

instance CategoryTheory.Functor.instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) [L.HasRightKanExtension F] : (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F)

theorem CategoryTheory.Functor.rightKanExtension_hom_ext {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) [L.HasRightKanExtension F] {G : Functor D H} (γ₁ γ₂ : G ⟶ L.rightKanExtension F) (hγ : CategoryStruct.comp (L.whiskerLeft γ₁) (L.rightKanExtensionCounit F) = CategoryStruct.comp (L.whiskerLeft γ₂) (L.rightKanExtensionCounit F)) : γ₁ = γ₂

theorem CategoryTheory.Functor.rightKanExtension_hom_ext_iff {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L : Functor C D} {F : Functor C H} [L.HasRightKanExtension F] {G : Functor D H} {γ₁ γ₂ : G ⟶ L.rightKanExtension F} : γ₁ = γ₂ ↔ CategoryStruct.comp (L.whiskerLeft γ₁) (L.rightKanExtensionCounit F) = CategoryStruct.comp (L.whiskerLeft γ₂) (L.rightKanExtensionCounit F)

noncomputable def CategoryTheory.Functor.leftKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) [L.HasLeftKanExtension F] : Functor D H

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

noncomputable def CategoryTheory.Functor.leftKanExtensionUnit {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) [L.HasLeftKanExtension F] : F ⟶ L.comp (L.leftKanExtension F)

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

instance CategoryTheory.Functor.instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) [L.HasLeftKanExtension F] : (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F)

theorem CategoryTheory.Functor.leftKanExtension_hom_ext {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) [L.HasLeftKanExtension F] {G : Functor D H} (γ₁ γ₂ : L.leftKanExtension F ⟶ G) (hγ : CategoryStruct.comp (L.leftKanExtensionUnit F) (L.whiskerLeft γ₁) = CategoryStruct.comp (L.leftKanExtensionUnit F) (L.whiskerLeft γ₂)) : γ₁ = γ₂

theorem CategoryTheory.Functor.leftKanExtension_hom_ext_iff {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L : Functor C D} {F : Functor C H} [L.HasLeftKanExtension F] {G : Functor D H} {γ₁ γ₂ : L.leftKanExtension F ⟶ G} : γ₁ = γ₂ ↔ CategoryStruct.comp (L.leftKanExtensionUnit F) (L.whiskerLeft γ₁) = CategoryStruct.comp (L.leftKanExtensionUnit F) (L.whiskerLeft γ₂)

def CategoryTheory.Functor.LeftExtension.postcomp₁ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L' ⟶ L.comp G) (F : Functor C H) : Functor (L'.LeftExtension F) (L.LeftExtension F)

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

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcomp₁_obj_left {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L' ⟶ L.comp G) (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D' H).obj L')) : ((postcomp₁ G f F).obj X).left = X.left

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcomp₁_obj_right_obj {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L' ⟶ L.comp G) (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D' H).obj L')) (X✝ : D) : ((postcomp₁ G f F).obj X).right.obj X✝ = X.right.obj (G.obj X✝)

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcomp₁_obj_right_map {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L' ⟶ L.comp G) (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D' H).obj L')) {X✝ Y✝ : D} (f✝ : X✝ ⟶ Y✝) : ((postcomp₁ G f F).obj X).right.map f✝ = X.right.map (G.map f✝)

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcomp₁_map_left {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L' ⟶ L.comp G) (F : Functor C H) {X Y : Comma (fromPUnit F) ((whiskeringLeft C D' H).obj L')} (φ : X ⟶ Y) : ((postcomp₁ G f F).map φ).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcomp₁_obj_hom_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L' ⟶ L.comp G) (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D' H).obj L')) (X✝ : C) : ((postcomp₁ G f F).obj X).hom.app X✝ = CategoryStruct.comp (X.hom.app X✝) (X.right.map (f.app X✝))

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcomp₁_map_right_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L' ⟶ L.comp G) (F : Functor C H) {X Y : Comma (fromPUnit F) ((whiskeringLeft C D' H).obj L')} (φ : X ⟶ Y) (X✝ : D) : ((postcomp₁ G f F).map φ).right.app X✝ = φ.right.app (G.obj X✝)

def CategoryTheory.Functor.RightExtension.postcomp₁ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L.comp G ⟶ L') (F : Functor C H) : Functor (L'.RightExtension F) (L.RightExtension F)

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

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcomp₁_map_right {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L.comp G ⟶ L') (F : Functor C H) {X Y : Comma ((whiskeringLeft C D' H).obj L') (fromPUnit F)} (φ : X ⟶ Y) : ((postcomp₁ G f F).map φ).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcomp₁_obj_right {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L.comp G ⟶ L') (F : Functor C H) (X : Comma ((whiskeringLeft C D' H).obj L') (fromPUnit F)) : ((postcomp₁ G f F).obj X).right = X.right

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcomp₁_map_left_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L.comp G ⟶ L') (F : Functor C H) {X Y : Comma ((whiskeringLeft C D' H).obj L') (fromPUnit F)} (φ : X ⟶ Y) (X✝ : D) : ((postcomp₁ G f F).map φ).left.app X✝ = φ.left.app (G.obj X✝)

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcomp₁_obj_left_obj {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L.comp G ⟶ L') (F : Functor C H) (X : Comma ((whiskeringLeft C D' H).obj L') (fromPUnit F)) (X✝ : D) : ((postcomp₁ G f F).obj X).left.obj X✝ = X.left.obj (G.obj X✝)

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcomp₁_obj_hom_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L.comp G ⟶ L') (F : Functor C H) (X : Comma ((whiskeringLeft C D' H).obj L') (fromPUnit F)) (X✝ : C) : ((postcomp₁ G f F).obj X).hom.app X✝ = CategoryStruct.comp (X.left.map (f.app X✝)) (X.hom.app X✝)

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcomp₁_obj_left_map {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') (f : L.comp G ⟶ L') (F : Functor C H) (X : Comma ((whiskeringLeft C D' H).obj L') (fromPUnit F)) {X✝ Y✝ : D} (f✝ : X✝ ⟶ Y✝) : ((postcomp₁ G f F).obj X).left.map f✝ = X.left.map (G.map f✝)

instance CategoryTheory.Functor.instIsEquivalenceLeftExtensionPostcomp₁OfIsIso {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') [G.IsEquivalence] (f : L' ⟶ L.comp G) [IsIso f] (F : Functor C H) : (LeftExtension.postcomp₁ G f F).IsEquivalence

instance CategoryTheory.Functor.instIsEquivalenceRightExtensionPostcomp₁OfIsIso {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') [G.IsEquivalence] (f : L.comp G ⟶ L') [IsIso f] (F : Functor C H) : (RightExtension.postcomp₁ G f F).IsEquivalence

theorem CategoryTheory.Functor.hasLeftExtension_iff_postcomp₁ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} {G : Functor D D'} [G.IsEquivalence] (e : L.comp G ≅ L') (F : 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_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} {G : Functor D D'} [G.IsEquivalence] (e : L.comp G ≅ L') (F : Functor C H) : L'.HasRightKanExtension F ↔ L.HasRightKanExtension F

noncomputable def CategoryTheory.Functor.LeftExtension.isUniversalPostcomp₁Equiv {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') [G.IsEquivalence] (e : L.comp G ≅ L') (F : Functor C H) (ex : L'.LeftExtension F) : StructuredArrow.IsUniversal ex ≃ StructuredArrow.IsUniversal ((postcomp₁ G e.inv F).obj ex)

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.

noncomputable def CategoryTheory.Functor.RightExtension.isUniversalPostcomp₁Equiv {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') [G.IsEquivalence] (e : L.comp G ≅ L') (F : Functor C H) (ex : L'.RightExtension F) : CostructuredArrow.IsUniversal ex ≃ CostructuredArrow.IsUniversal ((postcomp₁ G e.hom F).obj ex)

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.

theorem CategoryTheory.Functor.isLeftKanExtension_iff_postcomp₁ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') [G.IsEquivalence] (e : L.comp G ≅ L') {F : Functor C H} {F' : Functor D' H} (α : F ⟶ L'.comp F') : F'.IsLeftKanExtension α ↔ (G.comp F').IsLeftKanExtension (CategoryStruct.comp α (CategoryStruct.comp (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_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor C D'} (G : Functor D D') [G.IsEquivalence] (e : L.comp G ≅ L') {F : Functor C H} {F' : Functor D' H} (α : L'.comp F' ⟶ F) : F'.IsRightKanExtension α ↔ (G.comp F').IsRightKanExtension (CategoryStruct.comp (L.associator G F').inv (CategoryStruct.comp (whiskerRight e.hom F') α))

def CategoryTheory.Functor.LeftExtension.postcompose₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') : Functor (L.LeftExtension F) (L.LeftExtension (F.comp G))

Given a left extension E of F : C ⥤ H along L : C ⥤ D and a functor G : H ⥤ D', E.postcompose₂ G is the extension of F ⋙ G along L obtained by whiskering by G on the right.

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcompose₂_obj_right_map {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : ((postcompose₂ L F G).obj X).right.map f = G.map (X.right.map f)

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcompose₂_map_left {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') {X Y : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)} (φ : X ⟶ Y) : ((postcompose₂ L F G).map φ).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcompose₂_map_right_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') {X Y : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)} (φ : X ⟶ Y) (X✝ : D) : ((postcompose₂ L F G).map φ).right.app X✝ = G.map (φ.right.app X✝)

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcompose₂_obj_right_obj {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)) (X✝ : D) : ((postcompose₂ L F G).obj X).right.obj X✝ = G.obj (X.right.obj X✝)

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcompose₂_obj_left {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)) : ((postcompose₂ L F G).obj X).left = X.left

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcompose₂_obj_hom_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)) (X✝ : C) : ((postcompose₂ L F G).obj X).hom.app X✝ = G.map (X.hom.app X✝)

def CategoryTheory.Functor.RightExtension.postcompose₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') : Functor (L.RightExtension F) (L.RightExtension (F.comp G))

Given a right extension E of F : C ⥤ H along L : C ⥤ D and a functor G : H ⥤ D', E.postcompose₂ G is the extension of F ⋙ G along L obtained by whiskering by G on the right.

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcompose₂_obj_left_obj {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') (X : Comma ((whiskeringLeft C D H).obj L) (fromPUnit F)) (X✝ : D) : ((postcompose₂ L F G).obj X).left.obj X✝ = G.obj (X.left.obj X✝)

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcompose₂_map_right {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') {X Y : Comma ((whiskeringLeft C D H).obj L) (fromPUnit F)} (φ : X ⟶ Y) : ((postcompose₂ L F G).map φ).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcompose₂_obj_right {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') (X : Comma ((whiskeringLeft C D H).obj L) (fromPUnit F)) : ((postcompose₂ L F G).obj X).right = X.right

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcompose₂_obj_left_map {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') (X : Comma ((whiskeringLeft C D H).obj L) (fromPUnit F)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : ((postcompose₂ L F G).obj X).left.map f = G.map (X.left.map f)

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcompose₂_map_left_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') {X Y : Comma ((whiskeringLeft C D H).obj L) (fromPUnit F)} (φ : X ⟶ Y) (X✝ : D) : ((postcompose₂ L F G).map φ).left.app X✝ = G.map (φ.left.app X✝)

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcompose₂_obj_hom_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] (L : Functor C D) (F : Functor C H) (G : Functor H D') (X : Comma ((whiskeringLeft C D H).obj L) (fromPUnit F)) (X✝ : C) : ((postcompose₂ L F G).obj X).hom.app X✝ = G.map (X.hom.app X✝)

def CategoryTheory.Functor.LeftExtension.postcompose₂ObjMkIso {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {F : Functor C H} (G : Functor H D') {F' : Functor D H} (α : F ⟶ L.comp F') : (postcompose₂ L F G).obj (mk F' α) ≅ mk (F'.comp G) (CategoryStruct.comp (whiskerRight α G) (L.associator F' G).hom)

An isomorphism to describe the action of LeftExtension.postcompose₂ on terms of the form LeftExtension.mk _ α.

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcompose₂ObjMkIso_inv_right_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {F : Functor C H} (G : Functor H D') {F' : Functor D H} (α : F ⟶ L.comp F') (X : D) : (postcompose₂ObjMkIso G α).inv.right.app X = CategoryStruct.id (G.obj (F'.obj X))

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcompose₂ObjMkIso_hom_right_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {F : Functor C H} (G : Functor H D') {F' : Functor D H} (α : F ⟶ L.comp F') (X : D) : (postcompose₂ObjMkIso G α).hom.right.app X = CategoryStruct.id (G.obj (F'.obj X))

def CategoryTheory.Functor.RightExtension.postcompose₂ObjMkIso {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {F : Functor C H} (G : Functor H D') {F' : Functor D H} (α : L.comp F' ⟶ F) : (postcompose₂ L F G).obj (mk F' α) ≅ mk (F'.comp G) (CategoryStruct.comp (L.associator F' G).inv (whiskerRight α G))

An isomorphism to describe the action of RightExtension.postcompose₂ on terms of the form RightExtension.mk _ α.

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcompose₂ObjMkIso_hom_left_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {F : Functor C H} (G : Functor H D') {F' : Functor D H} (α : L.comp F' ⟶ F) (X : D) : (postcompose₂ObjMkIso G α).hom.left.app X = CategoryStruct.id (G.obj (F'.obj X))

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcompose₂ObjMkIso_inv_left_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {F : Functor C H} (G : Functor H D') {F' : Functor D H} (α : L.comp F' ⟶ F) (X : D) : (postcompose₂ObjMkIso G α).inv.left.app X = CategoryStruct.id (G.obj (F'.obj X))

def CategoryTheory.Functor.LeftExtension.precomp {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) : Functor (L.LeftExtension F) ((G.comp L).LeftExtension (G.comp F))

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

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp_map_right {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) {X Y : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)} (φ : X ⟶ Y) : ((precomp L F G).map φ).right = φ.right

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp_obj_right {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)) : ((precomp L F G).obj X).right = X.right

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp_obj_left {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)) : ((precomp L F G).obj X).left = X.left

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp_map_left {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) {X Y : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)} (φ : X ⟶ Y) : ((precomp L F G).map φ).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp_obj_hom_app {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)) (X✝ : C') : ((precomp L F G).obj X).hom.app X✝ = X.hom.app (G.obj X✝)

def CategoryTheory.Functor.RightExtension.precomp {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) : Functor (L.RightExtension F) ((G.comp L).RightExtension (G.comp F))

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

@[simp]

theorem CategoryTheory.Functor.RightExtension.precomp_obj_hom_app {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) (X : Comma ((whiskeringLeft C D H).obj L) (fromPUnit F)) (X✝ : C') : ((precomp L F G).obj X).hom.app X✝ = X.hom.app (G.obj X✝)

@[simp]

theorem CategoryTheory.Functor.RightExtension.precomp_obj_left {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) (X : Comma ((whiskeringLeft C D H).obj L) (fromPUnit F)) : ((precomp L F G).obj X).left = X.left

@[simp]

theorem CategoryTheory.Functor.RightExtension.precomp_obj_right {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) (X : Comma ((whiskeringLeft C D H).obj L) (fromPUnit F)) : ((precomp L F G).obj X).right = X.right

@[simp]

theorem CategoryTheory.Functor.RightExtension.precomp_map_left {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) {X Y : Comma ((whiskeringLeft C D H).obj L) (fromPUnit F)} (φ : X ⟶ Y) : ((precomp L F G).map φ).left = φ.left

@[simp]

theorem CategoryTheory.Functor.RightExtension.precomp_map_right {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) {X Y : Comma ((whiskeringLeft C D H).obj L) (fromPUnit F)} (φ : X ⟶ Y) : ((precomp L F G).map φ).right = CategoryStruct.id X.right

instance CategoryTheory.Functor.instIsEquivalenceLeftExtensionCompPrecomp {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) [G.IsEquivalence] : (LeftExtension.precomp L F G).IsEquivalence

instance CategoryTheory.Functor.instIsEquivalenceRightExtensionCompPrecomp {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) [G.IsEquivalence] : (RightExtension.precomp L F G).IsEquivalence

noncomputable def CategoryTheory.Functor.LeftExtension.isUniversalPrecompEquiv {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) [G.IsEquivalence] (e : L.LeftExtension F) : StructuredArrow.IsUniversal e ≃ StructuredArrow.IsUniversal ((precomp L F G).obj e)

If G is an equivalence, then a left extension of F along L is universal iff the corresponding left extension of G ⋙ F along G ⋙ L is.

noncomputable def CategoryTheory.Functor.RightExtension.isUniversalPrecompEquiv {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) (F : Functor C H) (G : Functor C' C) [G.IsEquivalence] (e : L.RightExtension F) : CostructuredArrow.IsUniversal e ≃ CostructuredArrow.IsUniversal ((precomp L F G).obj e)

If G is an equivalence, then a right extension of F along L is universal iff the corresponding left extension of G ⋙ F along G ⋙ L is.

theorem CategoryTheory.Functor.isLeftKanExtension_iff_precomp {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L : Functor C D} {F : Functor C H} (F' : Functor D H) (G : Functor C' C) [G.IsEquivalence] (α : F ⟶ L.comp F') : F'.IsLeftKanExtension α ↔ F'.IsLeftKanExtension (CategoryStruct.comp (G.whiskerLeft α) (G.associator L F').inv)

theorem CategoryTheory.Functor.isRightKanExtension_iff_precomp {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L : Functor C D} {F : Functor C H} (F' : Functor D H) (G : Functor C' C) [G.IsEquivalence] (α : L.comp F' ⟶ F) : F'.IsRightKanExtension α ↔ F'.IsRightKanExtension (CategoryStruct.comp (G.associator L F').hom (G.whiskerLeft α))

def CategoryTheory.Functor.rightExtensionEquivalenceOfIso₁ {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) : L.RightExtension F ≌ L'.RightExtension F

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

theorem CategoryTheory.Functor.hasRightExtension_iff_of_iso₁ {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) : L.HasRightKanExtension F ↔ L'.HasRightKanExtension F

def CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) : L.LeftExtension F ≌ L'.LeftExtension F

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

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_obj_hom_app {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)) (X✝ : C) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).functor.obj X).hom.app X✝ = CategoryStruct.comp (X.hom.app X✝) (X.right.map (iso₁.hom.app X✝))

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_obj_left {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).functor.obj X).left = X.left

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_counitIso_inv_app_right_app {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L')) (X✝ : D) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).counitIso.inv.app X).right.app X✝ = CategoryStruct.id (X.right.obj X✝)

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_unitIso_inv_app_right_app {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)) (X✝ : D) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).unitIso.inv.app X).right.app X✝ = CategoryStruct.id (X.right.obj X✝)

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_map_left {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) {X✝ Y✝ : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)} (f : X✝ ⟶ Y✝) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).functor.map f).left = CategoryStruct.id X✝.left

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_hom_app {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L')) (X✝ : C) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).inverse.obj X).hom.app X✝ = CategoryStruct.comp (X.hom.app X✝) (X.right.map (iso₁.inv.app X✝))

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_map_right {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) {X✝ Y✝ : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)} (f : X✝ ⟶ Y✝) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).functor.map f).right = f.right

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_left {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L')) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).inverse.obj X).left = X.left

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_obj_right {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).functor.obj X).right = X.right

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_counitIso_hom_app_right_app {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L')) (X✝ : D) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).counitIso.hom.app X).right.app X✝ = CategoryStruct.id (X.right.obj X✝)

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_map_left {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) {X✝ Y✝ : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L')} (f : X✝ ⟶ Y✝) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).inverse.map f).left = CategoryStruct.id X✝.left

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_map_right {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) {X✝ Y✝ : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L')} (f : X✝ ⟶ Y✝) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).inverse.map f).right = f.right

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_right {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L')) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).inverse.obj X).right = X.right

@[simp]

theorem CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_unitIso_hom_app_right_app {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) (X : Comma (fromPUnit F) ((whiskeringLeft C D H).obj L)) (X✝ : D) : ((leftExtensionEquivalenceOfIso₁ iso₁ F).unitIso.hom.app X).right.app X✝ = CategoryStruct.id (X.right.obj X✝)

theorem CategoryTheory.Functor.hasLeftExtension_iff_of_iso₁ {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L L' : Functor C D} (iso₁ : L ≅ L') (F : Functor C H) : L.HasLeftKanExtension F ↔ L'.HasLeftKanExtension F

def CategoryTheory.Functor.rightExtensionEquivalenceOfIso₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) {F F' : Functor C H} (iso₂ : F ≅ F') : L.RightExtension F ≌ L.RightExtension F'

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

theorem CategoryTheory.Functor.hasRightExtension_iff_of_iso₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) {F F' : Functor C H} (iso₂ : F ≅ F') : L.HasRightKanExtension F ↔ L.HasRightKanExtension F'

def CategoryTheory.Functor.leftExtensionEquivalenceOfIso₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) {F F' : Functor C H} (iso₂ : F ≅ F') : L.LeftExtension F ≌ L.LeftExtension F'

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

theorem CategoryTheory.Functor.hasLeftExtension_iff_of_iso₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (L : Functor C D) {F F' : Functor C H} (iso₂ : F ≅ F') : L.HasLeftKanExtension F ↔ L.HasLeftKanExtension F'

noncomputable def CategoryTheory.Functor.LeftExtension.isUniversalEquivOfIso₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L : Functor C D} {F₁ F₂ : Functor C H} (α₁ : L.LeftExtension F₁) (α₂ : L.LeftExtension F₂) (e : F₁ ≅ F₂) (e' : α₁.right ≅ α₂.right) (h : CategoryStruct.comp α₁.hom (L.whiskerLeft e'.hom) = CategoryStruct.comp e.hom α₂.hom) : StructuredArrow.IsUniversal α₁ ≃ StructuredArrow.IsUniversal α₂

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.

theorem CategoryTheory.Functor.isLeftKanExtension_iff_of_iso₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L : Functor C D} {F₁ F₂ : Functor C H} {F₁' F₂' : Functor D H} (α₁ : F₁ ⟶ L.comp F₁') (α₂ : F₂ ⟶ L.comp F₂') (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂') (h : CategoryStruct.comp α₁ (L.whiskerLeft e'.hom) = CategoryStruct.comp e.hom α₂) : F₁'.IsLeftKanExtension α₁ ↔ F₂'.IsLeftKanExtension α₂

noncomputable def CategoryTheory.Functor.RightExtension.isUniversalEquivOfIso₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L : Functor C D} {F₁ F₂ : Functor C H} (α₁ : L.RightExtension F₁) (α₂ : L.RightExtension F₂) (e : F₁ ≅ F₂) (e' : α₁.left ≅ α₂.left) (h : CategoryStruct.comp (L.whiskerLeft e'.hom) α₂.hom = CategoryStruct.comp α₁.hom e.hom) : CostructuredArrow.IsUniversal α₁ ≃ CostructuredArrow.IsUniversal α₂

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.

theorem CategoryTheory.Functor.isRightKanExtension_iff_of_iso₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L : Functor C D} {F₁ F₂ : Functor C H} {F₁' F₂' : Functor D H} (α₁ : L.comp F₁' ⟶ F₁) (α₂ : L.comp F₂' ⟶ F₂) (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂') (h : CategoryStruct.comp (L.whiskerLeft e'.hom) α₂ = CategoryStruct.comp α₁ e.hom) : F₁'.IsRightKanExtension α₁ ↔ F₂'.IsRightKanExtension α₂

def CategoryTheory.Functor.LeftExtension.precomp₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {F₀ : Functor C H} {L : Functor C D} {F₁ : Functor D H} (L' : Functor D D') (α : F₀ ⟶ L.comp F₁) : Functor (L'.LeftExtension F₁) ((L.comp L').LeftExtension F₀)

A variant of LeftExtension.precomp where we precompose, and then "whisker" the diagram by a given natural transformation (α : F₀ ⟶ L ⋙ F₁)

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp₂_map_left {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {F₀ : Functor C H} {L : Functor C D} {F₁ : Functor D H} (L' : Functor D D') (α : F₀ ⟶ L.comp F₁) {X✝ Y✝ : L'.LeftExtension F₁} (f : X✝ ⟶ Y✝) : ((precomp₂ L' α).map f).left = CategoryStruct.id X✝.left

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp₂_obj_left {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {F₀ : Functor C H} {L : Functor C D} {F₁ : Functor D H} (L' : Functor D D') (α : F₀ ⟶ L.comp F₁) (X : L'.LeftExtension F₁) : ((precomp₂ L' α).obj X).left = X.left

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp₂_obj_hom_app {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {F₀ : Functor C H} {L : Functor C D} {F₁ : Functor D H} (L' : Functor D D') (α : F₀ ⟶ L.comp F₁) (X : L'.LeftExtension F₁) (X✝ : C) : ((precomp₂ L' α).obj X).hom.app X✝ = CategoryStruct.comp (α.app X✝) (X.hom.app (L.obj X✝))

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp₂_obj_right {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {F₀ : Functor C H} {L : Functor C D} {F₁ : Functor D H} (L' : Functor D D') (α : F₀ ⟶ L.comp F₁) (X : L'.LeftExtension F₁) : ((precomp₂ L' α).obj X).right = X.right

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp₂_map_right {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {F₀ : Functor C H} {L : Functor C D} {F₁ : Functor D H} (L' : Functor D D') (α : F₀ ⟶ L.comp F₁) {X✝ Y✝ : L'.LeftExtension F₁} (f : X✝ ⟶ Y✝) : ((precomp₂ L' α).map f).right = f.right

def CategoryTheory.Functor.LeftExtension.isUniversalPrecomp₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor D D'} {F₀ : Functor C H} {F₁ : Functor D H} (α : F₀ ⟶ L.comp F₁) (hα : StructuredArrow.IsUniversal (mk F₁ α)) {b : L'.LeftExtension F₁} (hb : StructuredArrow.IsUniversal b) : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)

If the right extension defined by α : F₀ ⟶ L ⋙ F₁ is universal, then for every L' : D ⥤ D', F₁ : D ⥤ H, if an extension b : L'.LeftExtension F₁ is universal, so is the "pasted" extension (LeftExtension.precomp₂ L' α).obj b.

def CategoryTheory.Functor.LeftExtension.isUniversalOfPrecomp₂ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor D D'} {F₀ : Functor C H} {F₁ : Functor D H} (α : F₀ ⟶ L.comp F₁) (hα : StructuredArrow.IsUniversal (mk F₁ α)) {b : L'.LeftExtension F₁} (hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)) : StructuredArrow.IsUniversal b

If the left extension defined by α : F₀ ⟶ L ⋙ F₁ is universal, then for every L' : D ⥤ D', F₁ : D ⥤ H, if an extension b : L'.LeftExtension F₁ is such that the "pasted" extension (LeftExtension.precomp₂ L' α).obj b is universal, then b is itself universal.

def CategoryTheory.Functor.LeftExtension.isUniversalPrecomp₂Equiv {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor D D'} {F₀ : Functor C H} {F₁ : Functor D H} (α : F₀ ⟶ L.comp F₁) (hα : StructuredArrow.IsUniversal (mk F₁ α)) (b : L'.LeftExtension F₁) : StructuredArrow.IsUniversal b ≃ StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)

If the left extension defined by α : F₀ ⟶ L ⋙ F₁ is universal, then for every L' : D ⥤ D', F₁ : D ⥤ H, an extension b : L'.LeftExtension F₁ is universal if and only if (LeftExtension.precomp₂ L' α).obj b is universal.

theorem CategoryTheory.Functor.isLeftKanExtension_iff_postcompose {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] [Category.{v_5, u_5} D'] {L : Functor C D} {L' : Functor D D'} {F₀ : Functor C H} {F₁ : Functor D H} (α : F₀ ⟶ L.comp F₁) [F₁.IsLeftKanExtension α] {F₂ : Functor D' H} (L'' : Functor C D') (e : L.comp L' ≅ L'') (β : F₁ ⟶ L'.comp F₂) (γ : F₀ ⟶ L''.comp F₂) (hγ : CategoryStruct.comp α (CategoryStruct.comp (L.whiskerLeft β) (CategoryStruct.comp (L.associator L' F₂).inv (whiskerRight e.hom F₂))) = γ := by aesop_cat) : F₂.IsLeftKanExtension β ↔ F₂.IsLeftKanExtension γ

noncomputable def CategoryTheory.Functor.coconeOfIsLeftKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (c : Limits.Cocone F) : Limits.Cocone F'

Construct a cocone for a left Kan extension F' : D ⥤ H of F : C ⥤ H along a functor L : C ⥤ D given a cocone for F.

@[simp]

theorem CategoryTheory.Functor.coconeOfIsLeftKanExtension_ι {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (c : Limits.Cocone F) : (F'.coconeOfIsLeftKanExtension α c).ι = F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι

@[simp]

theorem CategoryTheory.Functor.coconeOfIsLeftKanExtension_pt {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (c : Limits.Cocone F) : (F'.coconeOfIsLeftKanExtension α c).pt = c.pt

noncomputable def CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] {c : Limits.Cocone F} (hc : Limits.IsColimit c) : Limits.IsColimit (F'.coconeOfIsLeftKanExtension α c)

If c is a colimit cocone for a functor F : C ⥤ H and α : F ⟶ L ⋙ F' is the unit of any left Kan extension F' : D ⥤ H of F along L : C ⥤ D, then coconeOfIsLeftKanExtension α c is a colimit cocone, too.

@[simp]

theorem CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtension_desc {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] {c : Limits.Cocone F} (hc : Limits.IsColimit c) (s : Limits.Cocone F') : (F'.isColimitCoconeOfIsLeftKanExtension α hc).desc s = hc.desc { pt := s.1, ι := CategoryStruct.comp α (L.whiskerLeft s.ι) }

noncomputable def CategoryTheory.Functor.colimitIsoOfIsLeftKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] [Limits.HasColimit F] [Limits.HasColimit F'] : Limits.colimit F' ≅ Limits.colimit F

If F' : D ⥤ H is a left Kan extension of F : C ⥤ H along L : C ⥤ D, the colimit over F' is isomorphic to the colimit over F.

@[simp]

theorem CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_hom {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] [Limits.HasColimit F] [Limits.HasColimit F'] (i : C) : CategoryStruct.comp (α.app i) (CategoryStruct.comp (Limits.colimit.ι F' (L.obj i)) (F'.colimitIsoOfIsLeftKanExtension α).hom) = Limits.colimit.ι F i

@[simp]

theorem CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_hom_assoc {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] [Limits.HasColimit F] [Limits.HasColimit F'] (i : C) {Z : H} (h : Limits.colimit F ⟶ Z) : CategoryStruct.comp (α.app i) (CategoryStruct.comp (Limits.colimit.ι F' (L.obj i)) (CategoryStruct.comp (F'.colimitIsoOfIsLeftKanExtension α).hom h)) = CategoryStruct.comp (Limits.colimit.ι F i) h

@[simp]

theorem CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] [Limits.HasColimit F] [Limits.HasColimit F'] (i : C) : CategoryStruct.comp (Limits.colimit.ι F i) (F'.colimitIsoOfIsLeftKanExtension α).inv = CategoryStruct.comp (α.app i) (Limits.colimit.ι F' (L.obj i))

@[simp]

theorem CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv_assoc {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] [Limits.HasColimit F] [Limits.HasColimit F'] (i : C) {Z : H} (h : Limits.colimit F' ⟶ Z) : CategoryStruct.comp (Limits.colimit.ι F i) (CategoryStruct.comp (F'.colimitIsoOfIsLeftKanExtension α).inv h) = CategoryStruct.comp (α.app i) (CategoryStruct.comp (Limits.colimit.ι F' (L.obj i)) h)

noncomputable def CategoryTheory.Functor.coneOfIsRightKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (c : Limits.Cone F) : Limits.Cone F'

Construct a cone for a right Kan extension F' : D ⥤ H of F : C ⥤ H along a functor L : C ⥤ D given a cone for F.

@[simp]

theorem CategoryTheory.Functor.coneOfIsRightKanExtension_pt {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (c : Limits.Cone F) : (F'.coneOfIsRightKanExtension α c).pt = c.pt

@[simp]

theorem CategoryTheory.Functor.coneOfIsRightKanExtension_π {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (c : Limits.Cone F) : (F'.coneOfIsRightKanExtension α c).π = F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π

noncomputable def CategoryTheory.Functor.isLimitConeOfIsRightKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] {c : Limits.Cone F} (hc : Limits.IsLimit c) : Limits.IsLimit (F'.coneOfIsRightKanExtension α c)

If c is a limit cone for a functor F : C ⥤ H and α : L ⋙ F' ⟶ F is the counit of any right Kan extension F' : D ⥤ H of F along L : C ⥤ D, then coneOfIsRightKanExtension α c is a limit cone, too.

@[simp]

theorem CategoryTheory.Functor.isLimitConeOfIsRightKanExtension_lift {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] {c : Limits.Cone F} (hc : Limits.IsLimit c) (s : Limits.Cone F') : (F'.isLimitConeOfIsRightKanExtension α hc).lift s = hc.lift { pt := s.1, π := CategoryStruct.comp (L.whiskerLeft s.π) α }

noncomputable def CategoryTheory.Functor.limitIsoOfIsRightKanExtension {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] [Limits.HasLimit F] [Limits.HasLimit F'] : Limits.limit F' ≅ Limits.limit F

If F' : D ⥤ H is a right Kan extension of F : C ⥤ H along L : C ⥤ D, the limit over F' is isomorphic to the limit over F.

@[simp]

theorem CategoryTheory.Functor.limitIsoOfIsRightKanExtension_inv_π {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] [Limits.HasLimit F] [Limits.HasLimit F'] (i : C) : CategoryStruct.comp (F'.limitIsoOfIsRightKanExtension α).inv (CategoryStruct.comp (Limits.limit.π F' (L.obj i)) (α.app i)) = Limits.limit.π F i

@[simp]

theorem CategoryTheory.Functor.limitIsoOfIsRightKanExtension_inv_π_assoc {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] [Limits.HasLimit F] [Limits.HasLimit F'] (i : C) {Z : H} (h : F.obj i ⟶ Z) : CategoryStruct.comp (F'.limitIsoOfIsRightKanExtension α).inv (CategoryStruct.comp (Limits.limit.π F' (L.obj i)) (CategoryStruct.comp (α.app i) h)) = CategoryStruct.comp (Limits.limit.π F i) h

@[simp]

theorem CategoryTheory.Functor.limitIsoOfIsRightKanExtension_hom_π {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] [Limits.HasLimit F] [Limits.HasLimit F'] (i : C) : CategoryStruct.comp (F'.limitIsoOfIsRightKanExtension α).hom (Limits.limit.π F i) = CategoryStruct.comp (Limits.limit.π F' (L.obj i)) (α.app i)

@[simp]

theorem CategoryTheory.Functor.limitIsoOfIsRightKanExtension_hom_π_assoc {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] (F' : Functor D H) {L : Functor C D} {F : Functor C H} (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] [Limits.HasLimit F] [Limits.HasLimit F'] (i : C) {Z : H} (h : F.obj i ⟶ Z) : CategoryStruct.comp (F'.limitIsoOfIsRightKanExtension α).hom (CategoryStruct.comp (Limits.limit.π F i) h) = CategoryStruct.comp (Limits.limit.π F' (L.obj i)) (CategoryStruct.comp (α.app i) h)

instance CategoryTheory.Functor.isLeftKanExtensionId {C : Type u_1} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] (F₀ : Functor C H) : F₀.IsLeftKanExtension F₀.leftUnitor.inv

instance CategoryTheory.Functor.isRightKanExtensionId {C : Type u_1} {H : Type u_3} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] (F₀ : Functor C H) : F₀.IsRightKanExtension F₀.leftUnitor.hom

instance CategoryTheory.Functor.isLeftKanExtensionAlongEquivalence {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L : C ≌ D} {F₀ : Functor C H} {F₁ : Functor D H} (α : F₀ ≅ L.functor.comp F₁) : F₁.IsLeftKanExtension α.hom

instance CategoryTheory.Functor.isLeftKanExtensionAlongEquivalence' {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {F₀ : Functor C H} {F₁ : Functor D H} (L : Functor C D) (α : F₀ ⟶ L.comp F₁) [L.IsEquivalence] [IsIso α] : F₁.IsLeftKanExtension α

instance CategoryTheory.Functor.isRightKanExtensionAlongEquivalence {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {L : C ≌ D} {F₀ : Functor C H} {F₁ : Functor D H} (α : L.functor.comp F₁ ≅ F₀) : F₁.IsRightKanExtension α.hom

instance CategoryTheory.Functor.isRightKanExtensionAlongEquivalence' {C : Type u_1} {H : Type u_3} {D : Type u_4} [Category.{v_1, u_1} C] [Category.{v_3, u_3} H] [Category.{v_4, u_4} D] {F₀ : Functor C H} {F₁ : Functor D H} (L : Functor C D) (α : L.comp F₁ ⟶ F₀) [L.IsEquivalence] [IsIso α] : F₁.IsRightKanExtension α