Exact pairings in rigid monoidal categories

This file records evaluation and coevaluation formulas for transported exact pairings and for the adjunction associated to an exact pairing.

Main declarations

• TauCeti.exactPairingCongrLeft_evaluation and TauCeti.exactPairingCongrLeft_coevaluation: transport in the left argument;
• TauCeti.exactPairingCongrRight_evaluation and TauCeti.exactPairingCongrRight_coevaluation: transport in the right argument;
• TauCeti.exactPairingCongr_evaluation and TauCeti.exactPairingCongr_coevaluation: simultaneous transport in both arguments;
• TauCeti.tensorLeftAdjunction_unit_app and TauCeti.tensorLeftAdjunction_counit_app: the unit and counit of the adjunction associated to an exact pairing.

theorem TauCeti.exactPairingCongrLeft_evaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X X' Y : C} [CategoryTheory.ExactPairing X' Y] (i : X ≅ X') : ε_ X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y i.hom) (ε_ X' Y)

The evaluation of an exact pairing transported across an isomorphism in its left argument.

This is not a simp lemma: CategoryTheory.exactPairingCongrLeft is how a transported pairing is built, so rewriting with it would unfold the evaluation of every such pairing and rob the transported instance of its own normal form.

theorem TauCeti.exactPairingCongrLeft_evaluation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X X' Y : C} [CategoryTheory.ExactPairing X' Y] (i : X ≅ X') {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp (ε_ X Y) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y i.hom) (CategoryTheory.CategoryStruct.comp (ε_ X' Y) h)

The evaluation of an exact pairing transported across an isomorphism in its left argument.

This is not a simp lemma: CategoryTheory.exactPairingCongrLeft is how a transported pairing is built, so rewriting with it would unfold the evaluation of every such pairing and rob the transported instance of its own normal form.

theorem TauCeti.exactPairingCongrLeft_coevaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X X' Y : C} [CategoryTheory.ExactPairing X' Y] (i : X ≅ X') : η_ X Y = CategoryTheory.CategoryStruct.comp (η_ X' Y) (CategoryTheory.MonoidalCategoryStruct.whiskerRight i.inv Y)

The coevaluation of an exact pairing transported across an isomorphism in its left argument. Not a simp lemma, for the reason given on TauCeti.exactPairingCongrLeft_evaluation.

theorem TauCeti.exactPairingCongrLeft_coevaluation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X X' Y : C} [CategoryTheory.ExactPairing X' Y] (i : X ≅ X') {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (η_ X Y) h = CategoryTheory.CategoryStruct.comp (η_ X' Y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight i.inv Y) h)

The coevaluation of an exact pairing transported across an isomorphism in its left argument. Not a simp lemma, for the reason given on TauCeti.exactPairingCongrLeft_evaluation.

theorem TauCeti.exactPairingCongrRight_evaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y Y' : C} [CategoryTheory.ExactPairing X Y'] (j : Y ≅ Y') : ε_ X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight j.hom X) (ε_ X Y')

The evaluation of an exact pairing transported across an isomorphism in its right argument.

theorem TauCeti.exactPairingCongrRight_evaluation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y Y' : C} [CategoryTheory.ExactPairing X Y'] (j : Y ≅ Y') {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp (ε_ X Y) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight j.hom X) (CategoryTheory.CategoryStruct.comp (ε_ X Y') h)

The evaluation of an exact pairing transported across an isomorphism in its right argument.

theorem TauCeti.exactPairingCongrRight_coevaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y Y' : C} [CategoryTheory.ExactPairing X Y'] (j : Y ≅ Y') : η_ X Y = CategoryTheory.CategoryStruct.comp (η_ X Y') (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X j.inv)

The coevaluation of an exact pairing transported across an isomorphism in its right argument.

theorem TauCeti.exactPairingCongrRight_coevaluation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y Y' : C} [CategoryTheory.ExactPairing X Y'] (j : Y ≅ Y') {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (η_ X Y) h = CategoryTheory.CategoryStruct.comp (η_ X Y') (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X j.inv) h)

The coevaluation of an exact pairing transported across an isomorphism in its right argument.

theorem TauCeti.exactPairingCongr_evaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X X' Y Y' : C} [CategoryTheory.ExactPairing X' Y'] (i : X ≅ X') (j : Y ≅ Y') : ε_ X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y i.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight j.hom X') (ε_ X' Y'))

The evaluation of an exact pairing transported across isomorphisms in both arguments.

theorem TauCeti.exactPairingCongr_evaluation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X X' Y Y' : C} [CategoryTheory.ExactPairing X' Y'] (i : X ≅ X') (j : Y ≅ Y') {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp (ε_ X Y) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y i.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight j.hom X') (CategoryTheory.CategoryStruct.comp (ε_ X' Y') h))

The evaluation of an exact pairing transported across isomorphisms in both arguments.

theorem TauCeti.exactPairingCongr_coevaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X X' Y Y' : C} [CategoryTheory.ExactPairing X' Y'] (i : X ≅ X') (j : Y ≅ Y') : η_ X Y = CategoryTheory.CategoryStruct.comp (η_ X' Y') (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' j.inv) (CategoryTheory.MonoidalCategoryStruct.whiskerRight i.inv Y))

The coevaluation of an exact pairing transported across isomorphisms in both arguments.

theorem TauCeti.exactPairingCongr_coevaluation_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X X' Y Y' : C} [CategoryTheory.ExactPairing X' Y'] (i : X ≅ X') (j : Y ≅ Y') {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (η_ X Y) h = CategoryTheory.CategoryStruct.comp (η_ X' Y') (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' j.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight i.inv Y) h))

The coevaluation of an exact pairing transported across isomorphisms in both arguments.

theorem TauCeti.tensorLeftAdjunction_unit_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] (Z : C) : (CategoryTheory.tensorLeftAdjunction D Y).unit.app Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (η_ D Y) Z) (CategoryTheory.MonoidalCategoryStruct.associator D Y Z).hom)

The unit of the adjunction tensorLeft Y ⊣ tensorLeft D attached to an exact pairing ExactPairing D Y inserts the coevaluation.

theorem TauCeti.tensorLeftAdjunction_counit_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (D Y : C) [CategoryTheory.ExactPairing D Y] (Z : C) : (CategoryTheory.tensorLeftAdjunction D Y).counit.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)

The counit of the adjunction tensorLeft Y ⊣ tensorLeft D attached to an exact pairing ExactPairing D Y contracts the evaluation.