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

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

@[reducible, inline]

abbrev CategoryTheory.Functor.RightExtension {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) : Type (max (max (max (max u_3 u_5) u_8) u_9) u_1 u_8)

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

• L.RightExtension F = CategoryTheory.CostructuredArrow ((CategoryTheory.whiskeringLeft C D H).obj L) F

@[reducible, inline]

abbrev CategoryTheory.Functor.LeftExtension {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) : Type (max (max (max (max u_3 u_5) u_8) u_9) u_1 u_8)

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

• L.LeftExtension F = CategoryTheory.StructuredArrow F ((CategoryTheory.whiskeringLeft C D H).obj L)

@[simp]

theorem CategoryTheory.Functor.RightExtension.mk_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) : (CategoryTheory.Functor.RightExtension.mk F' α).hom = α

@[simp]

theorem CategoryTheory.Functor.RightExtension.mk_left {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) : (CategoryTheory.Functor.RightExtension.mk F' α).left = F'

@[simp]

theorem CategoryTheory.Functor.RightExtension.mk_right_as {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) : (CategoryTheory.Functor.RightExtension.mk F' α).right.as = PUnit.unit

def CategoryTheory.Functor.RightExtension.mk {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) : L.RightExtension F

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

Equations

• CategoryTheory.Functor.RightExtension.mk F' α = CategoryTheory.CostructuredArrow.mk α

@[simp]

theorem CategoryTheory.Functor.LeftExtension.mk_right {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') : (CategoryTheory.Functor.LeftExtension.mk F' α).right = F'

@[simp]

theorem CategoryTheory.Functor.LeftExtension.mk_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') : (CategoryTheory.Functor.LeftExtension.mk F' α).hom = α

@[simp]

theorem CategoryTheory.Functor.LeftExtension.mk_left_as {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') : (CategoryTheory.Functor.LeftExtension.mk F' α).left.as = PUnit.unit

def CategoryTheory.Functor.LeftExtension.mk {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') : L.LeftExtension F

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

Equations

• CategoryTheory.Functor.LeftExtension.mk F' α = CategoryTheory.StructuredArrow.mk α

class CategoryTheory.Functor.IsRightKanExtension {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) : 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 (CategoryTheory.CostructuredArrow.IsUniversal (CategoryTheory.Functor.RightExtension.mk F' α))

theorem CategoryTheory.Functor.IsRightKanExtension.nonempty_isUniversal {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} [self : F'.IsRightKanExtension α] : Nonempty (CategoryTheory.CostructuredArrow.IsUniversal (CategoryTheory.Functor.RightExtension.mk F' α))

noncomputable def CategoryTheory.Functor.isUniversalOfIsRightKanExtension {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 α] : CategoryTheory.CostructuredArrow.IsUniversal (CategoryTheory.Functor.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.

Equations

• F'.isUniversalOfIsRightKanExtension α = ⋯.some

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

• F'.liftOfIsRightKanExtension α G β = (F'.isUniversalOfIsRightKanExtension α).lift (CategoryTheory.Functor.RightExtension.mk G β)

@[simp]

theorem CategoryTheory.Functor.liftOfIsRightKanExtension_fac_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) {Z : CategoryTheory.Functor C H} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L (F'.liftOfIsRightKanExtension α G β)) (CategoryTheory.CategoryStruct.comp α h) = CategoryTheory.CategoryStruct.comp β h

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

theorem CategoryTheory.Functor.hom_ext_of_isRightKanExtension {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} (γ₁ : G ⟶ F') (γ₂ : G ⟶ F') (hγ : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L γ₁) α = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L γ₂) α) : γ₁ = γ₂

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.

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

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

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.

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

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

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

• F'.rightKanExtensionUnique α F'' α' = F'.rightKanExtensionUniqueOfIso α (CategoryTheory.Iso.refl F) F'' α'

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 φ

class CategoryTheory.Functor.IsLeftKanExtension {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') : 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 (CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.LeftExtension.mk F' α))

theorem CategoryTheory.Functor.IsLeftKanExtension.nonempty_isUniversal {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'} [self : F'.IsLeftKanExtension α] : Nonempty (CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.LeftExtension.mk F' α))

noncomputable def CategoryTheory.Functor.isUniversalOfIsLeftKanExtension {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 α] : CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.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.

Equations

• F'.isUniversalOfIsLeftKanExtension α = ⋯.some

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

• F'.descOfIsLeftKanExtension α G β = (F'.isUniversalOfIsLeftKanExtension α).desc (CategoryTheory.Functor.LeftExtension.mk G β)

@[simp]

theorem CategoryTheory.Functor.descOfIsLeftKanExtension_fac_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) {Z : CategoryTheory.Functor C H} (h : L.comp G ⟶ Z) : CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L (F'.descOfIsLeftKanExtension α G β)) h) = CategoryTheory.CategoryStruct.comp β h

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

theorem CategoryTheory.Functor.hom_ext_of_isLeftKanExtension {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' ⟶ G) (γ₂ : F' ⟶ G) (hγ : CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L γ₁) = CategoryTheory.CategoryStruct.comp α (CategoryTheory.whiskerLeft L γ₂)) : γ₁ = γ₂

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.

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

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

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.

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

• F'.leftKanExtensionUnique α F'' α' = F'.leftKanExtensionUniqueOfIso α (CategoryTheory.Iso.refl F) F'' α'

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]

abbrev CategoryTheory.Functor.HasRightKanExtension {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) : Prop

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

Equations

• L.HasRightKanExtension F = CategoryTheory.Limits.HasTerminal (L.RightExtension F)

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]

abbrev CategoryTheory.Functor.HasLeftKanExtension {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) : Prop

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

Equations

• L.HasLeftKanExtension F = CategoryTheory.Limits.HasInitial (L.LeftExtension F)

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

noncomputable def CategoryTheory.Functor.rightKanExtension {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] : CategoryTheory.Functor D H

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

Equations

• L.rightKanExtension F = (⊤_ L.RightExtension F).left

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

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 {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)) : γ₁ = γ₂

noncomputable def CategoryTheory.Functor.leftKanExtension {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] : CategoryTheory.Functor D H

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

Equations

• L.leftKanExtension F = (⊥_ L.LeftExtension F).right

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

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 {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 γ₂)) : γ₁ = γ₂

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcomp₁_obj_right_obj {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_10, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') (f : L' ⟶ L.comp G) (F : CategoryTheory.Functor C H) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D' H).obj L')) (X : D) : ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).obj X✝).right.obj X = X✝.right.obj (G.obj X)

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcomp₁_obj_right_map {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_10, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') (f : L' ⟶ L.comp G) (F : CategoryTheory.Functor C H) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D' H).obj L')) : ∀ {X_1 Y : D} (f_1 : X_1 ⟶ Y), ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).obj X).right.map f_1 = X.right.map (G.map f_1)

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.LeftExtension.postcomp₁_obj_left {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_10, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') (f : L' ⟶ L.comp G) (F : CategoryTheory.Functor C H) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D' H).obj L')) : ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).obj X).left = X.left

@[simp]

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

