Basic

📁 Source: Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean

Statistics

Metric	Count
Definitions ExactPairing, coevaluation, coevaluation', evaluation, evaluation', termε_, termη_, HasLeftDual, exact, leftDual, HasRightDual, exact, rightDual, LeftRigidCategory, leftDual, RightRigidCategory, rightDual, RigidCategory, toLeftRigidCategory, toRightRigidCategory, closedOfHasLeftDual, exactPairingCongr, exactPairingCongrLeft, exactPairingCongrRight, exactPairingUnit, hasLeftDualRightDual, hasLeftDualUnit, hasRightDualLeftDual, hasRightDualUnit, leftAdjointMate, leftDualIso, monoidalClosedOfLeftRigidCategory, rightAdjointMate, rightDualIso, tensorLeftAdjunction, tensorLeftHomEquiv, tensorRightAdjunction, tensorRightHomEquiv, «term_ᘁ_1», «term_ᘁ», «termᘁ__1», «termᘁ_»	42
Theorems coevaluation_evaluation, coevaluation_evaluation', coevaluation_evaluation'', coevaluation_evaluation_assoc, evaluation_coevaluation, evaluation_coevaluation', evaluation_coevaluation'', evaluation_coevaluation_assoc, coevaluation_comp_leftAdjointMate, coevaluation_comp_leftAdjointMate_assoc, coevaluation_comp_rightAdjointMate, coevaluation_comp_rightAdjointMate_assoc, comp_leftAdjointMate, comp_leftAdjointMate_assoc, comp_rightAdjointMate, comp_rightAdjointMate_assoc, leftAdjointMate_comp, leftAdjointMate_comp_evaluation, leftAdjointMate_comp_evaluation_assoc, leftAdjointMate_id, leftDualIso_id, leftDual_rightDual, rightAdjointMate_comp, rightAdjointMate_comp_evaluation, rightAdjointMate_comp_evaluation_assoc, rightAdjointMate_id, rightDualIso_id, rightDual_leftDual, tensorLeftHomEquiv_naturality, tensorLeftHomEquiv_symm_coevaluation_comp_whiskerLeft, tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight, tensorLeftHomEquiv_symm_naturality, tensorLeftHomEquiv_tensor, tensorLeftHomEquiv_whiskerLeft_comp_evaluation, tensorLeftHomEquiv_whiskerRight_comp_evaluation, tensorRightHomEquiv_naturality, tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft, tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight, tensorRightHomEquiv_symm_naturality, tensorRightHomEquiv_tensor, tensorRightHomEquiv_whiskerLeft_comp_evaluation, tensorRightHomEquiv_whiskerRight_comp_evaluation	42
Total	84

CategoryTheory

Definitions

