mathlib documentation


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_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) :

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

Instances for category_theory.monoidal.transported

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