# mathlibdocumentation

category_theory.monoidal.transport

# 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, obtaining a monoidal structure on D.

We then upgrade the original functor and its inverse to monoidal functors with respect to the new monoidal structure on D.

theorem category_theory.monoidal.transport_left_unitor {C : Type u₁} {D : Type u₂} (e : C D) (X : D) :
theorem category_theory.monoidal.transport_associator {C : Type u₁} {D : Type u₂} (e : C D) (X Y Z : D) :
theorem category_theory.monoidal.transport_tensor_unit {C : Type u₁} {D : Type u₂} (e : C D) :
def category_theory.monoidal.transport {C : Type u₁} {D : Type u₂} (e : C D) :

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

Equations
theorem category_theory.monoidal.transport_tensor_hom {C : Type u₁} {D : Type u₂} (e : C D) (W X Y Z : D) (f : W X) (g : Y Z) :
theorem category_theory.monoidal.transport_tensor_obj {C : Type u₁} {D : Type u₂} (e : C D) (X Y : D) :
theorem category_theory.monoidal.transport_right_unitor {C : Type u₁} {D : Type u₂} (e : C D) (X : D) :
@[protected, instance]
def category_theory.monoidal.transported.category {C : Type u₁} {D : Type u₂} (e : C D) :
@[nolint]
def category_theory.monoidal.transported {C : Type u₁} {D : Type u₂} (e : C D) :
Type u₂

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

Equations
Instances for category_theory.monoidal.transported
@[protected, instance]
def category_theory.monoidal.transported.category_theory.monoidal_category {C : Type u₁} {D : Type u₂} (e : C D) :
Equations
@[protected, instance]
def category_theory.monoidal.transported.inhabited {C : Type u₁} {D : Type u₂} (e : C D) :
Equations
@[simp]
theorem category_theory.monoidal.lax_to_transported_μ {C : Type u₁} {D : Type u₂} (e : C D) (X Y : C) :
@[simp]
theorem category_theory.monoidal.lax_to_transported_ε {C : Type u₁} {D : Type u₂} (e : C D) :
@[simp]
theorem category_theory.monoidal.lax_to_transported_to_functor {C : Type u₁} {D : Type u₂} (e : C D) :
def category_theory.monoidal.lax_to_transported {C : Type u₁} {D : Type u₂} (e : C D) :

We can upgrade e.functor to a lax monoidal functor from C to D with the transported structure.

Equations
@[simp]
theorem category_theory.monoidal.to_transported_to_lax_monoidal_functor {C : Type u₁} {D : Type u₂} (e : C D) :
def category_theory.monoidal.to_transported {C : Type u₁} {D : Type u₂} (e : C D) :

We can upgrade e.functor to a monoidal functor from C to D with the transported structure.

Equations
@[protected, instance]
Equations
noncomputable def category_theory.monoidal.from_transported {C : Type u₁} {D : Type u₂} (e : C D) :

We can upgrade e.inverse to a monoidal functor from D with the transported structure to C.

Equations
@[simp]
theorem category_theory.monoidal.from_transported_to_lax_monoidal_functor_to_functor {C : Type u₁} {D : Type u₂} (e : C D) :
@[simp]
@[simp]
@[simp]
noncomputable def category_theory.monoidal.transported_monoidal_unit_iso {C : Type u₁} {D : Type u₂} (e : C D) :

The unit isomorphism upgrades to a monoidal isomorphism.

Equations
@[simp]
noncomputable def category_theory.monoidal.transported_monoidal_counit_iso {C : Type u₁} {D : Type u₂} (e : C D) :

The counit isomorphism upgrades to a monoidal isomorphism.

Equations
@[simp]