def CategoryTheory.Functor.LeftExtension.postcomp₁ {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_10, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') (f : L' ⟶ L.comp G) (F : CategoryTheory.Functor C H) : CategoryTheory.Functor (L'.LeftExtension F) (L.LeftExtension F)

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

Equations

• CategoryTheory.Functor.LeftExtension.postcomp₁ G f F = CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id F) ((CategoryTheory.whiskeringLeft C D' H).map f)

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcomp₁_obj_left_map {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_10, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') (f : L.comp G ⟶ L') (F : CategoryTheory.Functor C H) (X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)) : ∀ {X_1 Y : D} (f_1 : X_1 ⟶ Y), ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).obj X).left.map f_1 = X.left.map (G.map f_1)

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcomp₁_obj_right {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_10, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') (f : L.comp G ⟶ L') (F : CategoryTheory.Functor C H) (X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)) : ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).obj X).right = X.right

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.RightExtension.postcomp₁_map_left_app {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_10, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') (f : L.comp G ⟶ L') (F : CategoryTheory.Functor C H) {X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)} {Y : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)} (φ : X✝ ⟶ Y) (X : D) : ((CategoryTheory.Functor.RightExtension.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_5} {D' : Type u_6} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_10, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') (f : L.comp G ⟶ L') (F : CategoryTheory.Functor C H) (X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)) (X : D) : ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).obj X✝).left.obj X = X✝.left.obj (G.obj X)

@[simp]

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

def CategoryTheory.Functor.RightExtension.postcomp₁ {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_10, u_6} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'} (G : CategoryTheory.Functor D D') (f : L.comp G ⟶ L') (F : CategoryTheory.Functor C H) : CategoryTheory.Functor (L'.RightExtension F) (L.RightExtension F)

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.

noncomputable instance CategoryTheory.Functor.instIsEquivalenceLeftExtensionPostcomp₁OfIsIso {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] (f : L' ⟶ L.comp G) [CategoryTheory.IsIso f] (F : CategoryTheory.Functor C H) : (CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).IsEquivalence

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.Functor.instIsEquivalenceRightExtensionPostcomp₁OfIsIso {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] (f : L.comp G ⟶ L') [CategoryTheory.IsIso f] (F : CategoryTheory.Functor C H) : (CategoryTheory.Functor.RightExtension.postcomp₁ G f F).IsEquivalence

Equations

• ⋯ = ⋯

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_7, u_1} C] [CategoryTheory.Category.{u_8, 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) : 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_7, u_1} C] [CategoryTheory.Category.{u_8, 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) : L'.HasRightKanExtension F ↔ L.HasRightKanExtension F

noncomputable def CategoryTheory.Functor.LeftExtension.isUniversalPostcomp₁Equiv {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_10, 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) (ex : L'.LeftExtension F) : CategoryTheory.StructuredArrow.IsUniversal ex ≃ CategoryTheory.StructuredArrow.IsUniversal ((CategoryTheory.Functor.LeftExtension.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.

Equations

• CategoryTheory.Functor.LeftExtension.isUniversalPostcomp₁Equiv G e F ex = CategoryTheory.Limits.IsInitial.isInitialIffObj (CategoryTheory.Functor.LeftExtension.postcomp₁ G e.inv F) ex

noncomputable def CategoryTheory.Functor.RightExtension.isUniversalPostcomp₁Equiv {C : Type u_1} {H : Type u_3} {D : Type u_5} {D' : Type u_6} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] [CategoryTheory.Category.{u_10, 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) (ex : L'.RightExtension F) : CategoryTheory.CostructuredArrow.IsUniversal ex ≃ CategoryTheory.CostructuredArrow.IsUniversal ((CategoryTheory.Functor.RightExtension.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.

Equations

• CategoryTheory.Functor.RightExtension.isUniversalPostcomp₁Equiv G e F ex = CategoryTheory.Limits.IsTerminal.isTerminalIffObj (CategoryTheory.Functor.RightExtension.postcomp₁ G e.hom F) ex

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

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp_obj_right {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D H).obj L)) : ((CategoryTheory.Functor.LeftExtension.precomp L F G).obj X).right = X.right

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp_obj_hom_app {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D H).obj L)) (X : C') : ((CategoryTheory.Functor.LeftExtension.precomp L F G).obj X✝).hom.app X = X✝.hom.app (G.obj X)

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp_map_right {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) {X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D H).obj L)} {Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D H).obj L)} (φ : X ⟶ Y) : ((CategoryTheory.Functor.LeftExtension.precomp L F G).map φ).right = φ.right

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.LeftExtension.precomp_obj_left {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.whiskeringLeft C D H).obj L)) : ((CategoryTheory.Functor.LeftExtension.precomp L F G).obj X).left = X.left

def CategoryTheory.Functor.LeftExtension.precomp {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) : CategoryTheory.Functor (L.LeftExtension F) ((G.comp L).LeftExtension (G.comp 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.

@[simp]

theorem CategoryTheory.Functor.RightExtension.precomp_map_right {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) {X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)} {Y : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)} (φ : X ⟶ Y) : ((CategoryTheory.Functor.RightExtension.precomp L F G).map φ).right = CategoryTheory.CategoryStruct.id 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_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) {X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)} {Y : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)} (φ : X ⟶ Y) : ((CategoryTheory.Functor.RightExtension.precomp L F G).map φ).left = φ.left

@[simp]

