Documentation

Mathlib.CategoryTheory.Monoidal.Transport

Transport a monoidal structure along an equivalence. #

When C and D are equivalent as categories, we can transport a monoidal structure on C along the equivalence as CategoryTheory.Monoidal.transport, obtaining a monoidal structure on D.

More generally, we can transport the lawfulness of a monoidal structure along a suitable faithful functor, as CategoryTheory.Monoidal.induced. The comparison is analogous to the difference between Equiv.monoid and Function.Injective.monoid.

We then upgrade the original functor and its inverse to monoidal functors with respect to the new monoidal structure on D.

The data needed to induce a MonoidalCategory via the functor F; namely, pre-existing definitions of , 𝟙_, , that are preserved by F.

Instances For

    Induce the lawfulness of the monoidal structure along an faithful functor of (plain) categories, where the operations are already defined on the destination type D.

    The functor F must preserve all the data parts of the monoidal structure between the two categories.

    Equations
    Instances For

      A faithful functor equipped with a InducingFunctorData structure is monoidal.

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

        Transport a monoidal structure along an equivalence of (plain) categories.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem CategoryTheory.Monoidal.transportStruct_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (X : D) (Y : D) (Z : D) :
          CategoryTheory.MonoidalCategory.associator X Y Z = e.functor.mapIso (CategoryTheory.MonoidalCategory.whiskerRightIso (e.unitIso.app (CategoryTheory.MonoidalCategory.tensorObj (e.inverse.obj X) (e.inverse.obj Y))).symm (e.inverse.obj Z) ≪≫ CategoryTheory.MonoidalCategory.associator (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso (e.inverse.obj X) (e.unitIso.app (CategoryTheory.MonoidalCategory.tensorObj (e.inverse.obj Y) (e.inverse.obj Z))))
          theorem CategoryTheory.Monoidal.transportStruct_tensorHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) :
          ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ Y₁) (g : X₂ Y₂), CategoryTheory.MonoidalCategory.tensorHom f g = e.functor.map (CategoryTheory.MonoidalCategory.tensorHom (e.inverse.map f) (e.inverse.map g))

          Transport a monoidal structure along an equivalence of (plain) categories.

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

            A type synonym for D, which will carry the transported monoidal structure.

            Equations
            Instances For
              @[reducible, inline]

              We upgrade the equivalence of categories e : C ≌ D to a monoidal category equivalence C ≌ Transported e.

              Equations
              Instances For