feat(category_theory/enriched): abstract enriched categories (#7175)

# Enriched categories

We set up the basic theory of `V`-enriched categories,
for `V` an arbitrary monoidal category.

We do not assume here that `V` is a concrete category,
so there does not need to be a "honest" underlying category!

Use `X ⟶[V] Y` to obtain the `V` object of morphisms from `X` to `Y`.

This file contains the definitions of `V`-enriched categories and
`V`-functors.

We don't yet define the `V`-object of natural transformations
between a pair of `V`-functors (this requires limits in `V`),
but we do provide a presheaf isomorphic to the Yoneda embedding of this object.

We verify that when `V = Type v`, all these notion reduce to the usual ones.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/category/Module/adjunctions.lean

@@ -67,7 +67,7 @@ instance : lax_monoidal.{u} (free R).obj :=
     ext x x' ⟨y, y'⟩,
     -- This is rather tedious: it's a terminal simp, with no arguments,
     -- but between the four of them it is too slow.
-    simp only [tensor_product.mk_apply, mul_one, monoidal.tensor_apply, monoidal_category.hom_apply,
+    simp only [tensor_product.mk_apply, mul_one, tensor_apply, monoidal_category.hom_apply,
       Module.free_map, Module.coe_comp, map_functorial_obj,
       linear_map.compr₂_apply, linear_equiv.coe_to_linear_map, linear_map.comp_apply,
       function.comp_app,
@@ -79,7 +79,7 @@ instance : lax_monoidal.{u} (free R).obj :=
     ext,
     simp only [tensor_product.mk_apply, mul_one,
       Module.id_apply, Module.free_map, Module.coe_comp, map_functorial_obj,
-      Module.monoidal_category.hom_apply, monoidal.left_unitor_hom_apply,
+      Module.monoidal_category.hom_apply, left_unitor_hom_apply,
       Module.monoidal_category.left_unitor_hom_apply,
       linear_map.compr₂_apply, linear_equiv.coe_to_linear_map, linear_map.comp_apply,
       function.comp_app,
@@ -91,7 +91,7 @@ instance : lax_monoidal.{u} (free R).obj :=
     ext,
     simp only [tensor_product.mk_apply, mul_one,
       Module.id_apply, Module.free_map, Module.coe_comp, map_functorial_obj,
-      Module.monoidal_category.hom_apply, monoidal.right_unitor_hom_apply,
+      Module.monoidal_category.hom_apply, right_unitor_hom_apply,
       Module.monoidal_category.right_unitor_hom_apply,
       linear_map.compr₂_apply, linear_equiv.coe_to_linear_map, linear_map.comp_apply,
       function.comp_app,
@@ -103,7 +103,7 @@ instance : lax_monoidal.{u} (free R).obj :=
     ext,
     simp only [tensor_product.mk_apply, mul_one,
       Module.id_apply, Module.free_map, Module.coe_comp, map_functorial_obj,
-      Module.monoidal_category.hom_apply, monoidal.associator_hom_apply,
+      Module.monoidal_category.hom_apply, associator_hom_apply,
       Module.monoidal_category.associator_hom_apply,
       linear_map.compr₂_apply, linear_equiv.coe_to_linear_map, linear_map.comp_apply,
       function.comp_app,