inducingFunctorData — Mathlib

English

The forgetful functor from BialgCat to AlgCat inherits a monoidal structure, i.e., it can be promoted to a monoidal functor between the respective forgetful contexts.

Русский

Забывающий функтор из BialgCat в AlgCat наследует монодическую структуру и представляет собой моноидальный функтор между соответствующими забывательными контекстами.

LaTeX

$$$(forget₂(\mathrm{BialgCat}\, R)\, \mathrm{toAlgCat}\, R)\;\text{ is Monoidal}$$$

Lean4

/-- The data needed to induce a `MonoidalCategory` structure via
`BialgCat.instMonoidalCategoryStruct` and the forgetful functor to algebras. -/
@[simps]
noncomputable def inducingFunctorData : Monoidal.InducingFunctorData (forget₂ (BialgCat R) (AlgCat 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 _ _
    _ :=
    AlgCat.hom_ext _ <| Algebra.TensorProduct.ext (Algebra.TensorProduct.ext (by ext; rfl) (by ext; rfl)) (by ext; rfl)
  leftUnitor_eq _ := AlgCat.hom_ext _ <| Algebra.TensorProduct.ext rfl (by ext; rfl)
  rightUnitor_eq _ := AlgCat.hom_ext _ <| Algebra.TensorProduct.ext (by ext; rfl) rfl

Похожие утверждения