feat(CategoryTheory/Enriched/Limits): define cotensors in an enriched category

[daniel-carranza]

Defines the notion of cotensors in a V-category C, where V is a braided monoidal category. Proves that V itself has all cotensors when viewed as a category enriched in V. Also proves that if C has all cotensors and V is additionally symmetric then the cotensors form a V-functor from the enriched tensor productV\op \times C to C.

---

This work originates from the infinity-cosmos project, where the dual theory of tensors was formalized by @arnoudvanderleer .

The current version of this code introduces an abbrev definition Ehom V C x y for the hom-object C(x, y) in V. The intention is to make the code easier to both to write and read; the existing notation x \hom[V] y throws an error when instantiated at C = V (ambiguous term; Possible interpretations: (ihom x).obj y : V x ⟶[V] y : V). A possibly related issue is there are a few calls to erw that stem from a failure to identify (ihom x).obj : V with Ehom V V x y. Any help with these issues, or any other assistance, is greatly appreciated!

• depends on: feat(CategoryTheory/Enriched): tensor product of enriched categories #35144 [required to prove V-functoriality of cotensors]
• depends on: [Merged by Bors] - feat(CategoryTheory/Monoidal/Closed): Prove the isomorphism of internal hom objects C(x \otimes y, z) and C(y, C(x, z)) #35436 [required to prove that V admits all cotensors by itself]

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 33a2f73096

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying (new file)	444
Mathlib.CategoryTheory.Enriched.TensorProductCategory (new file)	637
Mathlib.CategoryTheory.Enriched.Limits.Cotensors (new file)	648

---

Declarations diff

+ Cotensor
+ Cotensor.coneNatTransIso
+ CotensoredCategory
+ Ehom
+ EhomPrecompose
+ EhomPrecompose_coneNatTrans_eq
+ EhomPrecompose_selfEval_comp_eq
+ EnrichedBifunctor
+ Ihom
+ IhomPrecompose
+ IhomPrecompose_coneNatTrans_eq
+ IhomPrecompose_selfEval_comp_eq
+ Precotensor
+ Precotensor.coneNatTrans
+ Precotensor.coneNatTrans_braid_eq
+ Precotensor.coneNatTrans_eq
+ braiding_inv_tensorμ
+ braiding_inv_unit_unit_eq_id
+ braiding_tensorμ
+ braiding_unit_unit_eq_id
+ braiding_unit_unit_hom_eq_inv
+ comp_tensor_comp_eq_comp_mid_left_right
+ cotensor_bifunc
+ cotensor_prod_func
+ enrichedBifunctorEquiv
+ enrichedBifunctorEquiv.from
+ enrichedBifunctorEquiv.to
+ enrichedTensorProduct
+ internalHomCurry
+ internalHomCurryIso
+ internalHomCurry_PrecotensorCone_eq
+ internalHomCurry_uncurry_eq
+ internalHomCurry_uncurry_uncurry_eq
+ internalHomUncurry
+ internalHomUncurry_uncurry_eq
+ internalHom_curry_uncurry
+ internalHom_uncurry_curry
+ post_pre_eq_pre_post
+ postcompose
+ postcompose_comp_eq
+ postcompose_coneNatTrans_eq
+ postcompose_id_eq
+ postcompose_selfEval_comp_eq
+ precompose_comp_eq
+ precompose_id_eq
+ selfEnrichedCotensor
+ selfEnrichedPrecotensor
+ selfEnrichedPrecotensorCone
+ selfEnrichedPrecotensor_cone_eq
+ tensor_eComp_eq
+ tensor_eId_eq
+ tensorδ_unit_unit_eq_id
+ tensorμ_iso
+ tensorμ_unit_unit_eq_id
+ tensorμ_unit_unit_tensorδ
+ uncurry_postcompose_coneNatTrans_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (20.00, 0.03)

Current number	Change	Type
650	20	erw

Current commit eec6fd0aff
Reference commit 33a2f73096

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CategoryTheory/Enriched): tensor product of enriched categories #35144
• [Merged by Bors] - feat(CategoryTheory/Monoidal/Closed): Prove the isomorphism of internal hom objects C(x \otimes y, z) and C(y, C(x, z)) #35436
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.