Lean4
/-- Transport a monoidal structure along an equivalence of (plain) categories.
-/
@[simps -isSimp]
def transportStruct (e : C ≌ D) : MonoidalCategoryStruct.{v₂} D
where
tensorObj X Y := e.functor.obj (e.inverse.obj X ⊗ e.inverse.obj Y)
whiskerLeft X _ _ f := e.functor.map (e.inverse.obj X ◁ e.inverse.map f)
whiskerRight f X := e.functor.map (e.inverse.map f ▷ e.inverse.obj X)
tensorHom f g := e.functor.map (e.inverse.map f ⊗ₘ e.inverse.map g)
tensorUnit := e.functor.obj (𝟙_ C)
associator X Y
Z :=
e.functor.mapIso
(whiskerRightIso (e.unitIso.app _).symm _ ≪≫
α_ (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫ whiskerLeftIso _ (e.unitIso.app _))
leftUnitor
X := e.functor.mapIso ((whiskerRightIso (e.unitIso.app _).symm _) ≪≫ λ_ (e.inverse.obj X)) ≪≫ e.counitIso.app _
rightUnitor
X := e.functor.mapIso ((whiskerLeftIso _ (e.unitIso.app _).symm) ≪≫ ρ_ (e.inverse.obj X)) ≪≫ e.counitIso.app _
