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.

---

• [x] depends on: #17761

[github-actions[bot]]

PR summary b912f42316

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Monoidal.Functorial	394	0	-394 (-100.00%)
Mathlib.CategoryTheory.Monoidal.Limits	435	433	-2 (-0.46%)
Mathlib.CategoryTheory.Monoidal.Internal.Limits	458	456	-2 (-0.44%)
Mathlib.Algebra.Category.ModuleCat.Adjunctions	1022	1020	-2 (-0.20%)
Mathlib.RepresentationTheory.Rep	1498	1496	-2 (-0.13%)
Mathlib.RepresentationTheory.GroupCohomology.Resolution	1579	1577	-2 (-0.13%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Monoidal.Functorial	-394
25 files Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.Condensed.Limits Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Explicit Mathlib.Condensed.Module Mathlib.Condensed.Discrete.Characterization Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.Condensed.Light.CartesianClosed Mathlib.RepresentationTheory.Rep Mathlib.RepresentationTheory.Invariants Mathlib.Condensed.Solid Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Light.Epi Mathlib.RepresentationTheory.Character Mathlib.CategoryTheory.Monoidal.Limits Mathlib.CategoryTheory.Monoidal.Internal.Limits Mathlib.Condensed.Light.Limits Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.FDRep Mathlib.Condensed.CartesianClosed Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.Condensed.Light.Module Mathlib.Condensed.Epi Mathlib.Algebra.Category.ModuleCat.Presheaf.Free	-2

---

Declarations diff

+ CoreMonoidal + Discrete.monoidalFunctorBraided + Discrete.monoidalFunctorComp_isMonoidal + Discrete.monoidalFunctorMonoidal + Discrete.monoidalFunctor_obj + Discrete.monoidalFunctor_δ + Discrete.monoidalFunctor_ε + Discrete.monoidalFunctor_η + Discrete.monoidalFunctor_μ + Functor.Braided + Functor.LaxBraided + Functor.map_braiding + FunctorCategoryEquivalence.functor_δ + FunctorCategoryEquivalence.functor_ε + FunctorCategoryEquivalence.functor_η + FunctorCategoryEquivalence.functor_μ + Hom + LaxMonoidal.prod' + Monoidal + Monoidal.ofLaxMonoidal + Monoidal.ofOplaxMonoidal + Monoidal.prod' + OplaxMonoidal + OplaxMonoidal.prod' + chosenFiniteProducts + commMonToLaxBraidedObj + commMonToLaxBraidedObj_ε + commMonToLaxBraidedObj_μ + comp_δ + comp_ε + comp_η + comp_μ + counitIso_inv_app_comp_functor_map_η_inverse + counitIso_inv_app_tensor_comp_functor_map_δ_inverse + diag_δ + diag_ε + diag_η + diag_μ + equivalenceTransported + free_δ_freeMk + free_ε_one + free_η_freeMk + free_μ_freeMk_tmul_freeMk + fromInducedCoreMonoidal + fromInducedMonoidal + fullSubcategoryInclusionMonoidal + fullSubcategoryInclusion_δ + fullSubcategoryInclusion_ε + fullSubcategoryInclusion_η + fullSubcategoryInclusion_μ + fullSubcategory_map_δ + fullSubcategory_map_ε + fullSubcategory_map_η + fullSubcategory_map_μ + fullyFaithfulForget + fullyFaithfulForget₂Mon_ + functor_map_ε_inverse_comp_counitIso_hom_app + functor_map_μ_inverse_comp_counitIso_hom_app_tensor + id_δ + id_ε + id_η + id_μ + in + instMonoidalCategory + instance (A : CommMon_ C) : (commMonToLaxBraidedObj A).LaxBraided + instance (A : CommMon_ C) : (commMonToLaxBraidedObj A).LaxMonoidal + instance (A : Mon_ C) : (monToLaxMonoidalObj A).LaxMonoidal + instance (A B : C) : IsIso (δ F A B) + instance (C : Type u) [Category.{v} C] [MonoidalCategory C] : + instance (F : C ⥤ D) (G : D ⥤ E) (H : E ⥤ E') [F.LaxMonoidal] [G.LaxMonoidal] [H.LaxMonoidal] : + instance (F : C ⥤ D) (G : D ⥤ E) [F.Braided] [G.Braided] : (F ⋙ G).Braided + instance (F : C ⥤ D) (G : D ⥤ E) [F.LaxBraided] [G.LaxBraided] : + instance (F : C ⥤ D) [F.LaxMonoidal] : NatTrans.IsMonoidal F.leftUnitor.hom + instance (F : C ⥤ D) [F.LaxMonoidal] : NatTrans.IsMonoidal F.rightUnitor.hom + instance (X Y : C) : IsIso (δ F X Y) := (μIso F X Y).isIso_inv + instance (X Y : C) : IsIso (δ F X Y) := by dsimp [δ_eq]; infer_instance + instance (X Y : C) : IsIso (μ F X Y) := (μIso F X Y).isIso_hom + instance (h : ShiftMkCore C A) : (Discrete.functor h.F).Monoidal + instance : + instance : (Action.forget V G).Braided + instance : (Action.forget V G).Monoidal + instance : (FullSubcategory.map h).Monoidal + instance : (FunctorCategoryEquivalence.functor (V := V) (G := G)).IsEquivalence + instance : (FunctorCategoryEquivalence.functor (V := V) (G := G)).Monoidal + instance : (FunctorCategoryEquivalence.inverse (V := V) (G := G)).IsEquivalence + instance : (FunctorCategoryEquivalence.inverse (V := V) (G := G)).Monoidal + instance : (diag C).Monoidal + instance : (endMonoidalStarFunctor C).Monoidal + instance : (equivalenceTransported e).functor.Monoidal + instance : (equivalenceTransported e).inverse.Monoidal := by + instance : (equivalenceTransported e).symm.IsMonoidal := by + instance : (equivalenceTransported e).symm.functor.Monoidal + instance : (equivalenceTransported e).symm.inverse.Monoidal + instance : (forget₂ (AlgebraCat R) (ModuleCat R)).Braided + instance : (forget₂ (FGModuleCat.{u} R) (ModuleCat.{u} R)).Additive + instance : (forget₂ (FGModuleCat.{u} R) (ModuleCat.{u} R)).Linear R + instance : (forget₂ (FGModuleCat.{u} R) (ModuleCat.{u} R)).Monoidal + instance : (forget₂ (QuadraticModuleCat R) (ModuleCat R)).Braided + instance : (free R).Monoidal + instance : (fullSubcategoryInclusion P).Braided + instance : (functorCategoryEquivalence V G).functor.Monoidal := by + instance : (functorCategoryEquivalence V G).inverse.Monoidal := by + instance : (lim (J := J) (C := C)).LaxMonoidal + instance : (linearization k G).Monoidal := by + instance : (mopFunctor C).Braided + instance : (mopFunctor C).Monoidal + instance : (ofBraided C).Monoidal + instance : (prod F G).LaxMonoidal + instance : (prod F G).OplaxMonoidal + instance : (project f).Monoidal + instance : (shiftMonoidalFunctor C A).Monoidal := HasShift.shiftMonoidal + instance : (tensoringRight C).Monoidal + instance : (unmopFunctor C).Braided + instance : (unmopFunctor C).Monoidal + instance : (𝟭 C).Braided + instance : (𝟭 C).Monoidal + instance : Category (LaxBraidedFunctor C D) + instance : Category (LaxMonoidalFunctor C D) + instance : EnrichedCategory W (TransportEnrichment F C) + instance : F.Monoidal := Functor.Monoidal.ofOplaxMonoidal F + instance : F.OplaxMonoidal + instance : IsIso (ε F) := (εIso F).isIso_hom + instance : IsIso (η F) + instance : IsIso (η F) := (εIso F).isIso_inv + instance : IsIso (η F) := by dsimp [η_eq]; infer_instance + instance : NatTrans.IsMonoidal (equivalenceTransported e).counit + instance : NatTrans.IsMonoidal (equivalenceTransported e).unit + instance : NatTrans.IsMonoidal adj.counit + instance : NatTrans.IsMonoidal adj.unit + instance : NatTrans.IsMonoidal e.counit + instance : NatTrans.IsMonoidal e.inv + instance : NatTrans.IsMonoidal e.unit + instance [F.LaxMonoidal] : (F.mapAction G).LaxMonoidal + instance [F.Monoidal] : (F.mapAction G).Monoidal + instance [F.Monoidal] [G.Monoidal] : (F ⋙ G).Monoidal + instance [F.Monoidal] [G.Monoidal] : (prod F G).Monoidal + instance [F.OplaxMonoidal] : (F.mapAction G).OplaxMonoidal + instance [e.functor.Monoidal] : e.symm.inverse.Monoidal := inferInstanceAs (e.functor.Monoidal) + instance [e.inverse.Monoidal] : e.symm.functor.Monoidal := inferInstanceAs (e.inverse.Monoidal) + instance {F G : C ⥤ D} {H K : C ⥤ E} (α : F ⟶ G) (β : H ⟶ K) + instance {P' : C → Prop} [MonoidalPredicate P'] (h : ∀ ⦃X⦄, P X → P' X) : + inverseMonoidal + isMonoidal_symm + isoOfComponents_hom_hom_app + isoOfComponents_inv_hom_app + left_unitality_hom + left_unitality_inv + lim_ε_π + lim_μ_π + linearization_δ_hom + linearization_η_hom_apply + mapAction_δ_hom + mapAction_ε_hom + mapAction_η_hom + mapAction_μ_hom + map_leftUnitor_inv + map_rightUnitor_inv + map_δ_μ + map_ε_comp_counit_app_unit + map_ε_η + map_η_ε + map_μ_comp_counit_app_tensor + map_μ_δ + mkIso_hom_hom + mkIso_inv_hom + monToLaxMonoidalObj + monToLaxMonoidalObj_ε + monToLaxMonoidalObj_μ + monoidalOfChosenFiniteProducts + mopFunctor_δ + mopFunctor_ε + mopFunctor_η + mopFunctor_μ + obj_η_app + ofBraided_δ_f + ofBraided_ε_f + ofBraided_η_f + ofBraided_μ_f + ofLaxMonoidal + ofOplaxMonoidal + ofTensorHom + ofTensorHom_ε + ofTensorHom_μ + op_tensorμ + oplaxMonoidalOfChosenFiniteProducts + prod'_app_fst + prod'_app_snd + prod'_δ_fst + prod'_δ_snd + prod'_ε_fst + prod'_ε_snd + prod'_η_fst + prod'_η_snd + prod'_μ_fst + prod'_μ_snd + prod_comp_fst + prod_comp_snd + prod_δ_fst + prod_δ_snd + prod_ε_fst + prod_ε_snd + prod_η_fst + prod_η_snd + prod_μ_fst + prod_μ_snd + rightAdjointLaxMonoidal + rightAdjointLaxMonoidal_ε + rightAdjointLaxMonoidal_μ + right_unitality_hom + right_unitality_inv + sheafToPresheafMonoidal + sheafToPresheaf_δ + sheafToPresheaf_ε + sheafToPresheaf_η + sheafToPresheaf_μ + tensor_naturality + tensor_δ + tensor_ε + tensor_η + tensoringRight_δ + tensoringRight_ε + tensoringRight_η + tensoringRight_μ + tensorδ + tensorδ_tensorμ + tensorμ + tensorμ_apply + tensorμ_eq_tensorTensorTensorComm + tensorμ_natural + tensorμ_natural_left + tensorμ_natural_right + tensorμ_tensorδ + toLaxMonoidal + toLaxMonoidalFunctor + toLaxMonoidal_ε + toLaxMonoidal_μ + toMonoidal + toOplaxMonoidal + toOplaxMonoidal_δ + toOplaxMonoidal_η + unitIso_hom_app_comp_inverse_map_η_functor + unitIso_hom_app_tensor_comp_inverse_map_δ_functor + unitIso_hom_app_tensor_comp_inverse_map_δ_functor__ + unit_app_tensor_comp_map_δ + unit_app_unit_comp_map_η + unmopFunctor_δ + unmopFunctor_ε + unmopFunctor_η + unmopFunctor_μ + unop_tensorμ + whiskerLeft_app_tensor_app + whiskerLeft_δ_μ + whiskerLeft_ε_η + whiskerLeft_η_ε + whiskerLeft_μ_δ + whiskerRight_app_tensor_app + whiskerRight_δ_μ + whiskerRight_ε_η + whiskerRight_η_ε + whiskerRight_μ_δ + δ + δ_eq + δ_natural + δ_natural_left + δ_natural_right + δ_naturality + δ_naturalityᵣ + δ_naturalityₗ + δ_of_chosenFiniteProducts + δ_μ_app + εIso_hom_one + εIso_inv_freeMk + ε_η_app + η + η_app_obj + η_eq + η_naturality + η_of_chosenFiniteProducts + η_ε_app + μIso_hom_freeMk_tmul_freeMk + μIso_inv_freeMk + μ_natural_left + μ_natural_right + μ_δ_app ++ associativity_inv ++ comp_hom ++ homMk ++ hom_ext ++ id_hom ++ isoMk ++ isoOfComponents ++ εIso ++ μIso +++ IsMonoidal +++ instance : (forget C).Monoidal ++++ forget_δ ++++ forget_ε ++++ forget_η ++++ forget_μ ++- associativity ++- forget ++- left_unitality ++- right_unitality +-- mkIso +-- prod' - BraidedFunctor - Discrete.braidedFunctor - Functor.toMonoidalFunctorOfChosenFiniteProducts - Functor.toMonoidalFunctorOfHasFiniteProducts - Functor.toOplaxMonoidalFunctorOfChosenFiniteProducts - HasShift.shift_obj_obj - LaxMonoidal.ofTensorHom - LaxMonoidalFunctor.associativity_inv - LaxMonoidalFunctor.left_unitality_inv - LaxMonoidalFunctor.ofTensorHom - LaxMonoidalFunctor.right_unitality_inv - LaxMonoidalFunctor.μ_natural - MonoidalFunctor - MonoidalFunctor.fromOplaxMonoidalFunctor - MonoidalFunctor.toOplaxMonoidalFunctor - MonoidalFunctor.εIso - MonoidalFunctor.μIso - MonoidalNatTrans - OplaxMonoidalFunctor - OplaxMonoidalFunctor.associativity_inv - OplaxMonoidalFunctor.left_unitality_hom - OplaxMonoidalFunctor.right_unitality_hom - OplaxMonoidalFunctor.δ_natural - as - categoryBraidedFunctor - categoryLaxBraidedFunctor - categoryLaxMonoidalFunctor - categoryMonoidalFunctor - chosenFiniteProducts: - comp_toNatTrans_lax - coyonedaTensorUnit - diag - forgetBraided - forgetBraided_faithful - forgetMonoidal_faithful - forget₂Monoidal - forget₂Monoidal_additive - forget₂Monoidal_faithful - forget₂Monoidal_linear - fromInduced - fromTransported - fullBraidedSubcategory.faithful - fullBraidedSubcategory.full - fullBraidedSubcategory.map - fullBraidedSubcategory.mapFull - fullBraidedSubcategory.map_faithful - fullBraidedSubcategoryInclusion - fullMonoidalSubcategory.faithful - fullMonoidalSubcategory.full - fullMonoidalSubcategory.map - fullMonoidalSubcategory.map_faithful - fullMonoidalSubcategory.map_full - fullMonoidalSubcategoryInclusion - fullMonoidalSubcategoryInclusion_additive - fullMonoidalSubcategoryInclusion_linear - functorCategoryMonoidalAdjunction - functorCategoryMonoidalAdjunction.counit_app_app - functorCategoryMonoidalAdjunction.unit_app_hom - functorCategoryMonoidalEquivalence - functorCategoryMonoidalEquivalence.functor_map - functorCategoryMonoidalEquivalence.inverse_map - functorCategoryMonoidalEquivalence.ε_app - functorCategoryMonoidalEquivalence.μIso_inv_app - functorCategoryMonoidalEquivalence.μ_app - functorCategoryMonoidalEquivalenceInverse - instIsEquivalence_fromTransported - instance (A B : C) : IsIso (F.toOplaxMonoidalFunctorOfChosenFiniteProducts.δ A B) - instance (F : LaxMonoidalFunctor C D) : Inhabited (MonoidalNatTrans F F) - instance (F : LaxMonoidalFunctor V W) : EnrichedCategory W (TransportEnrichment F C) - instance (F : LaxMonoidalFunctor.{v₁, v₂} C D) : LaxMonoidal.{v₁, v₂} F.obj - instance (X Y : D) [F.IsEquivalence] : IsIso ((monoidalAdjoint F h).μ X Y) := by - instance (e : C ≌ D) : (toTransported e).IsEquivalence - instance : (functorCategoryMonoidalEquivalence V G).IsEquivalence := by - instance : Inhabited (BraidedFunctor C C) - instance : Inhabited (LaxBraidedFunctor C C) - instance : Inhabited (LaxMonoidalFunctor C C) - instance : Inhabited (MonoidalFunctor C C) - instance : Inhabited (OplaxMonoidalFunctor C C) - instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _) := by - instance : IsIso F.toOplaxMonoidalFunctorOfChosenFiniteProducts.η - instance : LaxMonoidal.{u} (free R).obj := .ofTensorHom - instance : MonoidalCategory (FGModuleCat R) := by - instance [F.IsEquivalence] : F.toMonoidalFunctorOfChosenFiniteProducts.IsEquivalence := by - instance [F.IsEquivalence] : F.toMonoidalFunctorOfHasFiniteProducts.IsEquivalence := by assumption - instance [F.IsEquivalence] : IsIso (monoidalAdjoint F h).ε := by - instance [F.IsEquivalence] : IsIso (monoidalCounit F h) := by - instance [F.IsEquivalence] : IsIso (monoidalUnit F h) := by - isIso_of_isIso_app - laxMonoidalId - limLax - limLax_map - limLax_obj - limLax_obj' - limLax_ε - limLax_μ - limitFunctorial - limitFunctorial_map - limitLaxMonoidal - linearization_ε_inv_hom_apply - linearization_μ_inv_hom - mapAction - mapActionLax - mapAction_ε_inv_hom - mapAction_μ_inv_hom - monoidalAdjoint - monoidalCounit - monoidalFree - monoidalInverse - monoidalSheafToPresheaf - monoidalUnit - mopBraidedFunctor - obj_ε_inv_app - ofComponents - ofComponents.hom_app - ofComponents.inv_app - op_tensor_μ - prod'_toFunctor - prod'_toLaxMonoidalFunctor - prod'_ε - prod'_μ - tensor_μ_apply - tensor_μ_eq_tensorTensorTensorComm - tensor_μ_natural - tensor_μ_natural_left - tensor_μ_natural_right - tensoringRightMonoidal - toLaxBraidedFunctor - toTransported - transportedMonoidalCounitIso - transportedMonoidalUnitIso - unmopBraidedFunctor - unop_tensor_μ - vcomp - εIso_hom - ε_apply - ε_hom_inv_app - ε_hom_inv_id - ε_inv_app_obj - ε_inv_hom_app - ε_inv_hom_id - ε_inv_naturality - μIso_hom - μ_hom_inv_app - μ_hom_inv_id - μ_inv_hom_app - μ_inv_hom_id - μ_inv_naturality - μ_inv_naturalityᵣ - μ_inv_naturalityₗ -++ of -- forgetMonoidal_toFunctor -- forgetMonoidal_ε -- forgetMonoidal_μ -- instance : (toModuleCatBraidedFunctor R).Faithful -- instance : (toModuleCatMonoidalFunctor R).Faithful -- toModuleCatBraidedFunctor -- toModuleCatMonoidalFunctor --- comp_toNatTrans --- ext' --- forgetMonoidal --- prod -----+++ comp ------++++ id

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.

[joelriou]

!bench

[leanprover-bot]

Here are the benchmark results for commit db50785afb30f7576034de1d7a3749b26caa9b65.Found no runs to compare against.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#17761~~ By Dependent Issues (🤖). Happy coding!

[joelriou]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1bc507c7c90614e0cb317c75bfe4e1fa11adb696. There were significant changes against commit d50eac5610440ba3d59f8a4779889ba4ececb1af:

  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 8500e0cf8c57ce50be1e0d9e0d1d902258cdca99. There were significant changes against commit d50eac5610440ba3d59f8a4779889ba4ececb1af:

  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 58ea18e126e026cb5a6d143ad1c11d3f8b570eba. There were significant changes against commit 9d61276a94857b7c19f2e62610a8939880226b02:

  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%

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

[joelriou]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build