English
If tensoring on the left with F preserves colimits of shape K in C, then for any diagram D of shape K in C, tensorLeft F preserves the colimit of D and the diagram D after tensoring commutes with taking colimits.
Русский
Если операция тензорирования слева на F сохраняет колимиты формы K в C, то для всякого диаграммы D формы K тензорование слева сохраняет ее колимит, и диаграмма после тензорования коммутирует со взятием колимита.
LaTeX
$$$\mathrm{PreservesColimitsOfShape}_K(\mathrm{tensorLeft} F)$$$
Lean4
instance {K : Type*} [Category K] [HasColimitsOfShape K C] [∀ X : C, PreservesColimitsOfShape K (tensorLeft X)]
{F : J ⥤ C} : PreservesColimitsOfShape K (tensorLeft F) :=
by
apply preservesColimitsOfShape_of_evaluation
intro k
haveI : tensorLeft F ⋙ (evaluation J C).obj k ≅ (evaluation J C).obj k ⋙ tensorLeft (F.obj k) :=
NatIso.ofComponents (fun _ ↦ Iso.refl _)
exact preservesColimitsOfShape_of_natIso this.symm
