Documentation

TauCeti.CategoryTheory.Monoidal.Rigid.Closed

The internal hom out of a dualizable object #

Let C be a monoidal category in which an object Y is closed, so that (Y ⟶[C] -) is right adjoint to Y ⊗ -. If Y also admits a left dual, that is, if ExactPairing D Y holds for some object D, then D ⊗ - is a second right adjoint of Y ⊗ -, and the two agree:

(Y ⟶[C] Z) ≅ D ⊗ Z,      in particular      (Y ⟶[C] 𝟙_ C) ≅ D.

So the internal hom into the unit computes the left dual, and the internal hom out of Y is tensoring with that dual. The comparison is characterized by the evaluation of the internal hom: under it, the evaluation becomes the composite Y ⊗ (D ⊗ Z) ⟶ (Y ⊗ D) ⊗ Z ⟶ 𝟙_ C ⊗ Z ⟶ Z built from the pairing ε_ D Y, and over the unit the evaluation becomes the pairing itself.

The dual D is an explicit argument rather than CategoryTheory.HasLeftDual, so that a caller with a preferred model of the dual — for instance a finite free sheaf of modules, which is its own dual — gets the comparison with that model. Taking D = ᘁY gives (Y ⟶[C] 𝟙_ C) ≅ ᘁY.

Mathlib builds the two adjunctions separately, as CategoryTheory.ihom.adjunction for the closed structure and CategoryTheory.tensorLeftAdjunction for the pairing; the comparison here is their uniqueness isomorphism CategoryTheory.Adjunction.rightAdjointUniq.

Main declarations #

source
def TauCeti.ihomIsoTensorLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] :
CategoryTheory.ihom Y ≅ CategoryTheory.MonoidalCategory.tensorLeft D

