Preservation of Kan extensions

Given functors F : A ⥤ B, L : B ⥤ C, and G : B ⥤ D, we introduce a typeclass G.PreservesLeftKanExtension F L which encodes the fact that the left Kan extension of F along L is preserved by the functor G.

When the Kan extension is pointwise, it suffices that G preserves (co)limits of the relevant diagrams.

We introduce the dual typeclass G.PreservesRightKanExtension.

class CategoryTheory.Functor.PreservesLeftKanExtension {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) : Prop

G.PreservesLeftKanExtension F L asserts that G preserves all left Kan extensions of F along L. See PreservesLeftKanExtension.mk_of_preserves_isLeftKanExtension for a constructor taking a single left Kan extension as input.

• preserves (F' : Functor C B) (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] : (F'.comp G).IsLeftKanExtension (CategoryStruct.comp (whiskerRight α G) (L.associator F' G).hom)

theorem CategoryTheory.Functor.PreservesLeftKanExtension.mk' {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (preserves : ∀ {E : L.LeftExtension F} (a : StructuredArrow.IsUniversal E), Nonempty (StructuredArrow.IsUniversal ((LeftExtension.postcompose₂ L F G).obj E))) : G.PreservesLeftKanExtension F L

Alternative constructor for PreservesLeftKanExtension, phrased in terms of LeftExtension.IsUniversal instead. See PreservesLeftKanExtension.mk_of_preserves_isUniversal for a similar constructor taking as input a single LeftExtension.

theorem CategoryTheory.Functor.PreservesLeftKanExtension.mk_of_preserves_isLeftKanExtension {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_7, u_1} A] [Category.{u_6, u_2} B] [Category.{u_5, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (F' : Functor C B) (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] (h : (F'.comp G).IsLeftKanExtension (CategoryStruct.comp (whiskerRight α G) (L.associator F' G).hom)) : G.PreservesLeftKanExtension F L

Show that G preserves left Kan extensions if it maps some left Kan extension to a left Kan extension.

theorem CategoryTheory.Functor.PreservesLeftKanExtension.mk_of_preserves_isUniversal {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (E : L.LeftExtension F) (hE : StructuredArrow.IsUniversal E) (h : Nonempty (StructuredArrow.IsUniversal ((LeftExtension.postcompose₂ L F G).obj E))) : G.PreservesLeftKanExtension F L

Show that G preserves left Kan extensions if it maps some left Kan extension to a left Kan extension, phrased in terms of IsUniversal.

class CategoryTheory.Functor.PreservesPointwiseLeftKanExtensionAt {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (c : C) : Prop

G.PreservesLeftKanExtensionAt F L c asserts that G preserves all pointwise left Kan extensions of F along L at the point c.

• preserves (E : L.LeftExtension F) : ∀ (a : E.IsPointwiseLeftKanExtensionAt c), Nonempty (((LeftExtension.postcompose₂ L F G).obj E).IsPointwiseLeftKanExtensionAt c)

  G preserves every pointwise extensions of F along L at c.

@[reducible, inline]

abbrev CategoryTheory.Functor.PreservesPointwiseLeftKanExtension {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) : Prop

G.PreservesLeftKanExtension F L asserts that G preserves all pointwise left Kan extensions of F along L.

def CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.postcompose {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) {F : Functor A B} {L : Functor A C} {c : C} [G.PreservesPointwiseLeftKanExtensionAt F L c] {E : L.LeftExtension F} (hE : E.IsPointwiseLeftKanExtensionAt c) : ((postcompose₂ L F G).obj E).IsPointwiseLeftKanExtensionAt c

Given a pointwise left Kan extension of F along L at c, exhibits (LeftExtension.whiskerRight L F G).obj E as a pointwise left Kan extension of F ⋙ G along L at c.

def CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.postcompose {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) {F : Functor A B} {L : Functor A C} [G.PreservesPointwiseLeftKanExtension F L] {E : L.LeftExtension F} (hE : E.IsPointwiseLeftKanExtension) : ((postcompose₂ L F G).obj E).IsPointwiseLeftKanExtension

Given a pointwise left Kan extension of F along L, exhibits (LeftExtension.whiskerRight L F G).obj E as a pointwise left Kan extension of F ⋙ G along L.

def CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (E : L.LeftExtension F) (c : C) : ((postcompose₂ L F G).obj E).coconeAt c ≅ G.mapCocone (E.coconeAt c)

The cocone at a point of the whiskering right by Gof an extension is isomorphic to the action of G on the cocone at that point for the original extension.

@[simp]

theorem CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso_inv_hom {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (E : L.LeftExtension F) (c : C) : (coconeAtWhiskerRightIso G F L E c).inv.hom = CategoryStruct.id (G.obj (E.right.obj c))

@[simp]

theorem CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso_hom_hom {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (E : L.LeftExtension F) (c : C) : (coconeAtWhiskerRightIso G F L E c).hom.hom = CategoryStruct.id (G.obj (E.right.obj c))

theorem CategoryTheory.Functor.PreservesPointwiseLeftKanExtensionAt.mk' {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (c : C) {E : L.LeftExtension F} (hE : E.IsPointwiseLeftKanExtensionAt c) (hGE : ((LeftExtension.postcompose₂ L F G).obj E).IsPointwiseLeftKanExtensionAt c) : G.PreservesPointwiseLeftKanExtensionAt F L c

If G preserves any pointwise left Kan extension of F along L at c, then it preserves all of them.

instance CategoryTheory.Functor.hasLeftKanExtension_of_preserves {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [L.HasLeftKanExtension F] [G.PreservesLeftKanExtension F L] : L.HasLeftKanExtension (F.comp G)

instance CategoryTheory.Functor.hasPointwiseLeftKanExtension_of_preserves {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_7, u_2} B] [Category.{u_6, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [L.HasPointwiseLeftKanExtension F] [G.PreservesPointwiseLeftKanExtension F L] : L.HasPointwiseLeftKanExtension (F.comp G)

def CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesLeftKanExtension F L] [L.HasLeftKanExtension F] : (L.leftKanExtension F).comp G ≅ L.leftKanExtension (F.comp G)

Extract an isomorphism (leftKanExtension L F) ⋙ G ≅ leftKanExtension L (F ⋙ G) when G preserves left Kan extensions.

@[simp]

theorem CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_hom_fac {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_7, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesLeftKanExtension F L] [L.HasLeftKanExtension F] : CategoryStruct.comp (whiskerRight (L.leftKanExtensionUnit F) G) (CategoryStruct.comp (L.associator (L.leftKanExtension F) G).hom (L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).hom)) = L.leftKanExtensionUnit (F.comp G)

@[simp]

theorem CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_hom_fac_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_7, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesLeftKanExtension F L] [L.HasLeftKanExtension F] {Z : Functor A D} (h : L.comp (L.leftKanExtension (F.comp G)) ⟶ Z) : CategoryStruct.comp (whiskerRight (L.leftKanExtensionUnit F) G) (CategoryStruct.comp (L.associator (L.leftKanExtension F) G).hom (CategoryStruct.comp (L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).hom) h)) = CategoryStruct.comp (L.leftKanExtensionUnit (F.comp G)) h

@[simp]

theorem CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_hom_fac_app {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_7, u_1} A] [Category.{u_6, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesLeftKanExtension F L] [L.HasLeftKanExtension F] (a : A) : CategoryStruct.comp (G.map ((L.leftKanExtensionUnit F).app a)) ((G.leftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a)) = (L.leftKanExtensionUnit (F.comp G)).app a

@[simp]

theorem CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_7, u_1} A] [Category.{u_6, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesLeftKanExtension F L] [L.HasLeftKanExtension F] (a : A) {Z : D} (h : (L.leftKanExtension (F.comp G)).obj (L.obj a) ⟶ Z) : CategoryStruct.comp (G.map ((L.leftKanExtensionUnit F).app a)) (CategoryStruct.comp ((G.leftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a)) h) = CategoryStruct.comp ((L.leftKanExtensionUnit (F.comp G)).app a) h

@[simp]

theorem CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_inv_fac {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_7, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesLeftKanExtension F L] [L.HasLeftKanExtension F] : CategoryStruct.comp (L.leftKanExtensionUnit (F.comp G)) (L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).inv) = CategoryStruct.comp (whiskerRight (L.leftKanExtensionUnit F) G) (L.associator (L.leftKanExtension F) G).hom

@[simp]

theorem CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_inv_fac_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_7, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesLeftKanExtension F L] [L.HasLeftKanExtension F] {Z : Functor A D} (h : L.comp ((L.leftKanExtension F).comp G) ⟶ Z) : CategoryStruct.comp (L.leftKanExtensionUnit (F.comp G)) (CategoryStruct.comp (L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).inv) h) = CategoryStruct.comp (whiskerRight (L.leftKanExtensionUnit F) G) (CategoryStruct.comp (L.associator (L.leftKanExtension F) G).hom h)

@[simp]

theorem CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_inv_fac_app {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_7, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesLeftKanExtension F L] [L.HasLeftKanExtension F] (a : A) : CategoryStruct.comp ((L.leftKanExtensionUnit (F.comp G)).app a) ((G.leftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a)) = G.map ((L.leftKanExtensionUnit F).app a)

@[simp]

theorem CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_inv_fac_app_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_7, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesLeftKanExtension F L] [L.HasLeftKanExtension F] (a : A) {Z : D} (h : G.obj ((L.leftKanExtension F).obj (L.obj a)) ⟶ Z) : CategoryStruct.comp ((L.leftKanExtensionUnit (F.comp G)).app a) (CategoryStruct.comp ((G.leftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a)) h) = CategoryStruct.comp (G.map ((L.leftKanExtensionUnit F).app a)) h

instance CategoryTheory.Functor.preservesPointwiseLeftKanExtensionAtOfPreservesColimit {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_7, u_2} B] [Category.{u_6, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (c : C) [Limits.PreservesColimit ((CostructuredArrow.proj L c).comp F) G] : G.PreservesPointwiseLeftKanExtensionAt F L c

A functor that preserves the colimit of CostructuredArrow.proj L c ⋙ F preserves the pointwise left Kan extension of F along L at c.

instance CategoryTheory.Functor.preservesPointwiseLKEOfHasPointwiseAndPreservesPointwise {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_7, u_2} B] [Category.{u_6, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [L.HasPointwiseLeftKanExtension F] [G.PreservesPointwiseLeftKanExtension F L] : G.PreservesLeftKanExtension F L

If there is a pointwise left Kan extension of F along L, and if G preserves them, then G preserves left Kan extensions of F along L.

def CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseLeftKanExtension F L] [L.HasPointwiseLeftKanExtension F] : (L.pointwiseLeftKanExtension F).comp G ≅ L.pointwiseLeftKanExtension (F.comp G)

Extract an isomorphism (pointwiseLeftKanExtension L F) ⋙ G ≅ pointwiseLeftKanExtension L (F ⋙ G) when G preserves left Kan extensions.

@[simp]

theorem CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_7, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseLeftKanExtension F L] [L.HasPointwiseLeftKanExtension F] : CategoryStruct.comp (whiskerRight (L.pointwiseLeftKanExtensionUnit F) G) (CategoryStruct.comp (L.associator (L.pointwiseLeftKanExtension F) G).hom (L.whiskerLeft (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom)) = L.pointwiseLeftKanExtensionUnit (F.comp G)

@[simp]

theorem CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_7, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseLeftKanExtension F L] [L.HasPointwiseLeftKanExtension F] {Z : Functor A D} (h : L.comp (L.pointwiseLeftKanExtension (F.comp G)) ⟶ Z) : CategoryStruct.comp (whiskerRight (L.pointwiseLeftKanExtensionUnit F) G) (CategoryStruct.comp (L.associator (L.pointwiseLeftKanExtension F) G).hom (CategoryStruct.comp (L.whiskerLeft (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom) h)) = CategoryStruct.comp (L.pointwiseLeftKanExtensionUnit (F.comp G)) h

theorem CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_7, u_1} A] [Category.{u_6, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseLeftKanExtension F L] [L.HasPointwiseLeftKanExtension F] (a : A) : CategoryStruct.comp (G.map ((L.pointwiseLeftKanExtensionUnit F).app a)) ((G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a)) = (L.pointwiseLeftKanExtensionUnit (F.comp G)).app a

theorem CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac_app_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_7, u_1} A] [Category.{u_6, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseLeftKanExtension F L] [L.HasPointwiseLeftKanExtension F] (a : A) {Z : D} (h : (L.pointwiseLeftKanExtension (F.comp G)).obj (L.obj a) ⟶ Z) : CategoryStruct.comp (G.map ((L.pointwiseLeftKanExtensionUnit F).app a)) (CategoryStruct.comp ((G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a)) h) = CategoryStruct.comp ((L.pointwiseLeftKanExtensionUnit (F.comp G)).app a) h

@[simp]

theorem CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_7, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseLeftKanExtension F L] [L.HasPointwiseLeftKanExtension F] : CategoryStruct.comp (L.pointwiseLeftKanExtensionUnit (F.comp G)) (L.whiskerLeft (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv) = CategoryStruct.comp (whiskerRight (L.pointwiseLeftKanExtensionUnit F) G) (L.associator (L.pointwiseLeftKanExtension F) G).hom

@[simp]

theorem CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_7, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseLeftKanExtension F L] [L.HasPointwiseLeftKanExtension F] {Z : Functor A D} (h : L.comp ((L.pointwiseLeftKanExtension F).comp G) ⟶ Z) : CategoryStruct.comp (L.pointwiseLeftKanExtensionUnit (F.comp G)) (CategoryStruct.comp (L.whiskerLeft (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv) h) = CategoryStruct.comp (whiskerRight (L.pointwiseLeftKanExtensionUnit F) G) (CategoryStruct.comp (L.associator (L.pointwiseLeftKanExtension F) G).hom h)

theorem CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_7, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseLeftKanExtension F L] [L.HasPointwiseLeftKanExtension F] (a : A) : CategoryStruct.comp ((L.pointwiseLeftKanExtensionUnit (F.comp G)).app a) ((G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a)) = G.map ((L.pointwiseLeftKanExtensionUnit F).app a)

