Theorems · Inductive type · category theory

CategoryTheory.MonoidalLinear

(R : Type u_1) →
  [inst : Semiring R] →
    (C : Type u_2) →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [CategoryTheory.Linear R C] →
            [inst : CategoryTheory.MonoidalCategory C] → [CategoryTheory.MonoidalPreadditive C] → Prop

A category is MonoidalLinear R if tensoring is R-linear in both factors.

Defined in

Mathlib.CategoryTheory.Monoidal.Linear

Cited by

4 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

SemiringCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.LinearCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalPreadditive