Commit 2021-09-12 06:48 b55483ae

View on Github →

feat(category_theory/monoidal): rigid (autonomous) monoidal categories (#8946) Defines rigid monoidal categories and creates the instance of finite dimensional vector spaces.

Estimated changes

Created src/algebra/category/FinVect.lean

added def FinVect.FinVect_coevaluation

added theorem FinVect.FinVect_coevaluation_apply_one

added def FinVect.FinVect_dual

added def FinVect.FinVect_evaluation

added theorem FinVect.FinVect_evaluation_apply

added def FinVect

Modified src/algebra/category/Module/monoidal.lean

added theorem Module.monoidal_category.associator_inv_apply

added theorem Module.monoidal_category.left_unitor_inv_apply

added theorem Module.monoidal_category.right_unitor_inv_apply

Modified src/category_theory/monoidal/category.lean

added theorem category_theory.monoidal_category.associator_conjugation

added theorem category_theory.monoidal_category.associator_inv_conjugation

added def category_theory.monoidal_category.full_monoidal_subcategory

added theorem category_theory.monoidal_category.id_tensor_right_unitor_inv

added theorem category_theory.monoidal_category.left_unitor_inv_comp_tensor

added theorem category_theory.monoidal_category.left_unitor_inv_tensor_id

added theorem category_theory.monoidal_category.pentagon_comp_id_tensor

added theorem category_theory.monoidal_category.pentagon_hom_inv

added theorem category_theory.monoidal_category.pentagon_inv_hom

added theorem category_theory.monoidal_category.pentagon_inv_inv_hom

added theorem category_theory.monoidal_category.right_unitor_inv_comp_tensor

Created src/category_theory/monoidal/rigid.lean

added theorem category_theory.comp_left_adjoint_mate

added theorem category_theory.comp_right_adjoint_mate

added def category_theory.left_adjoint_mate

added theorem category_theory.left_adjoint_mate_comp

added theorem category_theory.left_adjoint_mate_id

added def category_theory.left_dual_iso

added theorem category_theory.left_dual_iso_id

added theorem category_theory.left_dual_right_dual

added def category_theory.right_adjoint_mate

added theorem category_theory.right_adjoint_mate_comp

added theorem category_theory.right_adjoint_mate_id

added def category_theory.right_dual_iso

added theorem category_theory.right_dual_iso_id

added theorem category_theory.right_dual_left_dual

Created src/linear_algebra/coevaluation.lean

added def coevaluation

added theorem coevaluation_apply_one

added theorem contract_left_assoc_coevaluation'

added theorem contract_left_assoc_coevaluation

Modified src/linear_algebra/finsupp_vector_space.lean

deleted def finsupp.basis.tensor_product

Created src/linear_algebra/tensor_product_basis.lean

added def basis.tensor_product