mathlib documentation

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 don't yet prove anything about this transported structure! The next step would be to show that the original functor can be upgraded to a monoidal functor with respect to this new structure.

@[simp]
theorem category_theory.monoidal.transport_tensor_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C D) (W X Y Z : D) (f : W X) (g : Y Z) :
@[simp]
@[nolint]

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

Equations

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

Equations

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

Equations