Monoidal functors preserve exact pairings #
We show that a monoidal functor F : C тед D sends an
exact pairing (X, Y) in the source to an exact pairing
(F.obj X, F.obj Y) in the target, with evaluation and
coevaluation obtained by conjugating through the
tensorator and unit isomorphisms of F.
This is the forward direction of the standard fact
"monoidal functors preserve dualizability". The reverse
direction (pulling back exact pairings along a faithful
monoidal functor) is Mathlib's
ExactPairing.ofFaithful.
@[instance_reducible]
def
RS.ExactPairing.map
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.Functor C D)
[F.Monoidal]
{X Y : C}
[CategoryTheory.ExactPairing X Y]
:
CategoryTheory.ExactPairing (F.obj X) (F.obj Y)
Monoidal functors preserve exact pairings:
an ExactPairing X Y in C yields an
ExactPairing (F.obj X) (F.obj Y) in D,
with evaluation and coevaluation conjugated
through the tensorator and unit isomorphisms
of F.
Equations
- One or more equations did not get rendered due to their size.