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.

source

@[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))))

source

@[simp]

theorem CategoryTheory.Monoidal.transport_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : D) :

CategoryTheory.MonoidalCategory.leftUnitor X = e.functor.mapIso (((e.unitIso.app (CategoryTheory.MonoidalCategory.tensorUnit C)).symm ⊗ CategoryTheory.Iso.refl (e.inverse.obj X)) ≪≫ CategoryTheory.MonoidalCategory.leftUnitor (e.inverse.obj X)) ≪≫ e.counitIso.app X

source

@[simp]

theorem CategoryTheory.Monoidal.transport_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : D) :

CategoryTheory.MonoidalCategory.rightUnitor X = e.functor.mapIso ((CategoryTheory.Iso.refl (e.inverse.obj X) ⊗ (e.unitIso.app (CategoryTheory.MonoidalCategory.tensorUnit C)).symm) ≪≫ CategoryTheory.MonoidalCategory.rightUnitor (e.inverse.obj X)) ≪≫ e.counitIso.app X

source

@[simp]

theorem CategoryTheory.Monoidal.transport_tensorUnit' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

CategoryTheory.MonoidalCategory.tensorUnit' = e.functor.obj (CategoryTheory.MonoidalCategory.tensorUnit C)

source

@[simp]

theorem CategoryTheory.Monoidal.transport_tensorObj {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) :

CategoryTheory.MonoidalCategory.tensorObj X Y = e.functor.obj (CategoryTheory.MonoidalCategory.tensorObj (e.inverse.obj X) (e.inverse.obj Y))

source

@[simp]

theorem CategoryTheory.Monoidal.transport_whiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : D) :

∀ (x x_1 : D) (f : x ⟶ x_1), CategoryTheory.MonoidalCategory.whiskerLeft X f = e.functor.map (CategoryTheory.MonoidalCategory.whiskerLeft (e.inverse.obj X) (e.inverse.map f))

source

@[simp]

theorem CategoryTheory.Monoidal.transport_whiskerRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (X : D), CategoryTheory.MonoidalCategory.whiskerRight f X = e.functor.map (CategoryTheory.MonoidalCategory.whiskerRight (e.inverse.map f) (e.inverse.obj X))

source

@[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))

source

