Documentation

Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

Transport rigid structures over a monoidal equivalence. #

Given candidate data for an exact pairing, which is sent by a faithful monoidal functor to an exact pairing, the equations holds automatically.

Equations
Instances For

    Given a pair of objects which are sent by a fully faithful functor to a pair of objects with an exact pairing, we get an exact pairing.

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

      Pull back a rigid structure along an equivalence.

      Equations
      Instances For