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
@[simp]
theorem category_theory.endofunctor.algebra_preadditive_hom_group_add_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C C) [F.additive] (A₁ A₂ : category_theory.endofunctor.algebra F) (α β : A₁ A₂) :
+ β).f = α.f + β.f
@[simp]
theorem category_theory.endofunctor.algebra_preadditive_hom_group_sub_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C C) [F.additive] (A₁ A₂ : category_theory.endofunctor.algebra F) (α β : A₁ A₂) :
- β).f = α.f - β.f
@[simp]
@[simp]
@[protected, instance]
Equations