def CategoryTheory.Monoidal.transport {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

CategoryTheory.MonoidalCategory D

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

Instances For

source

def CategoryTheory.Monoidal.Transported {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] :

(C ≌ D) → Type u₂

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

Instances For

source

instance CategoryTheory.Monoidal.instCategoryTransported {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

CategoryTheory.Category.{v₂, u₂} (CategoryTheory.Monoidal.Transported e)

source

instance CategoryTheory.Monoidal.instMonoidalCategoryTransportedInstCategoryTransported {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

CategoryTheory.MonoidalCategory (CategoryTheory.Monoidal.Transported e)

source

instance CategoryTheory.Monoidal.instInhabitedTransported {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

Inhabited (CategoryTheory.Monoidal.Transported e)

source

@[simp]

theorem CategoryTheory.Monoidal.laxToTransported_toFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

(CategoryTheory.Monoidal.laxToTransported e).toFunctor = e.functor

source

@[simp]

theorem CategoryTheory.Monoidal.laxToTransported_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

(CategoryTheory.Monoidal.laxToTransported e).ε = CategoryTheory.CategoryStruct.id (e.functor.obj (CategoryTheory.MonoidalCategory.tensorUnit C))

source

@[simp]

theorem CategoryTheory.Monoidal.laxToTransported_μ {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.LaxMonoidalFunctor.μ (CategoryTheory.Monoidal.laxToTransported e) X Y = e.functor.map (CategoryTheory.MonoidalCategory.tensorHom (e.unitInv.app X) (e.unitInv.app Y))

source

def CategoryTheory.Monoidal.laxToTransported {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

CategoryTheory.LaxMonoidalFunctor C (CategoryTheory.Monoidal.Transported e)

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

Instances For

source

@[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) :

(CategoryTheory.Monoidal.toTransported e).toLaxMonoidalFunctor = CategoryTheory.Monoidal.laxToTransported e

source

def CategoryTheory.Monoidal.toTransported {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

CategoryTheory.MonoidalFunctor C (CategoryTheory.Monoidal.Transported e)

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

Instances For

source

instance CategoryTheory.Monoidal.instIsEquivalenceTransportedInstCategoryTransportedToFunctorInstMonoidalCategoryTransportedInstCategoryTransportedToLaxMonoidalFunctorToTransported {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

CategoryTheory.IsEquivalence (CategoryTheory.Monoidal.toTransported e).toLaxMonoidalFunctor.toFunctor

source

@[simp]

theorem CategoryTheory.Monoidal.fromTransported_toLaxMonoidalFunctor_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : CategoryTheory.Monoidal.Transported e) (Y : CategoryTheory.Monoidal.Transported e) :

source

@[simp]

theorem CategoryTheory.Monoidal.fromTransported_toLaxMonoidalFunctor_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

(CategoryTheory.Monoidal.fromTransported e).toLaxMonoidalFunctor.ε = (CategoryTheory.Functor.asEquivalence e.functor).unit.app (CategoryTheory.MonoidalCategory.tensorUnit C)

source

@[simp]

theorem CategoryTheory.Monoidal.fromTransported_toLaxMonoidalFunctor_toFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

(CategoryTheory.Monoidal.fromTransported e).toLaxMonoidalFunctor.toFunctor = e.inverse

source

def CategoryTheory.Monoidal.fromTransported {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

CategoryTheory.MonoidalFunctor (CategoryTheory.Monoidal.Transported e) C

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

Instances For

source

instance CategoryTheory.Monoidal.instIsEquivalence_fromTransported {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

CategoryTheory.IsEquivalence (CategoryTheory.Monoidal.fromTransported e).toLaxMonoidalFunctor.toFunctor

source

@[simp]

theorem CategoryTheory.Monoidal.transportedMonoidalUnitIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

(CategoryTheory.Monoidal.transportedMonoidalUnitIso e).hom = CategoryTheory.monoidalUnit (CategoryTheory.Monoidal.toTransported e)

source

@[simp]

theorem CategoryTheory.Monoidal.transportedMonoidalUnitIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

(CategoryTheory.Monoidal.transportedMonoidalUnitIso e).inv = CategoryTheory.inv (CategoryTheory.monoidalUnit (CategoryTheory.Monoidal.toTransported e))

source

def CategoryTheory.Monoidal.transportedMonoidalUnitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

CategoryTheory.LaxMonoidalFunctor.id C ≅ CategoryTheory.Monoidal.laxToTransported e ⊗⋙ (CategoryTheory.Monoidal.fromTransported e).toLaxMonoidalFunctor

The unit isomorphism upgrades to a monoidal isomorphism.

Instances For

source

@[simp]

theorem CategoryTheory.Monoidal.transportedMonoidalCounitIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

(CategoryTheory.Monoidal.transportedMonoidalCounitIso e).hom = CategoryTheory.monoidalCounit (CategoryTheory.Monoidal.toTransported e)

source

@[simp]

theorem CategoryTheory.Monoidal.transportedMonoidalCounitIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

(CategoryTheory.Monoidal.transportedMonoidalCounitIso e).inv = CategoryTheory.inv (CategoryTheory.monoidalCounit (CategoryTheory.Monoidal.toTransported e))

source

def CategoryTheory.Monoidal.transportedMonoidalCounitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

(CategoryTheory.Monoidal.fromTransported e).toLaxMonoidalFunctor ⊗⋙ CategoryTheory.Monoidal.laxToTransported e ≅ CategoryTheory.LaxMonoidalFunctor.id (CategoryTheory.Monoidal.Transported e)

The counit isomorphism upgrades to a monoidal isomorphism.

Instances For