Commit 2023-06-02 10:22 2ce27d01

View on Github →

feat: port CategoryTheory.Monoidal.Rigid.Basic (#4563)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean

added def CategoryTheory.ExactPairing.coevaluation

added theorem CategoryTheory.ExactPairing.coevaluation_evaluation

added def CategoryTheory.ExactPairing.evaluation

added theorem CategoryTheory.ExactPairing.evaluation_coevaluation

added def CategoryTheory.closedOfHasLeftDual

added theorem CategoryTheory.coevaluation_comp_leftAdjointMate

added theorem CategoryTheory.coevaluation_comp_rightAdjointMate

added theorem CategoryTheory.comp_leftAdjointMate

added theorem CategoryTheory.comp_rightAdjointMate

added def CategoryTheory.exactPairingCongr

added def CategoryTheory.exactPairingCongrLeft

added def CategoryTheory.exactPairingCongrRight

added def CategoryTheory.leftAdjointMate

added theorem CategoryTheory.leftAdjointMate_comp

added theorem CategoryTheory.leftAdjointMate_comp_evaluation

added theorem CategoryTheory.leftAdjointMate_id

added def CategoryTheory.leftDualIso

added theorem CategoryTheory.leftDualIso_id

added theorem CategoryTheory.leftDual_rightDual

added def CategoryTheory.monoidalClosedOfLeftRigidCategory

added def CategoryTheory.rightAdjointMate

added theorem CategoryTheory.rightAdjointMate_comp

added theorem CategoryTheory.rightAdjointMate_comp_evaluation

added theorem CategoryTheory.rightAdjointMate_id

added def CategoryTheory.rightDualIso

added theorem CategoryTheory.rightDualIso_id

added theorem CategoryTheory.rightDual_leftDual

added def CategoryTheory.tensorLeftAdjunction

added def CategoryTheory.tensorLeftHomEquiv

added theorem CategoryTheory.tensorLeftHomEquiv_id_tensor_comp_evaluation

added theorem CategoryTheory.tensorLeftHomEquiv_naturality

added theorem CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_id_tensor

added theorem CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_tensor_id

added theorem CategoryTheory.tensorLeftHomEquiv_symm_naturality

added theorem CategoryTheory.tensorLeftHomEquiv_tensor

added theorem CategoryTheory.tensorLeftHomEquiv_tensor_id_comp_evaluation

added def CategoryTheory.tensorRightAdjunction

added def CategoryTheory.tensorRightHomEquiv

added theorem CategoryTheory.tensorRightHomEquiv_id_tensor_comp_evaluation

added theorem CategoryTheory.tensorRightHomEquiv_naturality

added theorem CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_id_tensor

added theorem CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_tensor_id

added theorem CategoryTheory.tensorRightHomEquiv_symm_naturality

added theorem CategoryTheory.tensorRightHomEquiv_tensor

added theorem CategoryTheory.tensorRightHomEquiv_tensor_id_comp_evaluation