theorem CategoryTheory.Functor.RightExtension.precomp_obj_hom_app {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) (X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)) (X : C') : ((CategoryTheory.Functor.RightExtension.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_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) (X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)) : ((CategoryTheory.Functor.RightExtension.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_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) (X : CategoryTheory.Comma ((CategoryTheory.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)) : ((CategoryTheory.Functor.RightExtension.precomp L F G).obj X).right = X.right

def CategoryTheory.Functor.RightExtension.precomp {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) : CategoryTheory.Functor (L.RightExtension F) ((G.comp L).RightExtension (G.comp F))

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.

noncomputable instance CategoryTheory.Functor.instIsEquivalenceLeftExtensionCompPrecomp {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_10, u_2} C'] [CategoryTheory.Category.{u_7, u_3} H] [CategoryTheory.Category.{u_8, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] : (CategoryTheory.Functor.LeftExtension.precomp L F G).IsEquivalence

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.Functor.instIsEquivalenceRightExtensionCompPrecomp {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_9, u_1} C] [CategoryTheory.Category.{u_10, u_2} C'] [CategoryTheory.Category.{u_7, u_3} H] [CategoryTheory.Category.{u_8, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] : (CategoryTheory.Functor.RightExtension.precomp L F G).IsEquivalence

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Functor.LeftExtension.isUniversalPrecompEquiv {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] (e : L.LeftExtension F) : CategoryTheory.StructuredArrow.IsUniversal e ≃ CategoryTheory.StructuredArrow.IsUniversal ((CategoryTheory.Functor.LeftExtension.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.

Equations

• CategoryTheory.Functor.LeftExtension.isUniversalPrecompEquiv L F G e = CategoryTheory.Limits.IsInitial.isInitialIffObj (CategoryTheory.Functor.LeftExtension.precomp L F G) e

noncomputable def CategoryTheory.Functor.RightExtension.isUniversalPrecompEquiv {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_8, u_2} C'] [CategoryTheory.Category.{u_9, u_3} H] [CategoryTheory.Category.{u_10, u_5} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] (e : L.RightExtension F) : CategoryTheory.CostructuredArrow.IsUniversal e ≃ CategoryTheory.CostructuredArrow.IsUniversal ((CategoryTheory.Functor.RightExtension.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.

Equations

• CategoryTheory.Functor.RightExtension.isUniversalPrecompEquiv L F G e = CategoryTheory.Limits.IsTerminal.isTerminalIffObj (CategoryTheory.Functor.RightExtension.precomp L F G) e

theorem CategoryTheory.Functor.isLeftKanExtension_iff_precomp {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_5} [CategoryTheory.Category.{u_8, u_1} C] [CategoryTheory.Category.{u_10, u_2} C'] [CategoryTheory.Category.{u_7, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (F' : CategoryTheory.Functor D H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] (α : F ⟶ L.comp F') : F'.IsLeftKanExtension α ↔ F'.IsLeftKanExtension (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G α) (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_5} [CategoryTheory.Category.{u_8, u_1} C] [CategoryTheory.Category.{u_10, u_2} C'] [CategoryTheory.Category.{u_7, u_3} H] [CategoryTheory.Category.{u_9, u_5} D] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (F' : CategoryTheory.Functor D H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] (α : L.comp F' ⟶ F) : F'.IsRightKanExtension α ↔ F'.IsRightKanExtension (CategoryTheory.CategoryStruct.comp (G.associator L F').hom (CategoryTheory.whiskerLeft G α))

def CategoryTheory.Functor.rightExtensionEquivalenceOfIso₁ {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} {L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H) : L.RightExtension F ≌ L'.RightExtension F

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

Equations

• CategoryTheory.Functor.rightExtensionEquivalenceOfIso₁ iso₁ F = CategoryTheory.CostructuredArrow.mapNatIso ((CategoryTheory.whiskeringLeft C D H).mapIso iso₁)

theorem CategoryTheory.Functor.hasRightExtension_iff_of_iso₁ {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} {L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H) : L.HasRightKanExtension F ↔ L'.HasRightKanExtension F

def CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ {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} {L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H) : L.LeftExtension F ≌ L'.LeftExtension F

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

Equations

• CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F = CategoryTheory.StructuredArrow.mapNatIso ((CategoryTheory.whiskeringLeft C D H).mapIso iso₁)

theorem CategoryTheory.Functor.hasLeftExtension_iff_of_iso₁ {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} {L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H) : L.HasLeftKanExtension F ↔ L'.HasLeftKanExtension F

def CategoryTheory.Functor.rightExtensionEquivalenceOfIso₂ {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} {F' : CategoryTheory.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'.

Equations

• L.rightExtensionEquivalenceOfIso₂ iso₂ = CategoryTheory.CostructuredArrow.mapIso iso₂

theorem CategoryTheory.Functor.hasRightExtension_iff_of_iso₂ {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} {F' : CategoryTheory.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_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} {F' : CategoryTheory.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'.

Equations

• L.leftExtensionEquivalenceOfIso₂ iso₂ = CategoryTheory.StructuredArrow.mapIso iso₂

theorem CategoryTheory.Functor.hasLeftExtension_iff_of_iso₂ {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} {F' : CategoryTheory.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_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} {F₂ : CategoryTheory.Functor C H} (α₁ : L.LeftExtension F₁) (α₂ : L.LeftExtension F₂) (e : F₁ ≅ F₂) (e' : α₁.right ≅ α₂.right) (h : CategoryTheory.CategoryStruct.comp α₁.hom (CategoryTheory.whiskerLeft L e'.hom) = CategoryTheory.CategoryStruct.comp e.hom α₂.hom) : CategoryTheory.StructuredArrow.IsUniversal α₁ ≃ CategoryTheory.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.

Equations

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

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 α₂

noncomputable def CategoryTheory.Functor.RightExtension.isUniversalEquivOfIso₂ {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} {F₂ : CategoryTheory.Functor C H} (α₁ : L.RightExtension F₁) (α₂ : L.RightExtension F₂) (e : F₁ ≅ F₂) (e' : α₁.left ≅ α₂.left) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L e'.hom) α₂.hom = CategoryTheory.CategoryStruct.comp α₁.hom e.hom) : CategoryTheory.CostructuredArrow.IsUniversal α₁ ≃ CategoryTheory.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.

Equations

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

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 α₂