# 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]
theorem category_theory.monad.algebra_preadditive_hom_group_neg_f (C : Type u₁) (T : category_theory.monad C) [T.additive] (F G : T.algebra) (α : F G) :
(-α).f = -α.f
@[simp]
theorem category_theory.monad.algebra_preadditive_hom_group_zsmul_f (C : Type u₁) (T : category_theory.monad C) [T.additive] (F G : T.algebra) (r : ) (α : F G) :
α).f = r α.f
@[simp]
theorem category_theory.monad.algebra_preadditive_hom_group_nsmul_f (C : Type u₁) (T : category_theory.monad C) [T.additive] (F G : T.algebra) (n : ) (α : F G) :
α).f = n α.f
@[simp]
theorem category_theory.monad.algebra_preadditive_hom_group_sub_f (C : Type u₁) (T : category_theory.monad C) [T.additive] (F G : T.algebra) (α β : F G) :
- β).f = α.f - β.f
@[protected, instance]

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

Equations
@[simp]
theorem category_theory.monad.algebra_preadditive_hom_group_add_f (C : Type u₁) (T : category_theory.monad C) [T.additive] (F G : T.algebra) (α β : F G) :
+ β).f = α.f + β.f
@[protected, instance]
@[simp]
theorem category_theory.comonad.coalgebra_preadditive_hom_group_neg_f (C : Type u₁) (U : category_theory.comonad C) [U.additive] (F G : U.coalgebra) (α : F G) :
(-α).f = -α.f
@[protected, instance]

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

Equations
@[simp]
theorem category_theory.comonad.coalgebra_preadditive_hom_group_zsmul_f (C : Type u₁) (U : category_theory.comonad C) [U.additive] (F G : U.coalgebra) (r : ) (α : F G) :
α).f = r α.f
@[simp]
theorem category_theory.comonad.coalgebra_preadditive_hom_group_sub_f (C : Type u₁) (U : category_theory.comonad C) [U.additive] (F G : U.coalgebra) (α β : F G) :
- β).f = α.f - β.f
@[simp]
theorem category_theory.comonad.coalgebra_preadditive_hom_group_add_f (C : Type u₁) (U : category_theory.comonad C) [U.additive] (F G : U.coalgebra) (α β : F G) :
+ β).f = α.f + β.f
@[simp]
theorem category_theory.comonad.coalgebra_preadditive_hom_group_nsmul_f (C : Type u₁) (U : category_theory.comonad C) [U.additive] (F G : U.coalgebra) (n : ) (α : F G) :
α).f = n α.f
@[protected, instance]