Colimits of external products

External product with a fixed first diagram preserves colimits when tensoring with each value of that diagram does. Colimits in functor categories are computed pointwise, so the result follows by evaluating at a pair of objects. This supplies the colimit-preserving input to the left Kan extension defining Day convolution.

instance CategoryTheory.MonoidalCategory.preservesColimitsOfShape_externalProductLeft {C : Type u_1} {C' : Type u_2} {V : Type u_3} {J : Type u_4} [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [Category.{v_3, u_3} V] [Category.{v_4, u_4} J] [MonoidalCategory V] (F : Functor C V) [Limits.HasColimitsOfShape J V] [∀ (x : C), Limits.PreservesColimitsOfShape J (tensorLeft (F.obj x))] : Limits.PreservesColimitsOfShape J (((externalProductBifunctorCurried C C' V).obj F).comp Functor.uncurry)

External product with a fixed first diagram preserves pointwise colimits if tensoring with each of its values does.