Parametrized adjunctions and limits

Given bifunctors F : C₁ ⥤ C₂ ⥤ C₃, G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂ and a paremetrized adjunction adj₂ : F ⊣₂ G, we show that for any X₃ : C₃, the functor G.flip.obj X₃ : C₁ᵒᵖ ⥤ C₃ preserves limits of shape J if for any X₂ : C₂, the functor F.flip.obj X₂ : C₁ ⥤ C₃ preserves colimits of shape Jᵒᵖ.

theorem CategoryTheory.ParametrizedAdjunction.preservesLimit_flip_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {J : Type u_4} [Category.{v_4, u_4} J] (P : Functor J C₁ᵒᵖ) [∀ (X₂ : C₂), Limits.PreservesColimit P.leftOp (F.flip.obj X₂)] (X₃ : C₃) : Limits.PreservesLimit P (G.flip.obj X₃)

theorem CategoryTheory.ParametrizedAdjunction.preservesLimitsOfShape_flip_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] {F : Functor C₁ (Functor C₂ C₃)} {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} (adj₂ : F ⊣₂ G) (J : Type u_4) [Category.{v_4, u_4} J] [∀ (X₂ : C₂), Limits.PreservesColimitsOfShape Jᵒᵖ (F.flip.obj X₂)] (X₃ : C₃) : Limits.PreservesLimitsOfShape J (G.flip.obj X₃)