# Documentation

If C is a preadditive category 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 CategoryTheory.Monad.algebraPreadditive_homGroup_zsmul_f (C : Type u₁) [] (T : ) [CategoryTheory.Functor.Additive T.toFunctor] (F : ) (G : ) (r : ) (α : F G) :
(r α).f = r α.f
@[simp]
theorem CategoryTheory.Monad.algebraPreadditive_homGroup_sub_f (C : Type u₁) [] (T : ) [CategoryTheory.Functor.Additive T.toFunctor] (F : ) (G : ) (α : F G) (β : F G) :
(α - β).f = α.f - β.f
@[simp]
theorem CategoryTheory.Monad.algebraPreadditive_homGroup_neg_f (C : Type u₁) [] (T : ) [CategoryTheory.Functor.Additive T.toFunctor] (F : ) (G : ) (α : F G) :
(-α).f = -α.f
@[simp]
theorem CategoryTheory.Monad.algebraPreadditive_homGroup_add_f (C : Type u₁) [] (T : ) [CategoryTheory.Functor.Additive T.toFunctor] (F : ) (G : ) (α : F G) (β : F G) :
(α + β).f = α.f + β.f
@[simp]
theorem CategoryTheory.Monad.algebraPreadditive_homGroup_zero_f (C : Type u₁) [] (T : ) [CategoryTheory.Functor.Additive T.toFunctor] (F : ) (G : ) :
0.f = 0
@[simp]
theorem CategoryTheory.Monad.algebraPreadditive_homGroup_nsmul_f (C : Type u₁) [] (T : ) [CategoryTheory.Functor.Additive T.toFunctor] (F : ) (G : ) (n : ) (α : F G) :
(n α).f = n α.f

Equations
• = { homGroup := fun (F G : ) => , add_comp := , comp_add := }
Equations
• =
@[simp]
theorem CategoryTheory.Comonad.coalgebraPreadditive_homGroup_neg_f (C : Type u₁) [] (U : ) [CategoryTheory.Functor.Additive U.toFunctor] (α : F G) :
(-α).f = -α.f
@[simp]
theorem CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zsmul_f (C : Type u₁) [] (U : ) [CategoryTheory.Functor.Additive U.toFunctor] (r : ) (α : F G) :
(r α).f = r α.f
@[simp]
theorem CategoryTheory.Comonad.coalgebraPreadditive_homGroup_sub_f (C : Type u₁) [] (U : ) [CategoryTheory.Functor.Additive U.toFunctor] (α : F G) (β : F G) :
(α - β).f = α.f - β.f
@[simp]
theorem CategoryTheory.Comonad.coalgebraPreadditive_homGroup_nsmul_f (C : Type u₁) [] (U : ) [CategoryTheory.Functor.Additive U.toFunctor] (n : ) (α : F G) :
(n α).f = n α.f
@[simp]