inducingFunctorData — Mathlib

English

There is a canonical identification between the underlying type of the object 'of R X' and X itself, i.e., the carrier type of the algebra object corresponding to X is just X.

Русский

Существует каноническое тождество между базовым множеством объекта 'of R X' и X; носитель объекта, соответствующего X, просто равен X.

LaTeX

$$$(\mathrm{of\, R\, X})\;\text{carrier} = X$$$

Lean4

/-- The data needed to induce a `MonoidalCategory` structure via
`CoalgCat.instMonoidalCategoryStruct` and the forgetful functor to modules. -/
@[simps]
noncomputable def inducingFunctorData : Monoidal.InducingFunctorData (forget₂ (CoalgCat R) (ModuleCat R))
    where
  μIso _ _ := Iso.refl _
  whiskerLeft_eq X Y Z f := by ext; rfl
  whiskerRight_eq X f := by ext; rfl
  tensorHom_eq f g := by ext; rfl
  εIso := Iso.refl _
  associator_eq X Y Z := ModuleCat.hom_ext <| TensorProduct.ext <| TensorProduct.ext <| by ext; rfl
  leftUnitor_eq X := ModuleCat.hom_ext <| TensorProduct.ext <| by ext; rfl
  rightUnitor_eq X := ModuleCat.hom_ext <| TensorProduct.ext <| by ext; rfl

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