Documentation

TauCeti.CategoryTheory.Monoidal.Rigid.Mate

Adjoint mates for explicit exact pairings #

Mathlib's CategoryTheory.rightAdjointMate sends f : X ⟶ Y to fᘁ : Yᘁ ⟶ Xᘁ, where the duals are the ambient HasRightDual choices. Several right duals are not of that form: the tensor product pairing ExactPairing (X ⊗ Y) (Yᘁ ⊗ Xᘁ), the self-pairing of the unit, or a pairing transported along an isomorphism. This file takes the exact pairings as explicit arguments instead: for pX : ExactPairing X X' and pY : ExactPairing Y Y', the mate of f : X ⟶ Y is ExactPairing.rightMate pX pY f : Y' ⟶ X'. This is Mathlib's rightAdjointMate with the given pairings made ambient, and its basic properties are Mathlib's; what the definition adds is the type Y' ⟶ X', so that rewriting sees X' and Y' rather than projections out of HasRightDual records.

A morphism into a right dual is determined by its composite with the evaluation (CategoryTheory.ExactPairing.rightHom_ext), and the mate is characterized by CategoryTheory.ExactPairing.rightMate_comp_evaluation. From these we compute the mates of the monoidal structure morphisms with respect to the tensor product pairings: the mate of a tensor product of morphisms is the reversed tensor product of their mates, and the mates of the associator and the unitors are again an associator and unitors. These are the identities that make the right dual functor C ⥤ (Cᵒᵖ)ᴹᵒᵖ monoidal.

The same is done for left duals: for pX : ExactPairing X' X and pY : ExactPairing Y' Y, the left mate of f : X ⟶ Y is ExactPairing.leftMate pX pY f : Y' ⟶ X', Mathlib's leftAdjointMate with the given pairings made ambient. A morphism into a left dual is determined by its composite with the evaluation (CategoryTheory.ExactPairing.leftDualHom_ext), and the left mates of tensor products and of the structure morphisms are computed in the same way. These are the identities that make the left dual functor C ⥤ (Cᵒᵖ)ᴹᵒᵖ monoidal.

Taking a left adjoint mate and then a right adjoint mate, or conversely, recovers the original morphism.

Main declarations #

References #

source
theorem CategoryTheory.ExactPairing.rightHom_ext {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y A : C} [ExactPairing X Y] {f g : A ⟶ Y} (h : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f X) (ε_ X Y) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight g X) (ε_ X Y)) :
f = g

Two morphisms into a right dual Y of X agree as soon as they agree after evaluation against X.

source
theorem CategoryTheory.ExactPairing.leftHom_ext {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y A : C} [ExactPairing X Y] {f g : X ⟶ A} (h : CategoryStruct.comp (η_ X Y) (MonoidalCategoryStruct.whiskerRight f Y) = CategoryStruct.comp (η_ X Y) (MonoidalCategoryStruct.whiskerRight g Y)) :
f = g

Two morphisms out of the left member X of an exact pairing agree as soon as they agree after the coevaluation of the pairing.

