Commit 2024-01-25 12:14 d3da7bbc

View on Github →

refactor(CategoryTheory/Monoidal): replace axioms with those more suitable for the whiskerings (#9991) Extracted from #6307. We replace some axioms by those more preferable when using the whiskerings instead of the tensor of morphisms.

Estimated changes

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

Modified Mathlib/CategoryTheory/Monoidal/Braided.lean

added theorem CategoryTheory.BraidedCategory.braiding_inv_tensor_left

added theorem CategoryTheory.BraidedCategory.braiding_inv_tensor_right

added theorem CategoryTheory.BraidedCategory.braiding_naturality

added theorem CategoryTheory.BraidedCategory.braiding_tensor_left

added theorem CategoryTheory.BraidedCategory.braiding_tensor_right

Modified Mathlib/CategoryTheory/Monoidal/Center.lean

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

added theorem CategoryTheory.MonoidalFunctor.map_whiskerLeft

added theorem CategoryTheory.MonoidalFunctor.map_whiskerRight

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

Modified Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

Modified Mathlib/CategoryTheory/Monoidal/Preadditive.lean

added theorem CategoryTheory.MonoidalPreadditive.add_tensor

added theorem CategoryTheory.MonoidalPreadditive.tensor_add

added theorem CategoryTheory.MonoidalPreadditive.tensor_zero

added theorem CategoryTheory.MonoidalPreadditive.zero_tensor