Documentation

Mathlib.CategoryTheory.Monoidal.Braided.Transport

Transport a symmetric monoidal structure along an equivalence of categories #

source
@[implicit_reducible]
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
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
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
source
@[implicit_reducible]
noncomputable 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
Instances For
    source
    @[implicit_reducible]
    noncomputable 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.
    Instances For
      source
      @[implicit_reducible]
      noncomputable 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
      source
      @[implicit_reducible]
      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