-
Notifications
You must be signed in to change notification settings - Fork 331
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
refactor(CategoryTheory/Monoidal): typeclasses Functor.LaxMonoidal, Functor.OplaxMonoidal and Functor.Monoidal #17904
base: master
Are you sure you want to change the base?
Conversation
…roduct categories
…nctor-monoidal-refactor-typeclasses
… functor-monoidal-refactor-typeclasses
… functor-monoidal-refactor-typeclasses
Co-authored-by: Yuma Mizuno <[email protected]>
Co-authored-by: Yuma Mizuno <[email protected]>
!bench |
Here are the benchmark results for commit 1bc507c. 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% |
I do not know why |
!bench |
Here are the benchmark results for commit 8500e0c. 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% |
When shifts on categories are involved, it seems |
!bench |
Here are the benchmark results for commit 58ea18e. 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% |
Monoidal functors are refactored. Given a functor
F : C ⥤ D
between monoidal categories, we introduce typeclassesF.LaxMonoidal
andF.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 bothF.LaxMonoidal
andF.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 inCategoryTheory.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.