The internal hom out of Y is left tensoring by a left dual D of Y: both functors are right adjoint to Y ⊗ -.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.whiskerLeft_ihomIsoTensorLeft_inv_app_comp_ev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D Y : C} [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] (Z : C) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y ((ihomIsoTensorLeft D Y).inv.app Z)) ((CategoryTheory.ihom.ev Y).app Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y D Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ D Y) Z) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom)

    Under the comparison D ⊗ Z ⟶ (Y ⟶[C] Z), the evaluation of the internal hom becomes the evaluation of the pairing.

    source
    @[simp]
    theorem TauCeti.whiskerLeft_ihomIsoTensorLeft_inv_app_comp_ev_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D Y : C} [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] (Z : C) {Z✝ : C} (h : Z ⟶ Z✝) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y ((ihomIsoTensorLeft D Y).inv.app Z)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev Y).app Z) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y D Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ D Y) Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom h))

    Under the comparison D ⊗ Z ⟶ (Y ⟶[C] Z), the evaluation of the internal hom becomes the evaluation of the pairing.

    source
    theorem TauCeti.whiskerLeft_ihomIsoTensorLeft_hom_app_comp_evaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D Y : C} [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] (Z : C) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y ((ihomIsoTensorLeft D Y).hom.app Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y D Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ D Y) Z) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom)) = (CategoryTheory.ihom.ev Y).app Z

    Under the comparison (Y ⟶[C] Z) ⟶ D ⊗ Z, the evaluation of the pairing becomes the evaluation of the internal hom.

    source
    theorem TauCeti.whiskerLeft_ihomIsoTensorLeft_hom_app_comp_evaluation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D Y : C} [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] (Z : C) {Z✝ : C} (h : Z ⟶ Z✝) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y ((ihomIsoTensorLeft D Y).hom.app Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y D Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ D Y) Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom h))) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev Y).app Z) h

    Under the comparison (Y ⟶[C] Z) ⟶ D ⊗ Z, the evaluation of the pairing becomes the evaluation of the internal hom.

    source
    theorem TauCeti.ihomIsoTensorLeft_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D Y : C} [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] (Z : C) :
    (ihomIsoTensorLeft D Y).hom.app Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor ((CategoryTheory.ihom Y).obj Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (η_ D Y) ((CategoryTheory.ihom Y).obj Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator D Y ((CategoryTheory.ihom Y).obj Z)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft D ((CategoryTheory.ihom.ev Y).app Z))))

    The comparison (Y ⟶[C] Z) ⟶ D ⊗ Z inserts the coevaluation and then evaluates.

    source
    theorem TauCeti.ihomIsoTensorLeft_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D Y : C} [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] (Z : C) :
    (ihomIsoTensorLeft D Y).inv.app Z = CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y D Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ D Y) Z) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom))

    The comparison D ⊗ Z ⟶ (Y ⟶[C] Z) is the transpose of the evaluation of the pairing.

    source
    theorem TauCeti.ihomIsoTensorLeft_hom_app_comp_whiskerRight_leftAdjointMate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {Y Y' : C} [CategoryTheory.HasLeftDual Y] [CategoryTheory.HasLeftDual Y'] [CategoryTheory.Closed Y] [CategoryTheory.Closed Y'] (f : Y ⟶ Y') (Z : C) :
    CategoryTheory.CategoryStruct.comp ((ihomIsoTensorLeft (ᘁY') Y').hom.app Z) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ᘁf) Z) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre f).app Z) ((ihomIsoTensorLeft (ᘁY) Y).hom.app Z)

    The comparison is natural in the source: precomposing the internal hom with f : Y ⟶ Y' corresponds to tensoring with the left adjoint mate ᘁf.

    source
    def TauCeti.ihomUnitIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] :
    (CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ D

    The internal hom of Y into the unit is a left dual of Y.

    Equations
    Instances For
      source
      theorem TauCeti.ihomUnitIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] :
      (ihomUnitIso D Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (η_ D Y) ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator D Y ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft D ((CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) (CategoryTheory.MonoidalCategoryStruct.rightUnitor D).hom)))

      The comparison (Y ⟶[C] 𝟙_ C) ⟶ D inserts the coevaluation and then evaluates.

      source
      @[simp]
      theorem TauCeti.whiskerLeft_ihomUnitIso_inv_comp_ev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (ihomUnitIso D Y).inv) ((CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) = ε_ D Y

      Under the comparison D ⟶ (Y ⟶[C] 𝟙_ C), the evaluation of the internal hom becomes the evaluation of the pairing.

      source
      @[simp]
      theorem TauCeti.whiskerLeft_ihomUnitIso_inv_comp_ev_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (ihomUnitIso D Y).inv) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h) = CategoryTheory.CategoryStruct.comp (ε_ D Y) h

      Under the comparison D ⟶ (Y ⟶[C] 𝟙_ C), the evaluation of the internal hom becomes the evaluation of the pairing.

      source
      theorem TauCeti.ihomUnitIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] :
      (ihomUnitIso D Y).inv = CategoryTheory.MonoidalClosed.curry (ε_ D Y)

      The comparison D ⟶ (Y ⟶[C] 𝟙_ C) is the transpose of the evaluation of the pairing.

      source
      theorem TauCeti.tensorHom_ihomUnitIso_inv_comp_ev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] {M N : C} (f : M ⟶ Y) (g : N ⟶ D) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.comp g (ihomUnitIso D Y).inv)) ((CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (ε_ D Y)

      Pairing against the comparison D ⟶ (Y ⟶[C] 𝟙_ C) is pairing against the dual.

      source
      theorem TauCeti.tensorHom_ihomUnitIso_inv_comp_ev_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] {M N : C} (f : M ⟶ Y) (g : N ⟶ D) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.comp g (ihomUnitIso D Y).inv)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (CategoryTheory.CategoryStruct.comp (ε_ D Y) h)

      Pairing against the comparison D ⟶ (Y ⟶[C] 𝟙_ C) is pairing against the dual.

      source
      @[reducible]
      def TauCeti.exactPairingIhomUnit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] :
      CategoryTheory.ExactPairing ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y

      Transporting the pairing along TauCeti.ihomUnitIso exhibits the internal hom of Y into the unit as a left dual of Y: the categorical dual of Y is Hom(Y, 𝟙_ C).

      This is deliberately not an instance because the chosen dual D is not determined by the resulting ExactPairing type.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.exactPairingIhomUnit_evaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] :
        ε_ ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y = (CategoryTheory.ihom.ev Y).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

        The evaluation of the pairing transported to the internal hom is the internal-hom evaluation.

        source
        @[simp]
        theorem TauCeti.exactPairingIhomUnit_coevaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] [CategoryTheory.Closed Y] :
        η_ ((CategoryTheory.ihom Y).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Y = CategoryTheory.CategoryStruct.comp (η_ D Y) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ihomUnitIso D Y).inv Y)

        The coevaluation of the pairing transported to the internal hom is obtained by composing the original coevaluation with the inverse comparison.