Name	Category	Theorems
ExactPairing 📖	CompData	—
HasLeftDual 📖	CompData	—
HasRightDual 📖	CompData	—
LeftRigidCategory 📖	CompData	—
RightRigidCategory 📖	CompData	—
RigidCategory 📖	CompData	—
closedOfHasLeftDual 📖	CompOp	—
exactPairingCongr 📖	CompOp	—
exactPairingCongrLeft 📖	CompOp	—
exactPairingCongrRight 📖	CompOp	—
exactPairingUnit 📖	CompOp	—
hasLeftDualRightDual 📖	CompOp	1 math math: leftDual_rightDual
hasLeftDualUnit 📖	CompOp	—
hasRightDualLeftDual 📖	CompOp	1 math math: rightDual_leftDual
hasRightDualUnit 📖	CompOp	—
leftAdjointMate 📖	CompOp	12 math math: coevaluation_comp_leftAdjointMate_assoc, leftAdjointMate_id, comp_leftAdjointMate_assoc, tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft, leftDualFunctor_map, leftAdjointMate_comp_evaluation, leftAdjointMate_comp_evaluation_assoc, coevaluation_comp_leftAdjointMate, comp_leftAdjointMate, leftAdjointMate_comp, Action.leftDual_ρ, tensorLeftHomEquiv_whiskerRight_comp_evaluation
leftDualIso 📖	CompOp	1 math math: leftDualIso_id
monoidalClosedOfLeftRigidCategory 📖	CompOp	—
rightAdjointMate 📖	CompOp	12 math math: Action.rightDual_ρ, tensorRightHomEquiv_whiskerLeft_comp_evaluation, rightAdjointMate_comp_evaluation_assoc, comp_rightAdjointMate, comp_rightAdjointMate_assoc, rightDualFunctor_map, coevaluation_comp_rightAdjointMate, rightAdjointMate_id, tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight, rightAdjointMate_comp, rightAdjointMate_comp_evaluation, coevaluation_comp_rightAdjointMate_assoc
rightDualIso 📖	CompOp	1 math math: rightDualIso_id
tensorLeftAdjunction 📖	CompOp	—
tensorLeftHomEquiv 📖	CompOp	7 math math: tensorLeftHomEquiv_symm_coevaluation_comp_whiskerLeft, tensorLeftHomEquiv_naturality, tensorLeftHomEquiv_tensor, tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight, tensorLeftHomEquiv_whiskerLeft_comp_evaluation, tensorLeftHomEquiv_whiskerRight_comp_evaluation, tensorLeftHomEquiv_symm_naturality
tensorRightAdjunction 📖	CompOp	—
tensorRightHomEquiv 📖	CompOp	7 math math: tensorRightHomEquiv_symm_naturality, tensorRightHomEquiv_whiskerLeft_comp_evaluation, tensorRightHomEquiv_whiskerRight_comp_evaluation, tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight, tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft, tensorRightHomEquiv_naturality, tensorRightHomEquiv_tensor
«term_ᘁ_1» 📖	CompOp	—
«term_ᘁ» 📖	CompOp	—
«termᘁ__1» 📖	CompOp	—
«termᘁ_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coevaluation_comp_leftAdjointMate 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorObj HasLeftDual.leftDual ExactPairing.coevaluation HasLeftDual.exact MonoidalCategoryStruct.whiskerRight leftAdjointMate MonoidalCategoryStruct.whiskerLeft	—	Equiv.injective tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft
coevaluation_comp_leftAdjointMate_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorObj HasLeftDual.leftDual ExactPairing.coevaluation HasLeftDual.exact MonoidalCategoryStruct.whiskerRight leftAdjointMate MonoidalCategoryStruct.whiskerLeft	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coevaluation_comp_leftAdjointMate
coevaluation_comp_rightAdjointMate 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorObj HasRightDual.rightDual ExactPairing.coevaluation HasRightDual.exact MonoidalCategoryStruct.whiskerLeft rightAdjointMate MonoidalCategoryStruct.whiskerRight	—	Equiv.injective tensorLeftHomEquiv_symm_coevaluation_comp_whiskerLeft tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight
coevaluation_comp_rightAdjointMate_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorObj HasRightDual.rightDual ExactPairing.coevaluation HasRightDual.exact MonoidalCategoryStruct.whiskerLeft rightAdjointMate MonoidalCategoryStruct.whiskerRight	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coevaluation_comp_rightAdjointMate
comp_leftAdjointMate 📖	mathematical	—	leftAdjointMate CategoryStruct.comp Category.toCategoryStruct HasLeftDual.leftDual	—	leftAdjointMate_comp MonoidalCategory.whiskerLeft_comp Category.assoc MonoidalCategory.tensorHom_def Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_whisker Mathlib.Tactic.Monoidal.eval_monoidalComp Mathlib.Tactic.Monoidal.evalWhiskerLeft_id Mathlib.Tactic.Monoidal.evalWhiskerRight_comp Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_leftUnitor Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_whiskerLeft Mathlib.Tactic.Monoidal.naturality_rightUnitor MonoidalCategory.whisker_exchange Mathlib.Tactic.Monoidal.evalWhiskerRight_id Mathlib.Tactic.Monoidal.evalWhiskerLeft_comp ExactPairing.coevaluation_evaluation''
comp_leftAdjointMate_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct HasLeftDual.leftDual leftAdjointMate	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_leftAdjointMate
comp_rightAdjointMate 📖	mathematical	—	rightAdjointMate CategoryStruct.comp Category.toCategoryStruct HasRightDual.rightDual	—	rightAdjointMate_comp MonoidalCategory.comp_whiskerRight Category.assoc MonoidalCategory.tensorHom_def' Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.Monoidal.eval_monoidalComp Mathlib.Tactic.Monoidal.evalWhiskerRight_id Mathlib.Tactic.Monoidal.evalWhiskerLeft_comp Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_leftUnitor Mathlib.Tactic.Monoidal.naturality_rightUnitor Mathlib.Tactic.Monoidal.naturality_whiskerLeft Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_whiskerRight MonoidalCategory.whisker_exchange Mathlib.Tactic.Monoidal.evalWhiskerLeft_id Mathlib.Tactic.Monoidal.evalWhiskerRight_comp Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_whisker ExactPairing.evaluation_coevaluation''
comp_rightAdjointMate_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct HasRightDual.rightDual rightAdjointMate	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_rightAdjointMate
leftAdjointMate_comp 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct HasLeftDual.leftDual leftAdjointMate MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.leftUnitor MonoidalCategoryStruct.whiskerRight ExactPairing.coevaluation HasLeftDual.exact MonoidalCategoryStruct.tensorHom Iso.hom MonoidalCategoryStruct.associator MonoidalCategoryStruct.whiskerLeft ExactPairing.evaluation MonoidalCategoryStruct.rightUnitor	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_whisker Mathlib.Tactic.Monoidal.eval_monoidalComp Mathlib.Tactic.Monoidal.evalWhiskerRight_id Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_leftUnitor Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_whiskerLeft Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_rightUnitor MonoidalCategory.whisker_exchange MonoidalCategory.tensorHom_def' Mathlib.Tactic.Monoidal.evalWhiskerRight_comp
leftAdjointMate_comp_evaluation 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct HasLeftDual.leftDual MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.whiskerLeft leftAdjointMate ExactPairing.evaluation HasLeftDual.exact MonoidalCategoryStruct.whiskerRight	—	Equiv.injective tensorLeftHomEquiv_whiskerLeft_comp_evaluation tensorLeftHomEquiv_whiskerRight_comp_evaluation
leftAdjointMate_comp_evaluation_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct HasLeftDual.leftDual MonoidalCategoryStruct.whiskerLeft leftAdjointMate MonoidalCategoryStruct.tensorUnit ExactPairing.evaluation HasLeftDual.exact MonoidalCategoryStruct.whiskerRight	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftAdjointMate_comp_evaluation
leftAdjointMate_id 📖	mathematical	—	leftAdjointMate CategoryStruct.id Category.toCategoryStruct HasLeftDual.leftDual	—	MonoidalCategory.whiskerLeft_id MonoidalCategory.id_whiskerRight Category.id_comp ExactPairing.evaluation_coevaluation_assoc Iso.inv_hom_id Category.comp_id
leftDualIso_id 📖	mathematical	—	leftDualIso Iso.refl	—	Iso.ext leftAdjointMate_id
leftDual_rightDual 📖	mathematical	—	HasLeftDual.leftDual HasRightDual.rightDual hasLeftDualRightDual	—	—
rightAdjointMate_comp 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct HasRightDual.rightDual rightAdjointMate MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.rightUnitor MonoidalCategoryStruct.whiskerLeft ExactPairing.coevaluation HasRightDual.exact MonoidalCategoryStruct.tensorHom MonoidalCategoryStruct.associator MonoidalCategoryStruct.whiskerRight ExactPairing.evaluation Iso.hom MonoidalCategoryStruct.leftUnitor	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.Monoidal.eval_monoidalComp Mathlib.Tactic.Monoidal.evalWhiskerLeft_id Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_rightUnitor Mathlib.Tactic.Monoidal.naturality_whiskerLeft Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_leftUnitor MonoidalCategory.whisker_exchange MonoidalCategory.tensorHom_def Mathlib.Tactic.Monoidal.evalWhiskerLeft_comp
rightAdjointMate_comp_evaluation 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct HasRightDual.rightDual MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.whiskerRight rightAdjointMate ExactPairing.evaluation HasRightDual.exact MonoidalCategoryStruct.whiskerLeft	—	Equiv.injective tensorRightHomEquiv_whiskerRight_comp_evaluation tensorRightHomEquiv_whiskerLeft_comp_evaluation
rightAdjointMate_comp_evaluation_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct HasRightDual.rightDual MonoidalCategoryStruct.whiskerRight rightAdjointMate MonoidalCategoryStruct.tensorUnit ExactPairing.evaluation HasRightDual.exact MonoidalCategoryStruct.whiskerLeft	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightAdjointMate_comp_evaluation
rightAdjointMate_id 📖	mathematical	—	rightAdjointMate CategoryStruct.id Category.toCategoryStruct HasRightDual.rightDual	—	MonoidalCategory.id_whiskerRight MonoidalCategory.whiskerLeft_id Category.id_comp ExactPairing.coevaluation_evaluation_assoc Iso.inv_hom_id Category.comp_id
rightDualIso_id 📖	mathematical	—	rightDualIso Iso.refl	—	Iso.ext rightAdjointMate_id
rightDual_leftDual 📖	mathematical	—	HasRightDual.rightDual HasLeftDual.leftDual hasRightDualLeftDual	—	—
tensorLeftHomEquiv_naturality 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EquivLike.toFunLike Equiv.instEquivLike tensorLeftHomEquiv CategoryStruct.comp MonoidalCategoryStruct.whiskerLeft	—	MonoidalCategory.whiskerLeft_comp Category.assoc
tensorLeftHomEquiv_symm_coevaluation_comp_whiskerLeft 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorObj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm tensorLeftHomEquiv CategoryStruct.comp ExactPairing.coevaluation MonoidalCategoryStruct.whiskerLeft Iso.hom MonoidalCategoryStruct.rightUnitor	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.eval_monoidalComp Mathlib.Tactic.Monoidal.evalWhiskerLeft_comp Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_whiskerLeft Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_leftUnitor MonoidalCategory.whisker_exchange Mathlib.Tactic.Monoidal.evalWhiskerLeft_id ExactPairing.coevaluation_evaluation'' Mathlib.Tactic.Monoidal.naturality_rightUnitor
tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorObj HasRightDual.rightDual EquivLike.toFunLike Equiv.instEquivLike Equiv.symm tensorLeftHomEquiv HasRightDual.exact CategoryStruct.comp ExactPairing.coevaluation MonoidalCategoryStruct.whiskerRight Iso.hom MonoidalCategoryStruct.rightUnitor rightAdjointMate	—	MonoidalCategory.whiskerLeft_comp Category.assoc Iso.hom_inv_id_assoc
tensorLeftHomEquiv_symm_naturality 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm tensorLeftHomEquiv CategoryStruct.comp MonoidalCategoryStruct.whiskerLeft	—	MonoidalCategory.whiskerLeft_comp Category.assoc
tensorLeftHomEquiv_tensor 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm tensorLeftHomEquiv CategoryStruct.comp MonoidalCategoryStruct.tensorHom Iso.hom MonoidalCategoryStruct.associator Iso.inv	—	MonoidalCategory.whiskerRight_tensor Category.assoc MonoidalCategory.tensorHom_def' MonoidalCategory.whiskerLeft_comp MonoidalCategory.pentagon_hom_inv_inv_inv_inv_assoc MonoidalCategory.tensor_whiskerLeft MonoidalCategory.comp_whiskerRight MonoidalCategory.whisker_assoc MonoidalCategory.leftUnitor_whiskerRight Iso.inv_hom_id_assoc
tensorLeftHomEquiv_whiskerLeft_comp_evaluation 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit HasLeftDual.leftDual EquivLike.toFunLike Equiv.instEquivLike tensorLeftHomEquiv HasLeftDual.exact CategoryStruct.comp MonoidalCategoryStruct.whiskerLeft ExactPairing.evaluation Iso.inv MonoidalCategoryStruct.rightUnitor	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.eval_monoidalComp Mathlib.Tactic.Monoidal.evalWhiskerLeft_comp Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_leftUnitor Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_whiskerLeft MonoidalCategory.whisker_exchange Mathlib.Tactic.Monoidal.evalWhiskerLeft_id ExactPairing.evaluation_coevaluation'' Mathlib.Tactic.Monoidal.naturality_rightUnitor
tensorLeftHomEquiv_whiskerRight_comp_evaluation 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct HasLeftDual.leftDual MonoidalCategoryStruct.tensorUnit EquivLike.toFunLike Equiv.instEquivLike tensorLeftHomEquiv HasLeftDual.exact CategoryStruct.comp MonoidalCategoryStruct.whiskerRight ExactPairing.evaluation leftAdjointMate Iso.inv MonoidalCategoryStruct.rightUnitor	—	MonoidalCategory.whiskerLeft_comp MonoidalCategory.whisker_assoc Category.assoc Iso.inv_hom_id_assoc Iso.hom_inv_id Category.comp_id
tensorRightHomEquiv_naturality 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EquivLike.toFunLike Equiv.instEquivLike tensorRightHomEquiv CategoryStruct.comp MonoidalCategoryStruct.whiskerRight	—	MonoidalCategory.comp_whiskerRight Category.assoc
tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorObj HasLeftDual.leftDual EquivLike.toFunLike Equiv.instEquivLike Equiv.symm tensorRightHomEquiv HasLeftDual.exact CategoryStruct.comp ExactPairing.coevaluation MonoidalCategoryStruct.whiskerLeft Iso.hom MonoidalCategoryStruct.leftUnitor leftAdjointMate	—	MonoidalCategory.comp_whiskerRight MonoidalCategory.whisker_assoc Category.assoc Iso.inv_hom_id_assoc Iso.hom_inv_id_assoc
tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorObj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm tensorRightHomEquiv CategoryStruct.comp ExactPairing.coevaluation MonoidalCategoryStruct.whiskerRight Iso.hom MonoidalCategoryStruct.leftUnitor	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.eval_monoidalComp Mathlib.Tactic.Monoidal.evalWhiskerRight_comp Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_whiskerLeft Mathlib.Tactic.Monoidal.naturality_rightUnitor MonoidalCategory.whisker_exchange Mathlib.Tactic.Monoidal.evalWhiskerRight_id ExactPairing.evaluation_coevaluation'' Mathlib.Tactic.Monoidal.naturality_leftUnitor
tensorRightHomEquiv_symm_naturality 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm tensorRightHomEquiv CategoryStruct.comp MonoidalCategoryStruct.whiskerRight	—	MonoidalCategory.comp_whiskerRight Category.assoc
tensorRightHomEquiv_tensor 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm tensorRightHomEquiv CategoryStruct.comp MonoidalCategoryStruct.tensorHom Iso.inv MonoidalCategoryStruct.associator Iso.hom	—	MonoidalCategory.tensor_whiskerLeft Category.assoc MonoidalCategory.tensorHom_def MonoidalCategory.comp_whiskerRight MonoidalCategory.whisker_assoc MonoidalCategory.pentagon_inv_hom_hom_hom_hom_assoc Iso.inv_hom_id_assoc MonoidalCategory.whiskerRight_tensor MonoidalCategory.whiskerLeft_comp MonoidalCategory.whiskerLeft_rightUnitor Iso.hom_inv_id_assoc
tensorRightHomEquiv_whiskerLeft_comp_evaluation 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct HasRightDual.rightDual MonoidalCategoryStruct.tensorUnit EquivLike.toFunLike Equiv.instEquivLike tensorRightHomEquiv HasRightDual.exact CategoryStruct.comp MonoidalCategoryStruct.whiskerLeft ExactPairing.evaluation rightAdjointMate Iso.inv MonoidalCategoryStruct.leftUnitor	—	MonoidalCategory.comp_whiskerRight MonoidalCategory.whisker_assoc Category.assoc Iso.inv_hom_id_assoc Iso.hom_inv_id Category.comp_id
tensorRightHomEquiv_whiskerRight_comp_evaluation 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit HasRightDual.rightDual EquivLike.toFunLike Equiv.instEquivLike tensorRightHomEquiv HasRightDual.exact CategoryStruct.comp MonoidalCategoryStruct.whiskerRight ExactPairing.evaluation Iso.inv MonoidalCategoryStruct.leftUnitor	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.Monoidal.eval_monoidalComp Mathlib.Tactic.Monoidal.evalWhiskerRight_comp Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_rightUnitor Mathlib.Tactic.Monoidal.naturality_whiskerLeft Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_whiskerRight MonoidalCategory.whisker_exchange Mathlib.Tactic.Monoidal.evalWhiskerRight_id ExactPairing.coevaluation_evaluation'' Mathlib.Tactic.Monoidal.naturality_leftUnitor

