Commit 2025-08-14 04:35 0c21e061

feat(CategoryTheory/Monoidal/Limits): miscellany about preservation of (co)limits by tensor products (#25732) Register some instances regarding preservations of (co)limits for the tensor product of a monoidal category. More precisely, we register the fact that if the category is braided and tensorLeft c preserves colimits (this can be inferred e.g via MonoidalClosed C), then so does tensorRight c for every c. We also rephrase preservation of (co)limits for curriedTensor C in terms of preservations of (co)limits for tensorRight c. The PR introduces also introduces a directory CategoryTheory.Monoidal.Limits and moves the existing file CategoryTheory.Monoidal.Limits.lean to CategoryTheory.Monoidal.Limits.Basic.