Commit 2022-04-12 17:21 c994ab3f

View on Github →

feat(category_theory/monoidal): define a monoidal structure on the tensor product functor of a braided monoidal category (#13150) Given a braided monoidal category C, equip its tensor product functor, viewed as a functor from C × C to C with a strength that turns it into a monoidal functor. See #13033 for a discussion of the motivation of this definition. (This PR replaces #13034 which was accidentally closed.)

Estimated changes

Modified docs/references.bib

Modified src/category_theory/monoidal/braided.lean

added theorem category_theory.left_unitor_inv_braiding

added theorem category_theory.right_unitor_inv_braiding

added theorem category_theory.tensor_associativity

added theorem category_theory.tensor_associativity_aux

added theorem category_theory.tensor_left_unitality

added def category_theory.tensor_monoidal

added theorem category_theory.tensor_right_unitality

added def category_theory.tensor_μ

added theorem category_theory.tensor_μ_def₁

added theorem category_theory.tensor_μ_def₂

added theorem category_theory.tensor_μ_natural

Modified src/category_theory/monoidal/category.lean

modified def category_theory.monoidal_category.tensor