instMonoidalLinearFullSubcategory

English

If C is monoidal with a MonoidalPreadditive structure and R a ring, then the full subcategory P.FullSubcategory carries a MonoidalLinear structure over R, provided Linear structure on C is compatible.

Русский

При наличии моноидальной структуры C и MonoidalPreadditive структуры вместе с кольцом R, полная подкатегория P.FullSubcategory получает MonoidalLinear структуру над R, совместимую с линейной структурой C.

LaTeX

$$[MonoidalPreadditive C] [MonoidalLinear R C] : MonoidalLinear R P.FullSubcategory$$

Lean4

instance [MonoidalPreadditive C] [MonoidalLinear R C] : MonoidalLinear R P.FullSubcategory :=
  monoidalLinearOfFaithful R P.ι

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