English
If the ambient category is braided and a left tensoring functor with c preserves a colimit, then the corresponding right tensoring functor with c also preserves that colimit.
Русский
Если окружающая категория канонически пересчитывается как braided и тензоризация слева на с сохраняет колимит, то тензоризация справа с тем же объектом c сохраняет этот колимит.
LaTeX
$$$[\\text{BraidedCategory } C] \;\\Rightarrow\\; \\big( \\text{PreservesColimit } F (\\text{tensorLeft } c) \\Rightarrow \\text{PreservesColimit } F (\\text{tensorRight } c) \\big)$$$
Lean4
/-- When `C` is braided and `tensorLeft c` preserves a colimit, then so does `tensorRight k`. -/
instance preservesColimit_of_braided_and_preservesColimit_tensor_left [BraidedCategory C] (c : C)
[PreservesColimit F (tensorLeft c)] : PreservesColimit F (tensorRight c) :=
preservesColimit_of_natIso F (BraidedCategory.tensorLeftIsoTensorRight c)
