refactor(CategoryTheory/Monoidal): typeclasses Functor.LaxMonoidal, Functor.OplaxMonoidal and Functor.Monoidal

[joelriou]

Monoidal functors are refactored. Given a functor F : C ⥤ D between monoidal categories, we introduce typeclasses F.LaxMonoidal and F.OplaxMonoidal which carry the data of morphisms like μ : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y) (or δ : F.obj (X ⊗ Y) ⟶ F.obj X ⊗ F.obj Y). Then, the functor is monoidal if both F.LaxMonoidal and F.OplaxMonoidal and that both data provide inverse isomorphisms. With this design, there is more symmetry between lax and oplax functors (in the bundled setting, this was also experimented upon in #10845 ). (Roughly speaking, what was previously in CategoryTheory.Monoidal.Functorial was generalized.)

This is also a change from the previous designs where (lax) monoidal functors were bundled, which would be quite problematic or at least very unpractical in future applications: sooner or later, we shall have functors between derived categories, which are lax/oplax/monoidal, but are also triangulated, and some of these functors shall be adjoints, etc. The bundled aspect was not very much in used before this refactor: it was relevant only when constructing functors from a category of lax monoidal functors; in such case, the corresponding case of bundled lax monoidal functors, etc, have been kept in the code.

---

• depends on: [Merged by Bors] - chore(CategoryTheory/Adjunction): homEquiv_unit is no longer a global simp lemma #17761

[joelriou]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1bc507c.
There were significant changes against commit d50eac5:

  Benchmark                                                    Metric         Change
  ==================================================================================
+ ~Mathlib.Algebra.Category.ModuleCat.Adjunctions              instructions   -31.3%
+ ~Mathlib.Algebra.Homology.BifunctorShift                     instructions   -25.8%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit   instructions   -27.0%
- ~Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift   instructions   143.7%
- ~Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated   instructions   100.9%
- ~Mathlib.Algebra.Homology.HomotopyCategory.Shift             instructions    40.4%
- ~Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence     instructions    18.7%
- ~Mathlib.Algebra.Homology.HomotopyCategory.Triangulated      instructions    67.1%
- ~Mathlib.Algebra.Homology.TotalComplexShift                  instructions    34.8%
+ ~Mathlib.CategoryTheory.Monoidal.Discrete                    instructions   -49.5%
+ ~Mathlib.CategoryTheory.Monoidal.End                         instructions   -20.6%
- ~Mathlib.CategoryTheory.Monoidal.Functor                     instructions    44.3%
+ ~Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts         instructions   -27.6%
- ~Mathlib.CategoryTheory.Triangulated.HomologicalFunctor      instructions    74.1%
+ ~Mathlib.CategoryTheory.Triangulated.Opposite                instructions   -12.6%

[joelriou]

I do not know why Algebra.Homology.HomotopyCategory has become significantly slower (I will try to investigate), but CategoryTheory.Triangulated.Opposite was an extremely slow file, any improvement on this is good!

[joelriou]

!bench

[leanprover-bot]

Here are the benchmark results for commit 8500e0c.
There were significant changes against commit d50eac5:

  Benchmark                                                    Metric         Change
  ==================================================================================
+ ~Mathlib.Algebra.Category.ModuleCat.Adjunctions              instructions   -31.3%
+ ~Mathlib.Algebra.Homology.BifunctorShift                     instructions   -25.8%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit   instructions   -27.0%
- ~Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift   instructions    25.7%
- ~Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated   instructions     5.6%
- ~Mathlib.Algebra.Homology.HomotopyCategory.Shift             instructions    19.5%
- ~Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence     instructions    18.7%
- ~Mathlib.Algebra.Homology.HomotopyCategory.Triangulated      instructions     6.3%
+ ~Mathlib.CategoryTheory.Monoidal.Discrete                    instructions   -49.5%
+ ~Mathlib.CategoryTheory.Monoidal.End                         instructions   -20.6%
- ~Mathlib.CategoryTheory.Monoidal.Functor                     instructions    44.3%
+ ~Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts         instructions   -27.6%
+ ~Mathlib.CategoryTheory.Triangulated.Opposite                instructions   -12.6%

[joelriou]

When shifts on categories are involved, it seems aesop_cat has become much slower than intros; ext; dsimp; simp.

[joelriou]

!bench

[leanprover-bot]

Here are the benchmark results for commit 58ea18e.
There were significant changes against commit 9d61276:

  Benchmark                                                    Metric         Change
  ==================================================================================
+ ~Mathlib.Algebra.Category.ModuleCat.Adjunctions              instructions   -31.3%
+ ~Mathlib.Algebra.Homology.BifunctorShift                     instructions   -25.8%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit   instructions   -27.0%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift   instructions   -20.3%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated   instructions    -7.8%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence     instructions   -19.9%
+ ~Mathlib.CategoryTheory.Monoidal.Discrete                    instructions   -49.5%
+ ~Mathlib.CategoryTheory.Monoidal.End                         instructions   -20.6%
- ~Mathlib.CategoryTheory.Monoidal.Functor                     instructions    44.3%
+ ~Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts         instructions   -27.6%
+ ~Mathlib.CategoryTheory.Triangulated.Opposite                instructions   -12.6%