English
In a braided setting, if a right tensoring by c preserves a colimit, then left tensoring by c also preserves that colimit (duality with the previous result).
Русский
В braided-среде, если тензоризация справа на c сохраняет колимит, то тензоризация слева на c также сохраняет этот колимит (отношение-дополнение к предыдущему результату).
LaTeX
$$$[\\text{BraidedCategory } C] (\\text{PreservesColimit } F (\\text{tensorRight } c)) \\Rightarrow (\\text{PreservesColimit } F (\\text{tensorLeft } c))$$$
Lean4
/-- When `C` is braided and `tensorRight c` preserves a colimit, then so does `tensorLeft k`.
We are not making this an instance to avoid an instance loop with
`preservesColimit_of_braided_and_preservesColimit_tensor_left`. -/
theorem preservesColimit_of_braided_and_preservesColimit_tensor_right [BraidedCategory C] (c : C)
[PreservesColimit F (tensorRight c)] : PreservesColimit F (tensorLeft c) :=
preservesColimit_of_natIso F (BraidedCategory.tensorLeftIsoTensorRight c).symm
