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.

structure CategoryTheory.Monoidal.InducingFunctorData {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategoryStruct D] (F : CategoryTheory.Functor D C) : Type (max u₂ v₁)

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

• μIso : (X Y : D) → CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) ≅ F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)

  Analogous to CategoryTheory.LaxMonoidalFunctor.μIso

• whiskerLeft_eq : ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (CategoryTheory.MonoidalCategory.whiskerLeft X f) = CategoryTheory.CategoryStruct.comp (self.μIso X Y₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (F.map f)) (self.μIso X Y₂).hom)
• whiskerRight_eq : ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (CategoryTheory.MonoidalCategory.whiskerRight f Y) = CategoryTheory.CategoryStruct.comp (self.μIso X₁ Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj Y)) (self.μIso X₂ Y).hom)
• tensorHom_eq : ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), F.map (CategoryTheory.MonoidalCategory.tensorHom f g) = CategoryTheory.CategoryStruct.comp (self.μIso X₁ X₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (self.μIso Y₁ Y₂).hom)
• εIso : 𝟙_ C ≅ F.obj (𝟙_ D)

  Analogous to CategoryTheory.LaxMonoidalFunctor.εIso

• associator_eq : ∀ (X Y Z : D), F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (((self.μIso (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).symm ≪≫ ((self.μIso X Y).symm ⊗ CategoryTheory.Iso.refl (F.obj Z))) ≪≫ CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (CategoryTheory.Iso.refl (F.obj X) ⊗ self.μIso Y Z) ≪≫ self.μIso X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom
• leftUnitor_eq : ∀ (X : D), F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom = (((self.μIso (𝟙_ D) X).symm ≪≫ (self.εIso.symm ⊗ CategoryTheory.Iso.refl (F.obj X))) ≪≫ CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom
• rightUnitor_eq : ∀ (X : D), F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom = (((self.μIso X (𝟙_ D)).symm ≪≫ (CategoryTheory.Iso.refl (F.obj X) ⊗ self.εIso.symm)) ≪≫ CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom

theorem CategoryTheory.Monoidal.InducingFunctorData.whiskerLeft_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategoryStruct D] {F : CategoryTheory.Functor D C} (self : CategoryTheory.Monoidal.InducingFunctorData F) (X : D) {Y₁ : D} {Y₂ : D} (f : Y₁ ⟶ Y₂) : F.map (CategoryTheory.MonoidalCategory.whiskerLeft X f) = CategoryTheory.CategoryStruct.comp (self.μIso X Y₁).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (F.map f)) (self.μIso X Y₂).hom)

theorem CategoryTheory.Monoidal.InducingFunctorData.whiskerRight_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategoryStruct D] {F : CategoryTheory.Functor D C} (self : CategoryTheory.Monoidal.InducingFunctorData F) {X₁ : D} {X₂ : D} (f : X₁ ⟶ X₂) (Y : D) : F.map (CategoryTheory.MonoidalCategory.whiskerRight f Y) = CategoryTheory.CategoryStruct.comp (self.μIso X₁ Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj Y)) (self.μIso X₂ Y).hom)

theorem CategoryTheory.Monoidal.InducingFunctorData.tensorHom_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategoryStruct D] {F : CategoryTheory.Functor D C} (self : CategoryTheory.Monoidal.InducingFunctorData F) {X₁ : D} {Y₁ : D} {X₂ : D} {Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : F.map (CategoryTheory.MonoidalCategory.tensorHom f g) = CategoryTheory.CategoryStruct.comp (self.μIso X₁ X₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (self.μIso Y₁ Y₂).hom)

theorem CategoryTheory.Monoidal.InducingFunctorData.associator_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategoryStruct D] {F : CategoryTheory.Functor D C} (self : CategoryTheory.Monoidal.InducingFunctorData F) (X : D) (Y : D) (Z : D) : F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (((self.μIso (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).symm ≪≫ ((self.μIso X Y).symm ⊗ CategoryTheory.Iso.refl (F.obj Z))) ≪≫ CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z) ≪≫ (CategoryTheory.Iso.refl (F.obj X) ⊗ self.μIso Y Z) ≪≫ self.μIso X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom

theorem CategoryTheory.Monoidal.InducingFunctorData.leftUnitor_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategoryStruct D] {F : CategoryTheory.Functor D C} (self : CategoryTheory.Monoidal.InducingFunctorData F) (X : D) : F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom = (((self.μIso (𝟙_ D) X).symm ≪≫ (self.εIso.symm ⊗ CategoryTheory.Iso.refl (F.obj X))) ≪≫ CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom

theorem CategoryTheory.Monoidal.InducingFunctorData.rightUnitor_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategoryStruct D] {F : CategoryTheory.Functor D C} (self : CategoryTheory.Monoidal.InducingFunctorData F) (X : D) : F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom = (((self.μIso X (𝟙_ D)).symm ≪≫ (CategoryTheory.Iso.refl (F.obj X) ⊗ self.εIso.symm)) ≪≫ CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom

def CategoryTheory.Monoidal.induced {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategoryStruct D] (F : CategoryTheory.Functor D C) [F.Faithful] (fData : CategoryTheory.Monoidal.InducingFunctorData F) : CategoryTheory.MonoidalCategory D

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

• CategoryTheory.Monoidal.induced F fData = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Monoidal.fromInduced_toLaxMonoidalFunctor_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategoryStruct D] (F : CategoryTheory.Functor D C) [F.Faithful] (fData : CategoryTheory.Monoidal.InducingFunctorData F) : (CategoryTheory.Monoidal.fromInduced F fData).ε = fData.εIso.hom

@[simp]

