mathlib3 documentation

category_theory.preadditive.eilenberg_moore

Preadditive structure on algebras over a monad #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[protected, instance]

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

Equations
@[protected, instance]

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

Equations