theorem CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_7, u_2} B] [Category.{u_8, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseLeftKanExtension F L] [L.HasPointwiseLeftKanExtension F] (a : A) {Z : D} (h : G.obj ((L.pointwiseLeftKanExtension F).obj (L.obj a)) ⟶ Z) : CategoryStruct.comp ((L.pointwiseLeftKanExtensionUnit (F.comp G)).app a) (CategoryStruct.comp ((G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a)) h) = CategoryStruct.comp (G.map ((L.pointwiseLeftKanExtensionUnit F).app a)) h

@[reducible, inline]

abbrev CategoryTheory.Functor.PreservesLeftKanExtensions {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (L : Functor A C) : Prop

G.PreservesLeftKanExtensions L means that G : B ⥤ D preserves all left Kan extensions along L : A ⥤ C of every functor A ⥤ B.

@[reducible, inline]

abbrev CategoryTheory.Functor.PreservesPointwiseLeftKanExtensions {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (L : Functor A C) : Prop

G.PreservesPointwiseLeftKanExtensions L means that G : B ⥤ D preserves all pointwise left Kan extensions along L : A ⥤ C of every functor A ⥤ B.

def CategoryTheory.Functor.lanCompIsoOfPreserves {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (L : Functor A C) [G.PreservesLeftKanExtensions L] [∀ (F : Functor A B), L.HasLeftKanExtension F] [∀ (F : Functor A D), L.HasLeftKanExtension F] : L.lan.comp ((whiskeringRight C B D).obj G) ≅ ((whiskeringRight A B D).obj G).comp L.lan

Commuting a functor that preserves left Kan extensions with the lan functor.

@[simp]

theorem CategoryTheory.Functor.lanCompIsoOfPreserves_hom_app {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (L : Functor A C) [G.PreservesLeftKanExtensions L] [∀ (F : Functor A B), L.HasLeftKanExtension F] [∀ (F : Functor A D), L.HasLeftKanExtension F] (X : Functor A B) : (G.lanCompIsoOfPreserves L).hom.app X = (G.leftKanExtensionCompIsoOfPreserves X L).hom

@[simp]

theorem CategoryTheory.Functor.lanCompIsoOfPreserves_inv_app {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (L : Functor A C) [G.PreservesLeftKanExtensions L] [∀ (F : Functor A B), L.HasLeftKanExtension F] [∀ (F : Functor A D), L.HasLeftKanExtension F] (X : Functor A B) : (G.lanCompIsoOfPreserves L).inv.app X = (G.leftKanExtensionCompIsoOfPreserves X L).inv

class CategoryTheory.Functor.PreservesRightKanExtension {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) : Prop

G.PreservesRightKanExtension F L asserts that G preserves all right Kan extensions of F along L. See PreservesRightKanExtension.mk_of_preserves_isRightKanExtension for a constructor taking a single right Kan extension as input.

• preserves (F' : Functor C B) (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] : (F'.comp G).IsRightKanExtension (CategoryStruct.comp (L.associator F' G).inv (whiskerRight α G))

theorem CategoryTheory.Functor.PreservesRightKanExtension.mk' {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (preserves : ∀ {E : L.RightExtension F} (a : CostructuredArrow.IsUniversal E), Nonempty (CostructuredArrow.IsUniversal ((RightExtension.postcompose₂ L F G).obj E))) : G.PreservesRightKanExtension F L

Alternative constructor for PreservesRightKanExtension, phrased in terms of RightExtension.IsUniversal instead. See PreservesRightKanExtension.mk_of_preserves_isUniversal for a similar constructor taking as input a single RightExtension.

theorem CategoryTheory.Functor.PreservesRightKanExtension.mk_of_preserves_isRightKanExtension {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_7, u_1} A] [Category.{u_6, u_2} B] [Category.{u_5, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (F' : Functor C B) (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] (h : (F'.comp G).IsRightKanExtension (CategoryStruct.comp (L.associator F' G).inv (whiskerRight α G))) : G.PreservesRightKanExtension F L

Show that G preserves right Kan extensions if it maps some right Kan extension to a right Kan extension.

theorem CategoryTheory.Functor.PreservesRightKanExtension.mk_of_preserves_isUniversal {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (E : L.RightExtension F) (hE : CostructuredArrow.IsUniversal E) (h : Nonempty (CostructuredArrow.IsUniversal ((RightExtension.postcompose₂ L F G).obj E))) : G.PreservesRightKanExtension F L

Show that G preserves right Kan extensions if it maps some right Kan extension to a left Kan extension, phrased in terms of IsUniversal.

class CategoryTheory.Functor.PreservesPointwiseRightKanExtensionAt {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (c : C) : Prop

G.PreservesRightKanExtensionAt F L c asserts that G preserves all right pointwise right Kan extensions of F along L at c.

• preserves (E : L.RightExtension F) : ∀ (a : E.IsPointwiseRightKanExtensionAt c), Nonempty (((RightExtension.postcompose₂ L F G).obj E).IsPointwiseRightKanExtensionAt c)

  G preserves every pointwise extensions of F along L at c.

@[reducible, inline]

abbrev CategoryTheory.Functor.PreservesPointwiseRightKanExtension {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) : Prop

G.PreservesRightKanExtensions L asserts that G preserves all pointwise right Kan extensions of F along L for every F.

def CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.postcompose {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) {F : Functor A B} {L : Functor A C} {c : C} [G.PreservesPointwiseRightKanExtensionAt F L c] {E : L.RightExtension F} (hE : E.IsPointwiseRightKanExtensionAt c) : ((postcompose₂ L F G).obj E).IsPointwiseRightKanExtensionAt c

Given a pointwise right Kan extension of F along L at c, exhibits (RightExtension.whiskerRight L F G).obj E as a pointwise right Kan extension of F ⋙ G along L at c.

def CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.postcompose {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) {F : Functor A B} {L : Functor A C} [G.PreservesPointwiseRightKanExtension F L] {E : L.RightExtension F} (hE : E.IsPointwiseRightKanExtension) : ((postcompose₂ L F G).obj E).IsPointwiseRightKanExtension

Given a pointwise right Kan extension of F along L, exhibits (RightExtension.whiskerRight L F G).obj E as a pointwise right Kan extension of F ⋙ G at L.

def CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (E : L.RightExtension F) (c : C) : ((postcompose₂ L F G).obj E).coneAt c ≅ G.mapCone (E.coneAt c)

The cone at a point of the whiskering right by Gof an extension is isomorphic to the action of G on the cone at that point for the original extension.

@[simp]

theorem CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso_hom_hom {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (E : L.RightExtension F) (c : C) : (coneAtWhiskerRightIso G F L E c).hom.hom = CategoryStruct.id (G.obj (E.left.obj c))

@[simp]

theorem CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso_inv_hom {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (E : L.RightExtension F) (c : C) : (coneAtWhiskerRightIso G F L E c).inv.hom = CategoryStruct.id (G.obj (E.left.obj c))

theorem CategoryTheory.Functor.PreservesPointwiseRightKanExtensionAt.mk' {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (c : C) {E : L.RightExtension F} (hE : E.IsPointwiseRightKanExtensionAt c) (hGE : ((RightExtension.postcompose₂ L F G).obj E).IsPointwiseRightKanExtensionAt c) : G.PreservesPointwiseRightKanExtensionAt F L c

If G preserves any pointwise right Kan extension of F along L at c, then it preserves all of them.

instance CategoryTheory.Functor.hasRightKanExtension_of_preserves {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [L.HasRightKanExtension F] [G.PreservesRightKanExtension F L] : L.HasRightKanExtension (F.comp G)

instance CategoryTheory.Functor.hasPointwiseRightKanExtension_of_preserves {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_7, u_2} B] [Category.{u_6, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [L.HasPointwiseRightKanExtension F] [G.PreservesPointwiseRightKanExtension F L] : L.HasPointwiseRightKanExtension (F.comp G)

def CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesRightKanExtension F L] [L.HasRightKanExtension F] : (L.rightKanExtension F).comp G ≅ L.rightKanExtension (F.comp G)

Extract an isomorphism rightKanExtension L F ⋙ G ≅ rightKanExtension L (F ⋙ G) when G preserves right Kan extensions.

@[simp]

theorem CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_hom_fac {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_8, u_2} B] [Category.{u_7, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesRightKanExtension F L] [L.HasRightKanExtension F] : CategoryStruct.comp (L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).hom) (L.rightKanExtensionCounit (F.comp G)) = CategoryStruct.comp (L.associator (L.rightKanExtension F) G).inv (whiskerRight (L.rightKanExtensionCounit F) G)

@[simp]

theorem CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_hom_fac_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_8, u_2} B] [Category.{u_7, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesRightKanExtension F L] [L.HasRightKanExtension F] {Z : Functor A D} (h : F.comp G ⟶ Z) : CategoryStruct.comp (L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).hom) (CategoryStruct.comp (L.rightKanExtensionCounit (F.comp G)) h) = CategoryStruct.comp (L.associator (L.rightKanExtension F) G).inv (CategoryStruct.comp (whiskerRight (L.rightKanExtensionCounit F) G) h)

@[simp]

theorem CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_hom_fac_app {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_8, u_1} A] [Category.{u_7, u_2} B] [Category.{u_6, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesRightKanExtension F L] [L.HasRightKanExtension F] (a : A) : CategoryStruct.comp ((G.rightKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a)) ((L.rightKanExtensionCounit (F.comp G)).app a) = G.map ((L.rightKanExtensionCounit F).app a)

@[simp]

theorem CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_8, u_1} A] [Category.{u_7, u_2} B] [Category.{u_6, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesRightKanExtension F L] [L.HasRightKanExtension F] (a : A) {Z : D} (h : G.obj (F.obj a) ⟶ Z) : CategoryStruct.comp ((G.rightKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a)) (CategoryStruct.comp ((L.rightKanExtensionCounit (F.comp G)).app a) h) = CategoryStruct.comp (G.map ((L.rightKanExtensionCounit F).app a)) h

@[simp]

theorem CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_inv_fac {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_8, u_2} B] [Category.{u_7, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesRightKanExtension F L] [L.HasRightKanExtension F] : CategoryStruct.comp (L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).inv) (CategoryStruct.comp (L.associator (L.rightKanExtension F) G).inv (whiskerRight (L.rightKanExtensionCounit F) G)) = L.rightKanExtensionCounit (F.comp G)

@[simp]

theorem CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_inv_fac_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_8, u_2} B] [Category.{u_7, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesRightKanExtension F L] [L.HasRightKanExtension F] {Z : Functor A D} (h : F.comp G ⟶ Z) : CategoryStruct.comp (L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).inv) (CategoryStruct.comp (L.associator (L.rightKanExtension F) G).inv (CategoryStruct.comp (whiskerRight (L.rightKanExtensionCounit F) G) h)) = CategoryStruct.comp (L.rightKanExtensionCounit (F.comp G)) h

@[simp]

theorem CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_inv_fac_app {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_7, u_1} A] [Category.{u_8, u_2} B] [Category.{u_6, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesRightKanExtension F L] [L.HasRightKanExtension F] (a : A) : CategoryStruct.comp ((G.rightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a)) (G.map ((L.rightKanExtensionCounit F).app a)) = (L.rightKanExtensionCounit (F.comp G)).app a

@[simp]

theorem CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_7, u_1} A] [Category.{u_8, u_2} B] [Category.{u_6, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesRightKanExtension F L] [L.HasRightKanExtension F] (a : A) {Z : D} (h : G.obj (F.obj a) ⟶ Z) : CategoryStruct.comp ((G.rightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a)) (CategoryStruct.comp (G.map ((L.rightKanExtensionCounit F).app a)) h) = CategoryStruct.comp ((L.rightKanExtensionCounit (F.comp G)).app a) h

instance CategoryTheory.Functor.preservesPointwiseRightKanExtensionAtOfPreservesLimit {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_7, u_2} B] [Category.{u_6, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) (c : C) [Limits.PreservesLimit ((StructuredArrow.proj c L).comp F) G] : G.PreservesPointwiseRightKanExtensionAt F L c

A functor that preserves the limit of (StructuredArrow.proj L c ⋙ F) preserves the pointwise right Kan extension of F along L at c.

instance CategoryTheory.Functor.preservesPointwiseRKEOfHasPointwiseAndPreservesPointwise {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_7, u_2} B] [Category.{u_6, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [L.HasPointwiseRightKanExtension F] [G.PreservesPointwiseRightKanExtension F L] : G.PreservesRightKanExtension F L

If there is a pointwise right Kan extension of F along L, and if G preserves them, then G preserves right Kan extensions of F along L.

def CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseRightKanExtension F L] [L.HasPointwiseRightKanExtension F] : (L.pointwiseRightKanExtension F).comp G ≅ L.pointwiseRightKanExtension (F.comp G)

Extract an isomorphism L.pointwiseRightKanExtension F ⋙ G ≅ L.pointwiseRightKanExtension (F ⋙ G) when G preserves right Kan extensions.

@[simp]

theorem CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_8, u_2} B] [Category.{u_7, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseRightKanExtension F L] [L.HasPointwiseRightKanExtension F] : CategoryStruct.comp (L.whiskerLeft (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom) (L.pointwiseRightKanExtensionCounit (F.comp G)) = CategoryStruct.comp (L.associator (L.pointwiseRightKanExtension F) G).inv (whiskerRight (L.pointwiseRightKanExtensionCounit F) G)

@[simp]

theorem CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_8, u_2} B] [Category.{u_7, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseRightKanExtension F L] [L.HasPointwiseRightKanExtension F] {Z : Functor A D} (h : F.comp G ⟶ Z) : CategoryStruct.comp (L.whiskerLeft (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom) (CategoryStruct.comp (L.pointwiseRightKanExtensionCounit (F.comp G)) h) = CategoryStruct.comp (L.associator (L.pointwiseRightKanExtension F) G).inv (CategoryStruct.comp (whiskerRight (L.pointwiseRightKanExtensionCounit F) G) h)

theorem CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_8, u_1} A] [Category.{u_7, u_2} B] [Category.{u_6, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseRightKanExtension F L] [L.HasPointwiseRightKanExtension F] (a : A) : CategoryStruct.comp ((G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a)) ((L.pointwiseRightKanExtensionCounit (F.comp G)).app a) = G.map ((L.pointwiseRightKanExtensionCounit F).app a)

theorem CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_8, u_1} A] [Category.{u_7, u_2} B] [Category.{u_6, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseRightKanExtension F L] [L.HasPointwiseRightKanExtension F] (a : A) {Z : D} (h : G.obj (F.obj a) ⟶ Z) : CategoryStruct.comp ((G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a)) (CategoryStruct.comp ((L.pointwiseRightKanExtensionCounit (F.comp G)).app a) h) = CategoryStruct.comp (G.map ((L.pointwiseRightKanExtensionCounit F).app a)) h

@[simp]

theorem CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_8, u_2} B] [Category.{u_7, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseRightKanExtension F L] [L.HasPointwiseRightKanExtension F] : CategoryStruct.comp (L.whiskerLeft (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv) (CategoryStruct.comp (L.associator (L.pointwiseRightKanExtension F) G).inv (whiskerRight (L.pointwiseRightKanExtensionCounit F) G)) = L.pointwiseRightKanExtensionCounit (F.comp G)

@[simp]

theorem CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_6, u_1} A] [Category.{u_8, u_2} B] [Category.{u_7, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseRightKanExtension F L] [L.HasPointwiseRightKanExtension F] {Z : Functor A D} (h : F.comp G ⟶ Z) : CategoryStruct.comp (L.whiskerLeft (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv) (CategoryStruct.comp (L.associator (L.pointwiseRightKanExtension F) G).inv (CategoryStruct.comp (whiskerRight (L.pointwiseRightKanExtensionCounit F) G) h)) = CategoryStruct.comp (L.pointwiseRightKanExtensionCounit (F.comp G)) h

theorem CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_7, u_1} A] [Category.{u_8, u_2} B] [Category.{u_6, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseRightKanExtension F L] [L.HasPointwiseRightKanExtension F] (a : A) : CategoryStruct.comp ((G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a)) (G.map ((L.pointwiseRightKanExtensionCounit F).app a)) = (L.pointwiseRightKanExtensionCounit (F.comp G)).app a

theorem CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app_assoc {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_7, u_1} A] [Category.{u_8, u_2} B] [Category.{u_6, u_3} C] [Category.{u_5, u_4} D] (G : Functor B D) (F : Functor A B) (L : Functor A C) [G.PreservesPointwiseRightKanExtension F L] [L.HasPointwiseRightKanExtension F] (a : A) {Z : D} (h : G.obj (F.obj a) ⟶ Z) : CategoryStruct.comp ((G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a)) (CategoryStruct.comp (G.map ((L.pointwiseRightKanExtensionCounit F).app a)) h) = CategoryStruct.comp ((L.pointwiseRightKanExtensionCounit (F.comp G)).app a) h

@[reducible, inline]

abbrev CategoryTheory.Functor.PreservesRightKanExtensions {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (L : Functor A C) : Prop

G.PreservesRightKanExtensions L means that G : B ⥤ D preserves all right Kan extensions along L : A ⥤ C of every functor A ⥤ B.

@[reducible, inline]

abbrev CategoryTheory.Functor.PreservesPointwiseRightKanExtensions {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (L : Functor A C) : Prop

G.PreservesPointwiseRightKanExtensions L means that G : B ⥤ D preserves all pointwise right Kan extensions along L : A ⥤ C of every functor A ⥤ B.

def CategoryTheory.Functor.ranCompIsoOfPreserves {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (L : Functor A C) [G.PreservesRightKanExtensions L] [∀ (F : Functor A B), L.HasRightKanExtension F] [∀ (F : Functor A D), L.HasRightKanExtension F] : L.ran.comp ((whiskeringRight C B D).obj G) ≅ ((whiskeringRight A B D).obj G).comp L.ran

Commuting a functor that preserves right Kan extensions with the ran functor.

@[simp]

theorem CategoryTheory.Functor.ranCompIsoOfPreserves_hom_app {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (L : Functor A C) [G.PreservesRightKanExtensions L] [∀ (F : Functor A B), L.HasRightKanExtension F] [∀ (F : Functor A D), L.HasRightKanExtension F] (X : Functor A B) : (G.ranCompIsoOfPreserves L).hom.app X = (G.rightKanExtensionCompIsoOfPreserves X L).hom

@[simp]

theorem CategoryTheory.Functor.ranCompIsoOfPreserves_inv_app {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (G : Functor B D) (L : Functor A C) [G.PreservesRightKanExtensions L] [∀ (F : Functor A B), L.HasRightKanExtension F] [∀ (F : Functor A D), L.HasRightKanExtension F] (X : Functor A B) : (G.ranCompIsoOfPreserves L).inv.app X = (G.rightKanExtensionCompIsoOfPreserves X L).inv