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 ≪≫ CategoryTheory.MonoidalCategory.tensorIso (self.μIso X Y).symm (CategoryTheory.Iso.refl (F.obj Z))) ≪≫ CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z) ≪≫ CategoryTheory.MonoidalCategory.tensorIso (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 ≪≫ CategoryTheory.MonoidalCategory.tensorIso 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.MonoidalCategory.tensorIso (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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def CategoryTheory.Monoidal.fromInducedCoreMonoidal {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) : F.CoreMonoidal

A faithful functor equipped with a InducingFunctorData structure is monoidal.

Equations

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

instance CategoryTheory.Monoidal.fromInducedMonoidal {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) : F.Monoidal

Equations

• CategoryTheory.Monoidal.fromInducedMonoidal F fData = (CategoryTheory.Monoidal.fromInducedCoreMonoidal F fData).toMonoidal

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.

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_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_tensorObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X 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_whiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X x✝ x✝¹ : D) (f : x✝ ⟶ x✝¹) : CategoryTheory.MonoidalCategory.whiskerLeft X f = e.functor.map (CategoryTheory.MonoidalCategory.whiskerLeft (e.inverse.obj X) (e.inverse.map f))

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 Y 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_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_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.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) }

@[reducible, inline]

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

We upgrade the equivalence of categories e : C ≌ D to a monoidal category equivalence C ≌ Transported e.

Equations

• CategoryTheory.Monoidal.equivalenceTransported e = e

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

Equations

• CategoryTheory.Monoidal.instMonoidalTransportedInverseEquivalenceTransported e = id inferInstance

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

Equations

• CategoryTheory.Monoidal.instMonoidalTransportedFunctorSymmEquivalenceTransported e = inferInstanceAs (CategoryTheory.Monoidal.equivalenceTransported e).inverse.Monoidal

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

Equations

• CategoryTheory.Monoidal.instMonoidalTransportedFunctorEquivalenceTransported e = (CategoryTheory.Monoidal.equivalenceTransported e).symm.inverseMonoidal

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

Equations

• CategoryTheory.Monoidal.instMonoidalTransportedInverseSymmEquivalenceTransported e = inferInstanceAs (CategoryTheory.Monoidal.equivalenceTransported e).functor.Monoidal

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

instance CategoryTheory.Monoidal.instIsMonoidalUnitTransportedEquivalenceTransported {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.Monoidal.equivalenceTransported e).unit

The unit isomorphism upgrades to a monoidal isomorphism.

instance CategoryTheory.Monoidal.instIsMonoidalTransportedCounitEquivalenceTransported {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.Monoidal.equivalenceTransported e).counit

The counit isomorphism upgrades to a monoidal isomorphism.