Commit 2020-07-28 08:55 ce70305b

View on Github →

feat(category_theory): monoidal_category (C ⥤ D) when D is monoidal (#3571) When C is any category, and D is a monoidal category, there is a natural "pointwise" monoidal structure on C ⥤ D. The initial intended application is tensor product of presheaves.

Estimated changes

Created src/category_theory/monoidal/functor_category.lean

added theorem category_theory.monoidal.associator_hom_app

added theorem category_theory.monoidal.associator_inv_app

added def category_theory.monoidal.functor_category.tensor_hom

added def category_theory.monoidal.functor_category.tensor_obj

added theorem category_theory.monoidal.left_unitor_hom_app

added theorem category_theory.monoidal.left_unitor_inv_app

added theorem category_theory.monoidal.right_unitor_hom_app

added theorem category_theory.monoidal.right_unitor_inv_app

added theorem category_theory.monoidal.tensor_hom_app

added theorem category_theory.monoidal.tensor_obj_map

added theorem category_theory.monoidal.tensor_obj_obj

added theorem category_theory.monoidal.tensor_unit_map

added theorem category_theory.monoidal.tensor_unit_obj