Transport a symmetric monoidal structure along an equivalence of categories

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

Equations

• CategoryTheory.Monoidal.Transported.instBraidedCategory e = CategoryTheory.BraidedCategory.ofFullyFaithful (CategoryTheory.Monoidal.equivalenceTransported e).inverse

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

Equations

• CategoryTheory.Monoidal.instBraidedTransportedInverseEquivalenceTransported e = { toMonoidal := CategoryTheory.Monoidal.instMonoidalTransportedInverseEquivalenceTransported e, braided := ⋯ }

def CategoryTheory.Monoidal.transportedFunctorCompInverseLaxBraided {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) [MonoidalCategory C] [BraidedCategory C] : ((equivalenceTransported e).functor.comp (equivalenceTransported e).inverse).LaxBraided

This is a def because once we have that both (e' e).inverse and (e' e).functor are braided, this causes a diamond.

Equations

• CategoryTheory.Monoidal.transportedFunctorCompInverseLaxBraided e = CategoryTheory.Functor.LaxBraided.ofNatIso (CategoryTheory.Monoidal.equivalenceTransported e).unitIso

def CategoryTheory.Monoidal.transportedFunctorCompInverseBraided {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) [MonoidalCategory C] [BraidedCategory C] : ((equivalenceTransported e).functor.comp (equivalenceTransported e).inverse).Braided

This is a def because once we have that both (e' e).inverse and (e' e).functor are braided, this causes a diamond.

Equations

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

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

Equations

• CategoryTheory.Monoidal.instBraidedTransportedFunctorEquivalenceTransported e = { toMonoidal := CategoryTheory.Monoidal.instMonoidalTransportedFunctorEquivalenceTransported e, braided := ⋯ }

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

Equations

• CategoryTheory.Monoidal.Transported.instSymmetricCategory e = CategoryTheory.symmetricCategoryOfFullyFaithful (CategoryTheory.Monoidal.equivalenceTransported e).inverse