Commit 2023-02-18 19:03 e0bb96d6

View on Github →

feat: port CategoryTheory.Monoidal.Category (#2318)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Category.lean

added def CategoryTheory.MonoidalCategory.associatorNatIso

added theorem CategoryTheory.MonoidalCategory.associator_conjugation

added theorem CategoryTheory.MonoidalCategory.associator_inv_conjugation

added theorem CategoryTheory.MonoidalCategory.associator_inv_naturality

added theorem CategoryTheory.MonoidalCategory.comp_tensor_id

added theorem CategoryTheory.MonoidalCategory.dite_tensor

added theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor'

added theorem CategoryTheory.MonoidalCategory.hom_inv_id_tensor

added theorem CategoryTheory.MonoidalCategory.id_tensor_associator_inv_naturality

added theorem CategoryTheory.MonoidalCategory.id_tensor_associator_naturality

added theorem CategoryTheory.MonoidalCategory.id_tensor_comp

added theorem CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id

added theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor'

added theorem CategoryTheory.MonoidalCategory.inv_hom_id_tensor

added theorem CategoryTheory.MonoidalCategory.inv_tensor

added def CategoryTheory.MonoidalCategory.leftAssocTensor

added theorem CategoryTheory.MonoidalCategory.leftAssocTensor_map

added theorem CategoryTheory.MonoidalCategory.leftAssocTensor_obj

added def CategoryTheory.MonoidalCategory.leftUnitorNatIso

added theorem CategoryTheory.MonoidalCategory.leftUnitor_conjugation

added theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality

added theorem CategoryTheory.MonoidalCategory.pentagon_inv

added theorem CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor_hom_fst

added theorem CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor_hom_snd

added theorem CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor_inv_fst

added theorem CategoryTheory.MonoidalCategory.prodMonoidal_leftUnitor_inv_snd

added theorem CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor_hom_fst

added theorem CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor_hom_snd

added theorem CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor_inv_fst

added theorem CategoryTheory.MonoidalCategory.prodMonoidal_rightUnitor_inv_snd

added def CategoryTheory.MonoidalCategory.rightAssocTensor

added theorem CategoryTheory.MonoidalCategory.rightAssocTensor_map

added theorem CategoryTheory.MonoidalCategory.rightAssocTensor_obj

added def CategoryTheory.MonoidalCategory.rightUnitorNatIso

added theorem CategoryTheory.MonoidalCategory.rightUnitor_conjugation

added theorem CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality

added theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor

added theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv

added def CategoryTheory.MonoidalCategory.tensor

added theorem CategoryTheory.MonoidalCategory.tensorHom_inv_id'

added theorem CategoryTheory.MonoidalCategory.tensorHom_inv_id

added def CategoryTheory.MonoidalCategory.tensorLeft

added def CategoryTheory.MonoidalCategory.tensorLeftTensor

added theorem CategoryTheory.MonoidalCategory.tensorLeftTensor_hom_app

added theorem CategoryTheory.MonoidalCategory.tensorLeftTensor_inv_app

added def CategoryTheory.MonoidalCategory.tensorRight

added def CategoryTheory.MonoidalCategory.tensorRightTensor

added theorem CategoryTheory.MonoidalCategory.tensorRightTensor_hom_app

added theorem CategoryTheory.MonoidalCategory.tensorRightTensor_inv_app

added def CategoryTheory.MonoidalCategory.tensorUnitLeft

added def CategoryTheory.MonoidalCategory.tensorUnitRight

added theorem CategoryTheory.MonoidalCategory.tensor_dite

added theorem CategoryTheory.MonoidalCategory.tensor_id_comp_id_tensor

added theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id'

added theorem CategoryTheory.MonoidalCategory.tensor_inv_hom_id

added theorem CategoryTheory.MonoidalCategory.tensor_left_iff

added theorem CategoryTheory.MonoidalCategory.tensor_right_iff

added def CategoryTheory.MonoidalCategory.tensoringLeft

added def CategoryTheory.MonoidalCategory.tensoringRight

added theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv

added theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right

added def CategoryTheory.tensorIso