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₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategoryStruct D] (F : 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) : Iso (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj (MonoidalCategoryStruct.tensorObj X Y))

  Analogous to CategoryTheory.LaxMonoidalFunctor.μIso

• whiskerLeft_eq (X : D) {Y₁ Y₂ : D} (f : Quiver.Hom Y₁ Y₂) : Eq (F.map (MonoidalCategoryStruct.whiskerLeft X f)) (CategoryStruct.comp (self.μIso X Y₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (F.map f)) (self.μIso X Y₂).hom))
• whiskerRight_eq {X₁ X₂ : D} (f : Quiver.Hom X₁ X₂) (Y : D) : Eq (F.map (MonoidalCategoryStruct.whiskerRight f Y)) (CategoryStruct.comp (self.μIso X₁ Y).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj Y)) (self.μIso X₂ Y).hom))
• tensorHom_eq {X₁ Y₁ X₂ Y₂ : D} (f : Quiver.Hom X₁ Y₁) (g : Quiver.Hom X₂ Y₂) : Eq (F.map (MonoidalCategoryStruct.tensorHom f g)) (CategoryStruct.comp (self.μIso X₁ X₂).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (self.μIso Y₁ Y₂).hom))
• εIso : Iso MonoidalCategoryStruct.tensorUnit (F.obj MonoidalCategoryStruct.tensorUnit)

  Analogous to CategoryTheory.LaxMonoidalFunctor.εIso

• associator_eq (X Y Z : D) : Eq (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (((self.μIso (MonoidalCategoryStruct.tensorObj X Y) Z).symm.trans (MonoidalCategory.tensorIso (self.μIso X Y).symm (Iso.refl (F.obj Z)))).trans ((MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).trans ((MonoidalCategory.tensorIso (Iso.refl (F.obj X)) (self.μIso Y Z)).trans (self.μIso X (MonoidalCategoryStruct.tensorObj Y Z))))).hom
• leftUnitor_eq (X : D) : Eq (F.map (MonoidalCategoryStruct.leftUnitor X).hom) (((self.μIso MonoidalCategoryStruct.tensorUnit X).symm.trans (MonoidalCategory.tensorIso self.εIso.symm (Iso.refl (F.obj X)))).trans (MonoidalCategoryStruct.leftUnitor (F.obj X))).hom
• rightUnitor_eq (X : D) : Eq (F.map (MonoidalCategoryStruct.rightUnitor X).hom) (((self.μIso X MonoidalCategoryStruct.tensorUnit).symm.trans (MonoidalCategory.tensorIso (Iso.refl (F.obj X)) self.εIso.symm)).trans (MonoidalCategoryStruct.rightUnitor (F.obj X))).hom

def CategoryTheory.Monoidal.induced {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategoryStruct D] (F : Functor D C) [F.Faithful] (fData : InducingFunctorData F) : 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

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

def CategoryTheory.Monoidal.fromInducedCoreMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategoryStruct D] (F : Functor D C) [F.Faithful] (fData : 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.

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

Equations

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

def CategoryTheory.Monoidal.transportStruct {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) : 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₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) {X₁✝ X₂✝ : D} (f : Quiver.Hom X₁✝ X₂✝) (X : D) : Eq (MonoidalCategoryStruct.whiskerRight f X) (e.functor.map (MonoidalCategoryStruct.whiskerRight (e.inverse.map f) (e.inverse.obj X)))

theorem CategoryTheory.Monoidal.transportStruct_leftUnitor {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) (X : D) : Eq (MonoidalCategoryStruct.leftUnitor X) ((e.functor.mapIso ((MonoidalCategory.whiskerRightIso (e.unitIso.app MonoidalCategoryStruct.tensorUnit).symm (e.inverse.obj X)).trans (MonoidalCategoryStruct.leftUnitor (e.inverse.obj X)))).trans (e.counitIso.app X))

theorem CategoryTheory.Monoidal.transportStruct_tensorObj {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) (X Y : D) : Eq (MonoidalCategoryStruct.tensorObj X Y) (e.functor.obj (MonoidalCategoryStruct.tensorObj (e.inverse.obj X) (e.inverse.obj Y)))

theorem CategoryTheory.Monoidal.transportStruct_whiskerLeft {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) (X x✝ x✝¹ : D) (f : Quiver.Hom x✝ x✝¹) : Eq (MonoidalCategoryStruct.whiskerLeft X f) (e.functor.map (MonoidalCategoryStruct.whiskerLeft (e.inverse.obj X) (e.inverse.map f)))

