Commit 2026-03-03 01:16 6a736c34

View on Github →

feat(CategoryTheory/Monoidal/Limits): colimit of tensor products (#35806) This PR builds on prior work by Robin Carlier about sifted categories and colimits of bifunctors in order to show that under suitable assumptions the colimit of F₁ ⊗ F₂ identifies to the tensor product of the colimits of F₁ and F₂.

Estimated changes