English
If C is braided and a left-tensoring by c preserves a limit, then right-tensoring by c preserves that limit as well.
Русский
Если C браидед и тензоризация слева на c сохраняет предел, то тензоризация справа на c сохраняет этот предел.
LaTeX
$$$[\\text{BraidedCategory } C] (c : C) [PreservesLimit F (\\text{tensorLeft } c)] : PreservesLimit F (\\text{tensorRight } c)$$$
Lean4
/-- When `C` is braided and `tensorRight c` preserves a limit, then so does `tensorLeft k`.
We are not making this an instance to avoid an instance loop with
`preservesLimit_of_braided_and_preservesLimit_tensor_left`. -/
theorem preservesLimit_of_braided_and_preservesLimit_tensor_right [BraidedCategory C] (c : C)
[PreservesLimit F (tensorRight c)] : PreservesLimit F (tensorLeft c) :=
preservesLimit_of_natIso F (BraidedCategory.tensorLeftIsoTensorRight c).symm