theorem CategoryTheory.Monoidal.transportStruct_tensorUnit {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) : Eq MonoidalCategoryStruct.tensorUnit (e.functor.obj MonoidalCategoryStruct.tensorUnit)

theorem CategoryTheory.Monoidal.transportStruct_associator {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) (X Y Z : D) : Eq (MonoidalCategoryStruct.associator X Y Z) (e.functor.mapIso ((MonoidalCategory.whiskerRightIso (e.unitIso.app (MonoidalCategoryStruct.tensorObj (e.inverse.obj X) (e.inverse.obj Y))).symm (e.inverse.obj Z)).trans ((MonoidalCategoryStruct.associator (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z)).trans (MonoidalCategory.whiskerLeftIso (e.inverse.obj X) (e.unitIso.app (MonoidalCategoryStruct.tensorObj (e.inverse.obj Y) (e.inverse.obj Z)))))))

theorem CategoryTheory.Monoidal.transportStruct_tensorHom {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) {X₁✝ Y₁✝ X₂✝ Y₂✝ : D} (f : Quiver.Hom X₁✝ Y₁✝) (g : Quiver.Hom X₂✝ Y₂✝) : Eq (MonoidalCategoryStruct.tensorHom f g) (e.functor.map (MonoidalCategoryStruct.tensorHom (e.inverse.map f) (e.inverse.map g)))

theorem CategoryTheory.Monoidal.transportStruct_rightUnitor {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) (X : D) : Eq (MonoidalCategoryStruct.rightUnitor X) ((e.functor.mapIso ((MonoidalCategory.whiskerLeftIso (e.inverse.obj X) (e.unitIso.app MonoidalCategoryStruct.tensorUnit).symm).trans (MonoidalCategoryStruct.rightUnitor (e.inverse.obj X)))).trans (e.counitIso.app X))

def CategoryTheory.Monoidal.transport {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) : 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₁} [Category C] {D : Type u₂} [Category D] : Equivalence C D → Type u₂

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

Equations

• Eq (CategoryTheory.Monoidal.Transported x✝) D

def CategoryTheory.Monoidal.instCategoryTransported {C : Type u₁} [Category C] {D : Type u₂} [Category D] (e : Equivalence C D) : Category (Transported e)

Equations

• Eq (CategoryTheory.Monoidal.instCategoryTransported e) inferInstance

def CategoryTheory.Monoidal.Transported.instMonoidalCategoryStruct {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) : MonoidalCategoryStruct (Transported e)

Equations

• Eq (CategoryTheory.Monoidal.Transported.instMonoidalCategoryStruct e) (CategoryTheory.Monoidal.transportStruct e)

def CategoryTheory.Monoidal.Transported.instMonoidalCategory {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) : MonoidalCategory (Transported e)

Equations

• Eq (CategoryTheory.Monoidal.Transported.instMonoidalCategory e) (CategoryTheory.Monoidal.transport e)

def CategoryTheory.Monoidal.instInhabitedTransported {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) : Inhabited (Transported e)

Equations

• Eq (CategoryTheory.Monoidal.instInhabitedTransported e) { default := CategoryTheory.MonoidalCategoryStruct.tensorUnit }

@[reducible, inline]

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

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

Equations

• Eq (CategoryTheory.Monoidal.equivalenceTransported e) e

def CategoryTheory.Monoidal.instMonoidalTransportedInverseEquivalenceTransported {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) : (equivalenceTransported e).inverse.Monoidal

Equations

• Eq (CategoryTheory.Monoidal.instMonoidalTransportedInverseEquivalenceTransported e) (id inferInstance)

def CategoryTheory.Monoidal.instMonoidalTransportedFunctorSymmEquivalenceTransported {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) : (equivalenceTransported e).symm.functor.Monoidal

Equations

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

def CategoryTheory.Monoidal.instMonoidalTransportedFunctorEquivalenceTransported {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) : (equivalenceTransported e).functor.Monoidal

Equations

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

def CategoryTheory.Monoidal.instMonoidalTransportedInverseSymmEquivalenceTransported {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) : (equivalenceTransported e).symm.inverse.Monoidal

Equations

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

theorem CategoryTheory.Monoidal.instIsMonoidalTransportedSymmEquivalenceTransported {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] (e : Equivalence C D) : (equivalenceTransported e).symm.IsMonoidal

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

The unit isomorphism upgrades to a monoidal isomorphism.

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

The counit isomorphism upgrades to a monoidal isomorphism.