CategoryTheory.ExactPairing

Definitions

Name	Category	Theorems
coevaluation 📖	CompOp	16 math math: CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerLeft, coevaluation_evaluation'', evaluation_coevaluation, CategoryTheory.coevaluation_comp_leftAdjointMate_assoc, CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight, CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft, evaluation_coevaluation'', CategoryTheory.coevaluation_comp_rightAdjointMate, evaluation_coevaluation_assoc, coevaluation_evaluation, CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight, CategoryTheory.coevaluation_comp_leftAdjointMate, CategoryTheory.leftAdjointMate_comp, coevaluation_evaluation_assoc, CategoryTheory.rightAdjointMate_comp, CategoryTheory.coevaluation_comp_rightAdjointMate_assoc
coevaluation' 📖	CompOp	2 math math: coevaluation_evaluation', evaluation_coevaluation'
evaluation 📖	CompOp	16 math math: coevaluation_evaluation'', evaluation_coevaluation, CategoryTheory.tensorRightHomEquiv_whiskerLeft_comp_evaluation, CategoryTheory.tensorRightHomEquiv_whiskerRight_comp_evaluation, CategoryTheory.rightAdjointMate_comp_evaluation_assoc, evaluation_coevaluation'', CategoryTheory.leftAdjointMate_comp_evaluation, evaluation_coevaluation_assoc, coevaluation_evaluation, CategoryTheory.leftAdjointMate_comp_evaluation_assoc, CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_evaluation, CategoryTheory.leftAdjointMate_comp, CategoryTheory.tensorLeftHomEquiv_whiskerRight_comp_evaluation, coevaluation_evaluation_assoc, CategoryTheory.rightAdjointMate_comp, CategoryTheory.rightAdjointMate_comp_evaluation
evaluation' 📖	CompOp	2 math math: coevaluation_evaluation', evaluation_coevaluation'
termε_ 📖	CompOp	—
termη_ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coevaluation_evaluation 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft coevaluation CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight evaluation CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	coevaluation_evaluation'
coevaluation_evaluation' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft coevaluation' CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight evaluation' CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
coevaluation_evaluation'' 📖	mathematical	—	CategoryTheory.monoidalComp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCoherence.assoc' CategoryTheory.MonoidalCoherence.whiskerRight CategoryTheory.MonoidalCoherence.refl CategoryTheory.MonoidalCategoryStruct.whiskerLeft coevaluation CategoryTheory.MonoidalCategoryStruct.whiskerRight evaluation CategoryTheory.Iso.hom CategoryTheory.MonoidalCoherence.iso CategoryTheory.MonoidalCoherence.right CategoryTheory.MonoidalCoherence.left'	—	CategoryTheory.MonoidalCategory.whiskerRightIso_refl CategoryTheory.Iso.refl_trans coevaluation_evaluation
coevaluation_evaluation_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft coevaluation CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight evaluation CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coevaluation_evaluation
evaluation_coevaluation 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight coevaluation CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft evaluation CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	evaluation_coevaluation'
evaluation_coevaluation' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight coevaluation' CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft evaluation' CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	—
evaluation_coevaluation'' 📖	mathematical	—	CategoryTheory.monoidalComp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCoherence.assoc CategoryTheory.MonoidalCoherence.whiskerRight CategoryTheory.MonoidalCoherence.refl CategoryTheory.MonoidalCategoryStruct.whiskerRight coevaluation CategoryTheory.MonoidalCategoryStruct.whiskerLeft evaluation CategoryTheory.Iso.hom CategoryTheory.MonoidalCoherence.iso CategoryTheory.MonoidalCoherence.left CategoryTheory.MonoidalCoherence.right'	—	CategoryTheory.MonoidalCategory.whiskerRightIso_refl CategoryTheory.Iso.trans_refl CategoryTheory.Iso.refl_trans evaluation_coevaluation
evaluation_coevaluation_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight coevaluation CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft evaluation CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' evaluation_coevaluation

