Theorems · Definition · category theory

CategoryTheory.HasLeftDual.leftDual

{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} → (Y : C) → [self : CategoryTheory.HasLeftDual Y] → C

The left dual of the object X.

Defined in: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Cited by: 17 results in Mathlib
Foundations: Depth 3 from the axioms · uses no axioms
Assumes: CategoryTheory.HasLeftDual

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.MonoidalCategorystatement and proof · cited by 3,095
CategoryTheory.HasLeftDualstatement and proof · cited by 12

Cited by24

Results whose statement or proof uses this declaration.

CategoryTheory.leftAdjointMatestatement and proof · cited by 13
CategoryTheory.leftDualFunctorproof · cited by 2
CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_evaluationstatement and proof · cited by 1
CategoryTheory.tensorLeftHomEquiv_whiskerRight_comp_evaluationstatement and proof · cited by 1
CategoryTheory.leftAdjointMate_compstatement and proof · cited by 1
CategoryTheory.leftAdjointMate_comp_evaluationstatement and proof · cited by 1
CategoryTheory.leftAdjointMate_idstatement and proof · cited by 1
CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeftstatement and proof · cited by 1
CategoryTheory.coevaluation_comp_leftAdjointMatestatement and proof · cited by 1
CategoryTheory.comp_leftAdjointMatestatement and proof · cited by 1
CategoryTheory.leftAdjointMate_comp_evaluation_assocstatement and proof · cited by 0
CategoryTheory.hasLeftDualOfEquivalenceproof · cited by 0