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, obtaining a monoidal structure on D.

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

@[simp]
theorem CategoryTheory.Monoidal.transport_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]
@[simp]
theorem CategoryTheory.Monoidal.transport_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.

Instances For

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

    Instances For

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

      Instances For

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

        Instances For

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

          Instances For