Documentation

Mathlib.CategoryTheory.Monoidal.Preadditive

Preadditive monoidal categories #

A monoidal category is MonoidalPreadditive if it is preadditive and tensor product of morphisms is linear in both factors.

A category is MonoidalPreadditive if tensoring is additive in both factors.

Note we don't extend Preadditive C here, as Abelian C already extends it, and we'll need to have both typeclasses sometimes.

Instances