mathlib documentation

category_theory.preadditive.eilenberg_moore

Preadditive structure on algebras over a monad #

If C is a preadditive categories and T is an additive monad on C then algebra T is also preadditive. Dually, if U is an additive comonad on C then coalgebra U is preadditive as well.

@[simp]
@[protected, instance]

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

Equations
@[simp]
@[protected, instance]

The category of coalgebras over an additive comonad on a preadditive category is preadditive.

Equations