feat(CategoryTheory): the localized category is monoidal

[joelriou]

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.

Co-authored-by: Dagur Asgeirsson dagurtomas@gmail.com

---

• depends on: [Merged by Bors] - feat(CategoryTheory/Monoidal): the curried associator isomorphism #11701
• depends on: [Merged by Bors] - chore(CategoryTheory): define the equivalences congrLeft and congrRight more explicitly #18165
• depends on: [Merged by Bors] - feat(CategoryTheory/Localization): liftings of bifunctors #19894
• depends on: feat(CategoryTheory): whiskering and curryfication of functors in three variables #20197

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]

PR summary 52c3e3e78f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Localization.Trifunctor (new file)	422
Mathlib.CategoryTheory.Localization.Monoidal (new file)	440

---

Declarations diff

+ IsInvertedBy₃
+ Iso.hom_inv_id_app_app_app
+ Iso.inv_hom_id_app_app_app
+ Lifting₃
+ Lifting₃.bifunctorComp₂₃
+ Lifting₃.iso
+ Lifting₃.uncurry
+ LocalizedMonoidal
+ Monoidal
+ Pentagon
+ associator_hom_app
+ associator_hom_app_app_app
+ associator_naturality
+ associator_naturality₁
+ associator_naturality₂
+ associator_naturality₃
+ bifunctorComp₁₂Functor
+ bifunctorComp₁₂FunctorMap
+ bifunctorComp₁₂FunctorObj
+ bifunctorComp₁₂Iso
+ bifunctorComp₂₃Functor
+ bifunctorComp₂₃FunctorMap
+ bifunctorComp₂₃FunctorObj
+ bifunctorComp₂₃Iso
+ currying₃
+ currying₃_unitIso_hom_app_app_app_app
+ currying₃_unitIso_inv_app_app_app_app
+ curry₃
+ curry₃ObjProdComp
+ curry₃_map_app_app_app
+ curry₃_obj_map_app_app
+ curry₃_obj_obj_map_app
+ curry₃_obj_obj_obj_map
+ fullyFaithfulUncurry₃
+ id_tensorHom
+ instance (X : C) :
+ instance (Y : C) :
+ instance :
+ instance : (L').EssSurj := Localization.essSurj L' W
+ instance : (L').IsLocalization W := inferInstanceAs (L.IsLocalization W)
+ instance : (toMonoidalCategory L W ε).Monoidal
+ instance : Category (LocalizedMonoidal L W ε)
+ instance : Lifting₂ L' L' W W (curriedTensor C ⋙ (whiskeringRight C C
+ instance : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F (lift₃ F hF L₁ L₂ L₃)
+ isInvertedBy₂
+ leftUnitor
+ leftUnitor_hom_app
+ leftUnitor_naturality
+ lift₃
+ lift₃NatIso
+ lift₃NatTrans
+ lift₃NatTrans_app_app_app
+ monoidalCategoryStruct
+ natTrans₃_ext
+ pentagon
+ pentagon_aux₁
+ pentagon_aux₂
+ pentagon_aux₃
+ rightUnitor
+ rightUnitor_hom_app
+ rightUnitor_naturality
+ tensorBifunctor
+ tensorBifunctorIso
+ tensorHom_id
+ tensorHom_mem
+ tensor_comp
+ tensor_id
+ toMonoidalCategory
+ triangle
+ triangle_aux
+ triangle_aux₁
+ triangle_aux₂
+ uncurry₃
+ whiskerLeft_comp
+ whiskerLeft_id
+ whiskerLeft_mem
+ whiskerRight_comp
+ whiskerRight_id
+ whiskerRight_mem
+ whisker_exchange
+ whiskeringLeft₃ObjObjObj
+ whiskeringRight₂'
+ whiskeringRight₃
+ ε'
+ μ
+ μ_inv_natural_left
+ μ_inv_natural_right
+ μ_natural_left
+ μ_natural_right
++ associator

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.

---

Increase in tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type
1518	3	erw

Current commit 52c3e3e78f
Reference commit e820917259

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).

[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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory/Monoidal): the curried associator isomorphism #11701
• [Merged by Bors] - chore(CategoryTheory): define the equivalences congrLeft and congrRight more explicitly #18165
• [Merged by Bors] - feat(CategoryTheory/Localization): liftings of bifunctors #19894
• feat(CategoryTheory): whiskering and curryfication of functors in three variables #20197
  By Dependent Issues (🤖). Happy coding!