CategoryTheory.HasLeftDual

Definitions

Name	Category	Theorems
exact 📖	CompOp	8 math math: CategoryTheory.coevaluation_comp_leftAdjointMate_assoc, CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft, CategoryTheory.leftAdjointMate_comp_evaluation, CategoryTheory.leftAdjointMate_comp_evaluation_assoc, CategoryTheory.coevaluation_comp_leftAdjointMate, CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_evaluation, CategoryTheory.leftAdjointMate_comp, CategoryTheory.tensorLeftHomEquiv_whiskerRight_comp_evaluation
leftDual 📖	CompOp	17 math math: CategoryTheory.coevaluation_comp_leftAdjointMate_assoc, CategoryTheory.leftDual_rightDual, CategoryTheory.leftDualFunctor_obj, CategoryTheory.leftAdjointMate_id, CategoryTheory.comp_leftAdjointMate_assoc, CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft, CategoryTheory.leftDualFunctor_map, CategoryTheory.leftAdjointMate_comp_evaluation, CategoryTheory.rightDual_leftDual, CategoryTheory.leftAdjointMate_comp_evaluation_assoc, CategoryTheory.coevaluation_comp_leftAdjointMate, CategoryTheory.comp_leftAdjointMate, CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_evaluation, Action.leftDual_v, CategoryTheory.leftAdjointMate_comp, Action.leftDual_ρ, CategoryTheory.tensorLeftHomEquiv_whiskerRight_comp_evaluation