theorem CategoryTheory.Monoidal.fromInduced_toLaxMonoidalFunctor_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategoryStruct D] (F : CategoryTheory.Functor D C) [F.Faithful] (fData : CategoryTheory.Monoidal.InducingFunctorData F) (X : D) (Y : D) : (CategoryTheory.Monoidal.fromInduced F fData).μ X Y = (fData.μIso X Y).hom

@[simp]

theorem CategoryTheory.Monoidal.fromInduced_toLaxMonoidalFunctor_toFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategoryStruct D] (F : CategoryTheory.Functor D C) [F.Faithful] (fData : CategoryTheory.Monoidal.InducingFunctorData F) : (CategoryTheory.Monoidal.fromInduced F fData).toFunctor = F

def CategoryTheory.Monoidal.fromInduced {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategoryStruct D] (F : CategoryTheory.Functor D C) [F.Faithful] (fData : CategoryTheory.Monoidal.InducingFunctorData F) : CategoryTheory.MonoidalFunctor D C

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.

theorem CategoryTheory.Monoidal.transportStruct_tensorUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : 𝟙_ D = e.functor.obj (𝟙_ C)

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_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 (CategoryTheory.MonoidalCategory.whiskerRightIso (e.unitIso.app (𝟙_ C)).symm (e.inverse.obj X) ≪≫ CategoryTheory.MonoidalCategory.leftUnitor (e.inverse.obj X)) ≪≫ e.counitIso.app X

theorem CategoryTheory.Monoidal.transportStruct_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))

theorem CategoryTheory.Monoidal.transportStruct_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))

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

theorem CategoryTheory.Monoidal.transportStruct_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))

theorem CategoryTheory.Monoidal.transportStruct_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.MonoidalCategory.whiskerLeftIso (e.inverse.obj X) (e.unitIso.app (𝟙_ C)).symm ≪≫ CategoryTheory.MonoidalCategory.rightUnitor (e.inverse.obj X)) ≪≫ e.counitIso.app X

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

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

Equations

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

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.

Equations

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

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.

Equations

• CategoryTheory.Monoidal.Transported x = D

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)

Equations

• CategoryTheory.Monoidal.instCategoryTransported e = inferInstance

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

Equations

• CategoryTheory.Monoidal.Transported.instMonoidalCategoryStruct e = CategoryTheory.Monoidal.transportStruct e

instance CategoryTheory.Monoidal.Transported.instMonoidalCategory {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)

Equations

• CategoryTheory.Monoidal.Transported.instMonoidalCategory e = CategoryTheory.Monoidal.transport e

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)

Equations

• CategoryTheory.Monoidal.instInhabitedTransported e = { default := 𝟙_ (CategoryTheory.Monoidal.Transported e) }

@[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).ε = e.unitIso.hom.app (𝟙_ C)

@[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).toFunctor = e.inverse

@[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) : (CategoryTheory.Monoidal.fromTransported e).μ X Y = e.unitIso.hom.app (CategoryTheory.MonoidalCategory.tensorObj (e.inverse.obj X) (e.inverse.obj Y))

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.

Equations

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

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.Monoidal.fromTransported e).IsEquivalence

Equations

• ⋯ = ⋯

@[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 = (e.symm.toAdjunction.homEquiv (CategoryTheory.MonoidalCategory.tensorObj (e.functor.obj X) (e.functor.obj Y)) (CategoryTheory.MonoidalCategory.tensorObj X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (e.unitIso.hom.app (CategoryTheory.MonoidalCategory.tensorObj (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y))))) (CategoryTheory.MonoidalCategory.tensorHom (e.symm.counit.app X) (e.symm.counit.app Y)))

@[simp]

theorem CategoryTheory.Monoidal.toTransported_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.toTransported e).toFunctor = e.functor

@[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).ε = (e.symm.toAdjunction.homEquiv (𝟙_ (CategoryTheory.Monoidal.Transported e)) (𝟙_ C)) (CategoryTheory.inv (e.unitIso.hom.app (𝟙_ C)))

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.

Equations

• CategoryTheory.Monoidal.toTransported e = CategoryTheory.monoidalInverse (CategoryTheory.Monoidal.fromTransported e) e.symm.toAdjunction

instance CategoryTheory.Monoidal.instIsEquivalenceTransportedToTransported {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).IsEquivalence

Equations

• ⋯ = ⋯

@[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.inv (CategoryTheory.monoidalCounit (CategoryTheory.Monoidal.fromTransported e) e.symm.toAdjunction)

@[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.monoidalCounit (CategoryTheory.Monoidal.fromTransported e) e.symm.toAdjunction

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.toTransported e).toLaxMonoidalFunctor ⊗⋙ (CategoryTheory.Monoidal.fromTransported e).toLaxMonoidalFunctor

The unit isomorphism upgrades to a monoidal isomorphism.

Equations

• CategoryTheory.Monoidal.transportedMonoidalUnitIso e = (CategoryTheory.asIso (CategoryTheory.monoidalCounit (CategoryTheory.Monoidal.fromTransported e) e.symm.toAdjunction)).symm

@[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.inv (CategoryTheory.monoidalUnit (CategoryTheory.Monoidal.fromTransported e) e.symm.toAdjunction)

@[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.monoidalUnit (CategoryTheory.Monoidal.fromTransported e) e.symm.toAdjunction

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.toTransported e).toLaxMonoidalFunctor ≅ CategoryTheory.LaxMonoidalFunctor.id (CategoryTheory.Monoidal.Transported e)

The counit isomorphism upgrades to a monoidal isomorphism.

Equations

• CategoryTheory.Monoidal.transportedMonoidalCounitIso e = (CategoryTheory.asIso (CategoryTheory.monoidalUnit (CategoryTheory.Monoidal.fromTransported e) e.symm.toAdjunction)).symm