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
    @[reducible, inline]

    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

      We can upgrade F to a monoidal functor from D to E with the induced structure.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        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 (((e.unitIso.app (CategoryTheory.MonoidalCategory.tensorObj (e.inverse.obj X) (e.inverse.obj Y))).symm CategoryTheory.Iso.refl (e.inverse.obj Z)) ≪≫ CategoryTheory.MonoidalCategory.associator (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫ (CategoryTheory.Iso.refl (e.inverse.obj X) e.unitIso.app (CategoryTheory.MonoidalCategory.tensorObj (e.inverse.obj Y) (e.inverse.obj Z))))
        @[simp]
        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

          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

              We can upgrade e.inverse to a monoidal functor from D with the transported structure to C.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.Monoidal.toTransported_toLaxMonoidalFunctor_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C D) (X : C) (Y : C) :
                (CategoryTheory.Monoidal.toTransported e) X Y = CategoryTheory.CategoryStruct.comp (e.symm.unit.app (e.functor.obj (CategoryTheory.MonoidalCategory.tensorObj (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y))))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (e.functor.map (e.unitIso.hom.app (CategoryTheory.MonoidalCategory.tensorObj (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y)))))) (e.functor.map (CategoryTheory.MonoidalCategory.tensorHom (e.symm.counit.app X) (e.symm.counit.app Y))))