mathlib3 documentation


Transport a monoidal structure along an equivalence. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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