Duality-intertwining morphisms are invertible

The per-object kernel of Deligne 3.2: a morphism compatible with exact pairings on both sides is an isomorphism, with inverse the mate of its partner. A monoidal natural transformation between fibre functors supplies exactly this data at every object.

noncomputable def RS.dualityMate {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {X X' Y Y' : D} [CategoryTheory.ExactPairing X X'] [CategoryTheory.ExactPairing Y Y'] (f' : X' ⟶ Y') : Y ⟶ X

The mate of the partner: the candidate inverse.

Equations

• One or more equations did not get rendered due to their size.