Documentation

Mathlib.CategoryTheory.Preadditive.EndoFunctor

Preadditive structure on algebras over a monad #

If C is a preadditive category and F is an additive endofunctor on C then Algebra F is also preadditive. Dually, the category Coalgebra F is also preadditive.