CategoryTheory.HasRightDual

Definitions

Name	Category	Theorems
exact 📖	CompOp	8 math math: CategoryTheory.tensorRightHomEquiv_whiskerLeft_comp_evaluation, CategoryTheory.tensorRightHomEquiv_whiskerRight_comp_evaluation, CategoryTheory.rightAdjointMate_comp_evaluation_assoc, CategoryTheory.coevaluation_comp_rightAdjointMate, CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight, CategoryTheory.rightAdjointMate_comp, CategoryTheory.rightAdjointMate_comp_evaluation, CategoryTheory.coevaluation_comp_rightAdjointMate_assoc
rightDual 📖	CompOp	17 math math: CategoryTheory.leftDual_rightDual, Action.rightDual_ρ, CategoryTheory.tensorRightHomEquiv_whiskerLeft_comp_evaluation, CategoryTheory.tensorRightHomEquiv_whiskerRight_comp_evaluation, CategoryTheory.rightAdjointMate_comp_evaluation_assoc, CategoryTheory.comp_rightAdjointMate, CategoryTheory.comp_rightAdjointMate_assoc, Action.rightDual_v, CategoryTheory.rightDualFunctor_map, CategoryTheory.coevaluation_comp_rightAdjointMate, CategoryTheory.rightDual_leftDual, CategoryTheory.rightAdjointMate_id, CategoryTheory.rightDualFunctor_obj, CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight, CategoryTheory.rightAdjointMate_comp, CategoryTheory.rightAdjointMate_comp_evaluation, CategoryTheory.coevaluation_comp_rightAdjointMate_assoc

CategoryTheory.LeftRigidCategory

Definitions

Name	Category	Theorems
leftDual 📖	CompOp	4 math math: CategoryTheory.leftDualFunctor_obj, CategoryTheory.leftDualFunctor_map, Action.leftDual_v, Action.leftDual_ρ

CategoryTheory.RightRigidCategory

Definitions

Name	Category	Theorems
rightDual 📖	CompOp	4 math math: Action.rightDual_ρ, Action.rightDual_v, CategoryTheory.rightDualFunctor_map, CategoryTheory.rightDualFunctor_obj

CategoryTheory.RigidCategory

Definitions

Name	Category	Theorems
toLeftRigidCategory 📖	CompOp	—
toRightRigidCategory 📖	CompOp	—

---

← Back to Index