mathlib documentation

category_theory.preadditive.endo_functor

Preadditive structure on algebras over a monad #

If C is a preadditive categories and F is an additive endofunctor on C then algebra F is also preadditive. Dually, the category coalgebra F is also preadditive.

@[protected, instance]

The category of algebras over an additive endofunctor on a preadditive category is preadditive.

Equations
@[protected, instance]
Equations