source
def CategoryTheory.ExactPairing.rightMate {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' : C} (pX : ExactPairing X X') (pY : ExactPairing Y Y') (f : X ⟶ Y) :
Y' ⟶ X'

The right adjoint mate Y' ⟶ X' of f : X ⟶ Y, with respect to explicitly given exact pairings (X, X') and (Y, Y'): Mathlib's CategoryTheory.rightAdjointMate with the given pairings made ambient. Stating it with the type Y' ⟶ X' keeps the duals X' and Y' visible to rewriting: as a term @rightAdjointMate C _ _ X Y ⟨X'⟩ ⟨Y'⟩ f, its source and target are the projections HasRightDual.rightDual ⟨Y'⟩ and HasRightDual.rightDual ⟨X'⟩, and Mathlib's lemmas about it do not rewrite against the evaluation ε_ X X' of the given pairing.

Instances For
    source
    theorem CategoryTheory.ExactPairing.rightMate_comp_evaluation {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' : C} (pX : ExactPairing X X') (pY : ExactPairing Y Y') (f : X ⟶ Y) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (pX.rightMate pY f) X) (ε_ X X') = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Y' f) (ε_ Y Y')

    The characteristic property of the right adjoint mate: evaluating it against X is the same as evaluating against Y after applying f.

    source
    theorem CategoryTheory.ExactPairing.rightMate_comp_evaluation_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' : C} (pX : ExactPairing X X') (pY : ExactPairing Y Y') (f : X ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (pX.rightMate pY f) X) (CategoryStruct.comp (ε_ X X') h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Y' f) (CategoryStruct.comp (ε_ Y Y') h)

    The characteristic property of the right adjoint mate: evaluating it against X is the same as evaluating against Y after applying f.

    source
    theorem CategoryTheory.ExactPairing.whiskerRight_rightMate_evaluation {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {W X X' Y Y' : C} (pX : ExactPairing X X') (pY : ExactPairing Y Y') (a : W ⟶ Y') (f : X ⟶ Y) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight a X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (pX.rightMate pY f) X) (ε_ X X')) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft W f) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight a Y) (ε_ Y Y'))

    The characteristic property of the right adjoint mate, after a morphism a : W ⟶ Y' into the dual of the target: evaluating a followed by the mate of f : X ⟶ Y against X is evaluating a against Y after applying f to X. Morphisms into a right dual are compared in this form via CategoryTheory.ExactPairing.rightHom_ext.

    source
    theorem CategoryTheory.ExactPairing.coevaluation_comp_rightMate {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' : C} (pX : ExactPairing X X') (pY : ExactPairing Y Y') (f : X ⟶ Y) :
    CategoryStruct.comp (η_ Y Y') (MonoidalCategoryStruct.whiskerLeft Y (pX.rightMate pY f)) = CategoryStruct.comp (η_ X X') (MonoidalCategoryStruct.whiskerRight f X')

    The dual characterization of the right adjoint mate: applying it after the coevaluation of (Y, Y') is the same as applying f after the coevaluation of (X, X').

    source
    theorem CategoryTheory.ExactPairing.coevaluation_comp_rightMate_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' : C} (pX : ExactPairing X X') (pY : ExactPairing Y Y') (f : X ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorObj Y X' ⟶ Z) :
    CategoryStruct.comp (η_ Y Y') (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Y (pX.rightMate pY f)) h) = CategoryStruct.comp (η_ X X') (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f X') h)

    The dual characterization of the right adjoint mate: applying it after the coevaluation of (Y, Y') is the same as applying f after the coevaluation of (X, X').

    source
    @[simp]
    theorem CategoryTheory.ExactPairing.rightMate_id {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' : C} (p : ExactPairing X X') :
    p.rightMate p (CategoryStruct.id X) = CategoryStruct.id X'

    The mate of an identity is an identity.

    source
    theorem CategoryTheory.ExactPairing.comp_rightMate {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} (pX : ExactPairing X X') (pY : ExactPairing Y Y') (pZ : ExactPairing Z Z') (f : X ⟶ Y) (g : Y ⟶ Z) :
    pX.rightMate pZ (CategoryStruct.comp f g) = CategoryStruct.comp (pY.rightMate pZ g) (pX.rightMate pY f)

    Taking mates reverses composition.

    source
    @[simp]
    theorem CategoryTheory.ExactPairing.rightMate_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} (pX : ExactPairing X X') (pY : ExactPairing Y Y') (pZ : ExactPairing Z Z') (f : X ⟶ Y) :
    tensor.rightMate tensor (MonoidalCategoryStruct.whiskerRight f Z) = MonoidalCategoryStruct.whiskerLeft Z' (pX.rightMate pY f)

    The mate of f ▷ Z with respect to the tensor product pairings is Z' ◁ fᘁ.

    source
    @[simp]
    theorem CategoryTheory.ExactPairing.rightMate_whiskerLeft {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} (pX : ExactPairing X X') (pY : ExactPairing Y Y') (pZ : ExactPairing Z Z') (f : X ⟶ Y) :
    tensor.rightMate tensor (MonoidalCategoryStruct.whiskerLeft Z f) = MonoidalCategoryStruct.whiskerRight (pX.rightMate pY f) Z'

    The mate of Z ◁ f with respect to the tensor product pairings is fᘁ ▷ Z'.

    source
    @[simp]
    theorem CategoryTheory.ExactPairing.rightMate_tensorHom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X₁ X₁' X₂ X₂' Y₁ Y₁' Y₂ Y₂' : C} (pX₁ : ExactPairing X₁ X₁') (pX₂ : ExactPairing X₂ X₂') (pY₁ : ExactPairing Y₁ Y₁') (pY₂ : ExactPairing Y₂ Y₂') (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
    tensor.rightMate tensor (MonoidalCategoryStruct.tensorHom f g) = MonoidalCategoryStruct.tensorHom (pX₂.rightMate pY₂ g) (pX₁.rightMate pY₁ f)

    The mate of a tensor product of morphisms with respect to the tensor product pairings is the tensor product of their mates, in the reverse order.

    source
    @[simp]
    theorem CategoryTheory.ExactPairing.rightMate_associator_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} (pX : ExactPairing X X') (pY : ExactPairing Y Y') (pZ : ExactPairing Z Z') :
    tensor.rightMate tensor (MonoidalCategoryStruct.associator X Y Z).hom = (MonoidalCategoryStruct.associator Z' Y' X').hom

    The mate of the associator of X, Y, Z with respect to the tensor product pairings is the associator of their duals.

    source
    @[simp]
    theorem CategoryTheory.ExactPairing.rightMate_leftUnitor_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' : C} (pX : ExactPairing X X') :
    tensor.rightMate pX (MonoidalCategoryStruct.leftUnitor X).hom = (MonoidalCategoryStruct.rightUnitor X').inv

    The mate of the left unitor of X with respect to the tensor product of the self-pairing of the unit with (X, X') is the inverse right unitor of X'.

    source
    @[simp]
    theorem CategoryTheory.ExactPairing.rightMate_rightUnitor_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' : C} (pX : ExactPairing X X') :
    tensor.rightMate pX (MonoidalCategoryStruct.rightUnitor X).hom = (MonoidalCategoryStruct.leftUnitor X').inv

    The mate of the right unitor of X with respect to the tensor product of (X, X') with the self-pairing of the unit is the inverse left unitor of X'.

    source
    theorem CategoryTheory.ExactPairing.rightDualIso_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y₁ Y₂ : C} (p₁ : ExactPairing X Y₁) (p₂ : ExactPairing X Y₂) :
    (rightDualIso p₁ p₂).hom = p₂.rightMate p₁ (CategoryStruct.id X)

    The comparison rightDualIso p₁ p₂ : Y₁ ≅ Y₂ between two right duals of X is the mate of the identity of X.

    source
    theorem CategoryTheory.ExactPairing.rightDualIso_inv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y₁ Y₂ : C} (p₁ : ExactPairing X Y₁) (p₂ : ExactPairing X Y₂) :
    (rightDualIso p₁ p₂).inv = p₁.rightMate p₂ (CategoryStruct.id X)

    The inverse of the comparison rightDualIso p₁ p₂ : Y₁ ≅ Y₂ is the mate of the identity of X taken in the other direction.

    source
    theorem CategoryTheory.ExactPairing.rightDualIso_hom_whiskerRight_evaluation {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y₁ Y₂ : C} (p₁ : ExactPairing X Y₁) (p₂ : ExactPairing X Y₂) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (rightDualIso p₁ p₂).hom X) (ε_ X Y₂) = ε_ X Y₁

    Through the comparison rightDualIso p₁ p₂ : Y₁ ≅ Y₂, the evaluation of p₂ is the evaluation of p₁.

    source
    theorem CategoryTheory.ExactPairing.rightDualIso_hom_whiskerRight_evaluation_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y₁ Y₂ : C} (p₁ : ExactPairing X Y₁) (p₂ : ExactPairing X Y₂) {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (rightDualIso p₁ p₂).hom X) (CategoryStruct.comp (ε_ X Y₂) h) = CategoryStruct.comp (ε_ X Y₁) h

    Through the comparison rightDualIso p₁ p₂ : Y₁ ≅ Y₂, the evaluation of p₂ is the evaluation of p₁.

    source
    theorem CategoryTheory.ExactPairing.rightDualIso_inv_whiskerRight_evaluation {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y₁ Y₂ : C} (p₁ : ExactPairing X Y₁) (p₂ : ExactPairing X Y₂) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (rightDualIso p₁ p₂).inv X) (ε_ X Y₁) = ε_ X Y₂

    Through the inverse comparison (rightDualIso p₁ p₂).inv : Y₂ ⟶ Y₁, the evaluation of p₁ is the evaluation of p₂.

    source
    theorem CategoryTheory.ExactPairing.rightDualIso_inv_whiskerRight_evaluation_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y₁ Y₂ : C} (p₁ : ExactPairing X Y₁) (p₂ : ExactPairing X Y₂) {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (rightDualIso p₁ p₂).inv X) (CategoryStruct.comp (ε_ X Y₁) h) = CategoryStruct.comp (ε_ X Y₂) h

    Through the inverse comparison (rightDualIso p₁ p₂).inv : Y₂ ⟶ Y₁, the evaluation of p₁ is the evaluation of p₂.

    source
    theorem CategoryTheory.ExactPairing.rightMate_evaluation {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' X'' : C} (pX : ExactPairing X X') (pX' : ExactPairing X' X'') :
    tensor.rightMate exactPairingUnit (ε_ X X') = η_ X' X''

    The mate of the evaluation ε_ X X' : X' ⊗ X ⟶ 𝟙_ C, taken with respect to the tensor product pairing of (X', X'') with (X, X') and the self-pairing of the unit, is the coevaluation η_ X' X'' : 𝟙_ C ⟶ X' ⊗ X''.

    source
    theorem CategoryTheory.ExactPairing.rightMate_coevaluation {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' X'' : C} (pX : ExactPairing X X') (pX' : ExactPairing X' X'') :
    exactPairingUnit.rightMate tensor (η_ X X') = ε_ X' X''

    The mate of the coevaluation η_ X X' : 𝟙_ C ⟶ X ⊗ X', taken with respect to the self-pairing of the unit and the tensor product pairing of (X, X') with (X', X''), is the evaluation ε_ X' X'' : X'' ⊗ X' ⟶ 𝟙_ C.

    Left adjoint mates #

    source
    theorem CategoryTheory.ExactPairing.leftDualHom_ext {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y A : C} [ExactPairing X Y] {f g : A ⟶ X} (h : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Y f) (ε_ X Y) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Y g) (ε_ X Y)) :
    f = g

    Two morphisms into the left member X of an exact pairing (X, Y), that is into a left dual of Y, agree as soon as they agree after evaluation against Y.

    source
    def CategoryTheory.ExactPairing.leftMate {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' : C} (pX : ExactPairing X' X) (pY : ExactPairing Y' Y) (f : X ⟶ Y) :
    Y' ⟶ X'

    The left adjoint mate Y' ⟶ X' of f : X ⟶ Y, with respect to explicitly given exact pairings (X', X) and (Y', Y): Mathlib's CategoryTheory.leftAdjointMate with the given pairings made ambient. As for CategoryTheory.ExactPairing.rightMate, the type Y' ⟶ X' keeps the left duals X' and Y' visible to rewriting.

    Instances For
      source
      theorem CategoryTheory.ExactPairing.leftMate_comp_evaluation {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' : C} (pX : ExactPairing X' X) (pY : ExactPairing Y' Y) (f : X ⟶ Y) :
      CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (pX.leftMate pY f)) (ε_ X' X) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Y') (ε_ Y' Y)

      The characteristic property of the left adjoint mate: evaluating it against X is the same as evaluating against Y after applying f.

      source
      theorem CategoryTheory.ExactPairing.leftMate_comp_evaluation_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' : C} (pX : ExactPairing X' X) (pY : ExactPairing Y' Y) (f : X ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) :
      CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (pX.leftMate pY f)) (CategoryStruct.comp (ε_ X' X) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Y') (CategoryStruct.comp (ε_ Y' Y) h)

      The characteristic property of the left adjoint mate: evaluating it against X is the same as evaluating against Y after applying f.

      source
      theorem CategoryTheory.ExactPairing.coevaluation_comp_leftMate {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' : C} (pX : ExactPairing X' X) (pY : ExactPairing Y' Y) (f : X ⟶ Y) :
      CategoryStruct.comp (η_ Y' Y) (MonoidalCategoryStruct.whiskerRight (pX.leftMate pY f) Y) = CategoryStruct.comp (η_ X' X) (MonoidalCategoryStruct.whiskerLeft X' f)

      The dual characterization of the left adjoint mate: applying it after the coevaluation of (Y', Y) is the same as applying f after the coevaluation of (X', X).

      source
      theorem CategoryTheory.ExactPairing.coevaluation_comp_leftMate_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' : C} (pX : ExactPairing X' X) (pY : ExactPairing Y' Y) (f : X ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorObj X' Y ⟶ Z) :
      CategoryStruct.comp (η_ Y' Y) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (pX.leftMate pY f) Y) h) = CategoryStruct.comp (η_ X' X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X' f) h)

      The dual characterization of the left adjoint mate: applying it after the coevaluation of (Y', Y) is the same as applying f after the coevaluation of (X', X).

      source
      @[simp]
      theorem CategoryTheory.ExactPairing.leftMate_id {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' : C} (p : ExactPairing X' X) :
      p.leftMate p (CategoryStruct.id X) = CategoryStruct.id X'

      The left mate of an identity is an identity.

      source
      theorem CategoryTheory.ExactPairing.comp_leftMate {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} (pX : ExactPairing X' X) (pY : ExactPairing Y' Y) (pZ : ExactPairing Z' Z) (f : X ⟶ Y) (g : Y ⟶ Z) :
      pX.leftMate pZ (CategoryStruct.comp f g) = CategoryStruct.comp (pY.leftMate pZ g) (pX.leftMate pY f)

      Taking left mates reverses composition.

      source
      @[simp]
      theorem CategoryTheory.ExactPairing.leftMate_whiskerLeft {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} (pX : ExactPairing X' X) (pY : ExactPairing Y' Y) (pZ : ExactPairing Z' Z) (f : X ⟶ Y) :
      tensor.leftMate tensor (MonoidalCategoryStruct.whiskerLeft Z f) = MonoidalCategoryStruct.whiskerRight (pX.leftMate pY f) Z'

      The left mate of Z ◁ f with respect to the tensor product pairings is ᘁf ▷ Z'.

      source
      @[simp]
      theorem CategoryTheory.ExactPairing.leftMate_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} (pX : ExactPairing X' X) (pY : ExactPairing Y' Y) (pZ : ExactPairing Z' Z) (f : X ⟶ Y) :
      tensor.leftMate tensor (MonoidalCategoryStruct.whiskerRight f Z) = MonoidalCategoryStruct.whiskerLeft Z' (pX.leftMate pY f)

      The left mate of f ▷ Z with respect to the tensor product pairings is Z' ◁ ᘁf.

      source
      @[simp]
      theorem CategoryTheory.ExactPairing.leftMate_tensorHom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X₁ X₁' X₂ X₂' Y₁ Y₁' Y₂ Y₂' : C} (pX₁ : ExactPairing X₁' X₁) (pX₂ : ExactPairing X₂' X₂) (pY₁ : ExactPairing Y₁' Y₁) (pY₂ : ExactPairing Y₂' Y₂) (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
      tensor.leftMate tensor (MonoidalCategoryStruct.tensorHom f g) = MonoidalCategoryStruct.tensorHom (pX₂.leftMate pY₂ g) (pX₁.leftMate pY₁ f)

      The left mate of a tensor product of morphisms with respect to the tensor product pairings is the tensor product of their left mates, in the reverse order.

      source
      @[simp]
      theorem CategoryTheory.ExactPairing.leftMate_associator_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} (pX : ExactPairing X' X) (pY : ExactPairing Y' Y) (pZ : ExactPairing Z' Z) :
      tensor.leftMate tensor (MonoidalCategoryStruct.associator X Y Z).hom = (MonoidalCategoryStruct.associator Z' Y' X').hom

      The left mate of the associator of X, Y, Z with respect to the tensor product pairings is the associator of their left duals.

      source
      @[simp]
      theorem CategoryTheory.ExactPairing.leftMate_leftUnitor_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' : C} (pX : ExactPairing X' X) :
      tensor.leftMate pX (MonoidalCategoryStruct.leftUnitor X).hom = (MonoidalCategoryStruct.rightUnitor X').inv

      The left mate of the left unitor of X with respect to the tensor product of the self-pairing of the unit with (X', X) is the inverse right unitor of X'.

      source
      @[simp]
      theorem CategoryTheory.ExactPairing.leftMate_rightUnitor_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' : C} (pX : ExactPairing X' X) :
      tensor.leftMate pX (MonoidalCategoryStruct.rightUnitor X).hom = (MonoidalCategoryStruct.leftUnitor X').inv

      The left mate of the right unitor of X with respect to the tensor product of (X', X) with the self-pairing of the unit is the inverse left unitor of X'.

      source
      theorem CategoryTheory.ExactPairing.leftDualIso_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X₁ X₂ Y : C} (p₁ : ExactPairing X₁ Y) (p₂ : ExactPairing X₂ Y) :
      (leftDualIso p₁ p₂).hom = p₂.leftMate p₁ (CategoryStruct.id Y)

      The comparison leftDualIso p₁ p₂ : X₁ ≅ X₂ between two left duals of Y is the left mate of the identity of Y.

      source
      theorem CategoryTheory.ExactPairing.leftDualIso_inv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X₁ X₂ Y : C} (p₁ : ExactPairing X₁ Y) (p₂ : ExactPairing X₂ Y) :
      (leftDualIso p₁ p₂).inv = p₁.leftMate p₂ (CategoryStruct.id Y)

      The inverse of the comparison leftDualIso p₁ p₂ : X₁ ≅ X₂ is the left mate of the identity of Y taken in the other direction.

      source
      theorem CategoryTheory.ExactPairing.leftMate_rightDualIso_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y₁ Y₂ Z : C} (p₁ : ExactPairing X Y₁) (p₂ : ExactPairing X Y₂) (q : ExactPairing Z Y₂) :
      p₁.leftMate q (rightDualIso p₁ p₂).hom = p₂.leftMate q (CategoryStruct.id Y₂)

      If X has two right duals Y₁ and Y₂, then taking the left mate with respect to (X, Y₁) turns the comparison rightDualIso p₁ p₂ : Y₁ ≅ Y₂ into the identity, transported to the pairing (X, Y₂). With q = p₂, the left mate of the comparison is 𝟙 X.

      source
      theorem CategoryTheory.ExactPairing.rightMate_leftDualIso_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X₁ X₂ Y Z : C} (p₁ : ExactPairing X₁ Y) (p₂ : ExactPairing X₂ Y) (q : ExactPairing X₂ Z) :
      p₁.rightMate q (leftDualIso p₁ p₂).hom = p₂.rightMate q (CategoryStruct.id X₂)

      If Y has two left duals X₁ and X₂, then taking the right mate with respect to (X₁, Y) turns the comparison leftDualIso p₁ p₂ : X₁ ≅ X₂ into the identity, transported to the pairing (X₂, Y). With q = p₂, the right mate of the comparison is 𝟙 Y.

      source
      theorem CategoryTheory.ExactPairing.leftMate_rightDualIso_inv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y₁ Y₂ Z : C} (p₁ : ExactPairing X Y₁) (p₂ : ExactPairing X Y₂) (q : ExactPairing Z Y₁) :
      p₂.leftMate q (rightDualIso p₁ p₂).inv = (leftDualIso q p₁).hom

      If X has two right duals Y₁ and Y₂ and Z is a left dual of Y₁, then the left mate of the inverse comparison Y₂ ⟶ Y₁ is the comparison leftDualIso q p₁ : Z ≅ X of the two left duals of Y₁.

      source
      theorem CategoryTheory.ExactPairing.rightMate_leftDualIso_inv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X₁ X₂ Y Z : C} (p₁ : ExactPairing X₁ Y) (p₂ : ExactPairing X₂ Y) (q : ExactPairing X₁ Z) :
      p₂.rightMate q (leftDualIso p₁ p₂).inv = (rightDualIso q p₁).hom

      If Y has two left duals X₁ and X₂ and Z is a right dual of X₁, then the right mate of the inverse comparison X₂ ⟶ X₁ is the comparison rightDualIso q p₁ : Z ≅ Y of the two right duals of X₁.

      source
      @[simp]
      theorem CategoryTheory.leftAdjointMate_rightAdjointMate {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] [HasRightDual Y] (f : X ⟶ Y) :
      (ᘁfᘁ) = f

      Taking the left adjoint mate of a right adjoint mate recovers the original morphism.

      source
      @[simp]
      theorem CategoryTheory.rightAdjointMate_leftAdjointMate {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [HasLeftDual X] [HasLeftDual Y] (f : X ⟶ Y) :
      (ᘁf)ᘁ = f

      Taking the right adjoint mate of a left adjoint mate recovers the original morphism.

      source
      theorem CategoryTheory.rightAdjointMate_injective {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] [HasRightDual Y] :
      Function.Injective rightAdjointMate

      Taking right adjoint mates is injective: the left adjoint mate is a left inverse.

      source
      def CategoryTheory.Iso.rightAdjointMate {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] [HasRightDual Y] (e : X ≅ Y) :
      Yᘁ ≅ Xᘁ

      An isomorphism X ≅ Y induces an isomorphism Yᘁ ≅ Xᘁ of right duals, whose components are the right adjoint mates of those of X ≅ Y.

      Instances For
        source
        @[simp]
        theorem CategoryTheory.Iso.rightAdjointMate_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] [HasRightDual Y] (e : X ≅ Y) :
        e.rightAdjointMate.hom = e.homᘁ

        The component of Iso.rightAdjointMate e is the right adjoint mate of that of e.

        source
        @[simp]
        theorem CategoryTheory.Iso.rightAdjointMate_inv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] [HasRightDual Y] (e : X ≅ Y) :
        e.rightAdjointMate.inv = e.invᘁ

        The inverse of Iso.rightAdjointMate e is the right adjoint mate of the inverse of e.

        source
        theorem TauCeti.rightAdjointMate_eq_rightMate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} [CategoryTheory.HasRightDual X] [CategoryTheory.HasRightDual Y] (f : X ⟶ Y) :
        fᘁ = CategoryTheory.HasRightDual.exact.rightMate CategoryTheory.HasRightDual.exact f

        Mathlib's right adjoint mate is the mate with respect to the ambient right duals.

        source
        theorem TauCeti.leftAdjointMate_eq_leftMate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} [CategoryTheory.HasLeftDual X] [CategoryTheory.HasLeftDual Y] (f : X ⟶ Y) :
        (ᘁf) = CategoryTheory.HasLeftDual.exact.leftMate CategoryTheory.HasLeftDual.exact f

        Mathlib's left adjoint mate is the left mate with respect to the ambient left duals.