Commit 2025-01-31 20:22 4565f9f1
View on Github →feat(CategoryTheory): the localized category is monoidal (#12728)
In this PR, we shall show that if C is a monoidal category and W is a class of morphism that is preserved by the tensor product, then the localized category is also monoidal.
(This shall be used in order to define a monoidal structure on the category of sheaves of abelian groups, and on categories of sheaves of modules.)