# 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₁} [] {D : Type u₂} [] (e : C D) (X : D) (Y : D) (Z : D) :
= 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.transport_leftUnitor {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : D) :
= e.functor.mapIso (((e.unitIso.app ()).symm CategoryTheory.Iso.refl (e.inverse.obj X)) ≪≫ CategoryTheory.MonoidalCategory.leftUnitor (e.inverse.obj X)) ≪≫ e.counitIso.app X
@[simp]
theorem CategoryTheory.Monoidal.transport_rightUnitor {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : D) :
= e.functor.mapIso ((CategoryTheory.Iso.refl (e.inverse.obj X) (e.unitIso.app ()).symm) ≪≫ CategoryTheory.MonoidalCategory.rightUnitor (e.inverse.obj X)) ≪≫ e.counitIso.app X
@[simp]
theorem CategoryTheory.Monoidal.transport_tensorUnit' {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
CategoryTheory.MonoidalCategory.tensorUnit' = e.functor.obj ()
@[simp]
theorem CategoryTheory.Monoidal.transport_tensorObj {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : D) (Y : D) :
= e.functor.obj (CategoryTheory.MonoidalCategory.tensorObj (e.inverse.obj X) (e.inverse.obj Y))
@[simp]
theorem CategoryTheory.Monoidal.transport_whiskerLeft {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : D) :
∀ (x x_1 : D) (f : x x_1), = e.functor.map (CategoryTheory.MonoidalCategory.whiskerLeft (e.inverse.obj X) (e.inverse.map f))
@[simp]
theorem CategoryTheory.Monoidal.transport_whiskerRight {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
∀ {X₁ X₂ : D} (f : X₁ X₂) (X : D), = e.functor.map (CategoryTheory.MonoidalCategory.whiskerRight (e.inverse.map f) (e.inverse.obj X))
@[simp]
theorem CategoryTheory.Monoidal.transport_tensorHom {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ Y₁) (g : X₂ Y₂), = e.functor.map (CategoryTheory.MonoidalCategory.tensorHom (e.inverse.map f) (e.inverse.map g))
def CategoryTheory.Monoidal.transport {C : Type u₁} [] {D : Type u₂} [] (e : C D) :

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

Instances For
def CategoryTheory.Monoidal.Transported {C : Type u₁} [] {D : Type u₂} [] :
(C D) → Type u₂

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

Instances For
instance CategoryTheory.Monoidal.instCategoryTransported {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
instance CategoryTheory.Monoidal.instInhabitedTransported {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
@[simp]
theorem CategoryTheory.Monoidal.laxToTransported_toFunctor {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
().toFunctor = e.functor
@[simp]
theorem CategoryTheory.Monoidal.laxToTransported_ε {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
@[simp]
theorem CategoryTheory.Monoidal.laxToTransported_μ {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : C) (Y : C) :
= e.functor.map (CategoryTheory.MonoidalCategory.tensorHom (e.unitInv.app X) (e.unitInv.app Y))
def CategoryTheory.Monoidal.laxToTransported {C : Type u₁} [] {D : Type u₂} [] (e : C D) :

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

Instances For
@[simp]
theorem CategoryTheory.Monoidal.toTransported_toLaxMonoidalFunctor {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
().toLaxMonoidalFunctor =
def CategoryTheory.Monoidal.toTransported {C : Type u₁} [] {D : Type u₂} [] (e : C D) :

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

Instances For
@[simp]
theorem CategoryTheory.Monoidal.fromTransported_toLaxMonoidalFunctor_μ {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
CategoryTheory.LaxMonoidalFunctor.μ ().toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.asEquivalence e.functor).unit.app (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.asEquivalence e.functor).inverse.obj X) ((CategoryTheory.Functor.asEquivalence e.functor).inverse.obj Y))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv ((CategoryTheory.Functor.asEquivalence e.functor).inverse.map (e.functor.map (CategoryTheory.MonoidalCategory.tensorHom (e.unitInv.app ((CategoryTheory.Functor.asEquivalence e.functor).inverse.obj X)) (e.unitInv.app ((CategoryTheory.Functor.asEquivalence e.functor).inverse.obj Y)))))) ((CategoryTheory.Functor.asEquivalence e.functor).inverse.map (e.functor.map (CategoryTheory.MonoidalCategory.tensorHom (e.inverse.map ((CategoryTheory.Functor.asEquivalence e.functor).counit.app X)) (e.inverse.map ((CategoryTheory.Functor.asEquivalence e.functor).counit.app Y))))))
@[simp]
theorem CategoryTheory.Monoidal.fromTransported_toLaxMonoidalFunctor_ε {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
().toLaxMonoidalFunctor = (CategoryTheory.Functor.asEquivalence e.functor).unit.app ()
@[simp]
theorem CategoryTheory.Monoidal.fromTransported_toLaxMonoidalFunctor_toFunctor {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
().toLaxMonoidalFunctor.toFunctor = e.inverse
def CategoryTheory.Monoidal.fromTransported {C : Type u₁} [] {D : Type u₂} [] (e : C D) :

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

Instances For
instance CategoryTheory.Monoidal.instIsEquivalence_fromTransported {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
CategoryTheory.IsEquivalence ().toLaxMonoidalFunctor.toFunctor
@[simp]
theorem CategoryTheory.Monoidal.transportedMonoidalUnitIso_hom {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
@[simp]
theorem CategoryTheory.Monoidal.transportedMonoidalUnitIso_inv {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
def CategoryTheory.Monoidal.transportedMonoidalUnitIso {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
⊗⋙ ().toLaxMonoidalFunctor

The unit isomorphism upgrades to a monoidal isomorphism.

Instances For
@[simp]
theorem CategoryTheory.Monoidal.transportedMonoidalCounitIso_hom {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
@[simp]
theorem CategoryTheory.Monoidal.transportedMonoidalCounitIso_inv {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
def CategoryTheory.Monoidal.transportedMonoidalCounitIso {C : Type u₁} [] {D : Type u₂} [] (e : C D) :

The counit isomorphism upgrades to a monoidal isomorphism.

Instances For