feat(CategoryTheory): the localized category is monoidal

[joelriou]

trafficstars

In this category, 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.

---

• [x] depends on: #11701

This shall be used in order to obtain a monoidal category structure on sheaves of modules from the monoidal structure on presheaves of modules. This also prepares some of the bifunctor API for the left derived monoidal category structure (when the tensor product does not preserves W but can still be left derived).

[github-actions[bot]]

messageFile.md

[dagurtomas]

I just opened #18165 which, if merged, should avoid random merge conflicts appearing here.

[jcommelin]

Do I understand that this PR is the next one in line in your epic derived + homology saga?

[joelriou]

Do I understand that this PR is the next one in line in your epic derived + homology saga?

Not exactly, in the future (not very soon), we should obtain a "left derived monoidal category structure" on the derived category using left derived functors instead of localized functors (which already invert W).

The main application of this PR shall be the monoidal category structure on categories of sheaves (by thinking of the category of sheaves as a localization of the category of presheaves). It is related to the proof that presheaf categories are monoidal closed (abstract proof #16067 by @dagurtomas and a more explicit approach is #19103). With some little extra work, this internal hom will be used in order to show that the class W of morphisms of presheaves which induce iso on the associated sheaves satisfy the assumption in this PR #12728, which will give the expected monoidal category structure on categories of sheaves (with values in a symmetric (braided?) monoidal closed category that has suitable limits).

[github-actions[bot]]

messageFile.md

[github-actions[bot]]

messageFile.md

[github-actions[bot]]

messageFile.md

[github-actions[bot]]

PR summary 8efbb77412

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Localization.Monoidal	426	428	+2 (+0.47%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Localization.Monoidal	2

---

Declarations diff

+ Pentagon + instance : + instance : (L').EssSurj := Localization.essSurj L' W + instance : (toMonoidalCategory L W ε).Monoidal + leftUnitor_naturality + pentagon + pentagon_aux₁ + pentagon_aux₂ + pentagon_aux₃ + rightUnitor_naturality + triangle + triangle_aux₁ + triangle_aux₂ + triangle_aux₃

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-bors[bot]]

:v: joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#20951~~
• ~~leanprover-community/mathlib4#11701~~
• ~~leanprover-community/mathlib4#18165~~
• ~~leanprover-community/mathlib4#19894~~
• ~~leanprover-community/mathlib4#20197~~
• ~~leanprover-community/mathlib4#20788~~ By Dependent Issues (🤖). Happy coding!

[joelriou]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style