English
There is a canonical Monoidal.InducingFunctorData structure making forget₂ (HopfAlgCat R) to (BialgCat R) into a monoidal functor, with coherence isomorphisms given by identity-like data
Русский
Существует каноническая структура Monoidal.InducingFunctorData, делающая forget₂ (HopfAlgCat R) ⥤ (BialgCat R) моноидальным функтором, со связующими изоморфизмами, аналогичными единице
LaTeX
$$HopfAlgCat.MonoidalCategory.inducingFunctorData$$
Lean4
/-- The data needed to induce a `MonoidalCategory` structure via
`HopfAlgCat.instMonoidalCategoryStruct` and the forgetful functor to bialgebras. -/
@[simps]
noncomputable def inducingFunctorData : Monoidal.InducingFunctorData (forget₂ (HopfAlgCat R) (BialgCat R))
where
μIso _ _ := Iso.refl _
whiskerLeft_eq _ _ _ _ := by ext; rfl
whiskerRight_eq _ _ := by ext; rfl
tensorHom_eq _ _ := by ext; rfl
εIso := Iso.refl _
associator_eq _ _
_ := BialgCat.Hom.ext <| BialgHom.coe_linearMap_injective <| TensorProduct.ext <| TensorProduct.ext (by ext; rfl)
leftUnitor_eq _ := BialgCat.Hom.ext <| BialgHom.coe_linearMap_injective <| TensorProduct.ext (by ext; rfl)
rightUnitor_eq _ := BialgCat.Hom.ext <| BialgHom.coe_linearMap_injective <| TensorProduct.ext (by ext; rfl)
