Commit 2023-08-07 12:37 763106d3

View on Github →

feat(CategoryTheory/Monoidal): define whiskering operators (#6420) Extracted from #6307. Just put the whiskerings into the constructor.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

added def ModuleCat.MonoidalCategory.whiskerLeft

added def ModuleCat.MonoidalCategory.whiskerRight

Modified Mathlib/CategoryTheory/Bicategory/End.lean

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

added theorem CategoryTheory.MonoidalCategory.id_tensorHom

added def CategoryTheory.MonoidalCategory.ofTensorHom

added theorem CategoryTheory.MonoidalCategory.tensorHom_def'

added theorem CategoryTheory.MonoidalCategory.tensorHom_id

added theorem CategoryTheory.MonoidalCategory.whisker_exchange

Modified Mathlib/CategoryTheory/Monoidal/Center.lean

Modified Mathlib/CategoryTheory/Monoidal/Discrete.lean

Modified Mathlib/CategoryTheory/Monoidal/End.lean

Modified Mathlib/CategoryTheory/Monoidal/Free/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean

added def CategoryTheory.Monoidal.FunctorCategory.whiskerLeft

added def CategoryTheory.Monoidal.FunctorCategory.whiskerRight

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

Modified Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean

modified def CategoryTheory.monoidalOfChosenFiniteProducts

Modified Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

added theorem CategoryTheory.monoidalOfHasFiniteCoproducts.associator_inv

modified def CategoryTheory.monoidalOfHasFiniteCoproducts

added theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv

modified def CategoryTheory.monoidalOfHasFiniteProducts

Modified Mathlib/CategoryTheory/Monoidal/Opposite.lean

Modified Mathlib/CategoryTheory/Monoidal/Subcategory.lean

Modified Mathlib/CategoryTheory/Monoidal/Transport.lean