# mathlibdocumentation

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]
(-α).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]
- β).f = α.f - β.f
@[protected, instance]

Equations
@[simp]
+ β).f = α.f + β.f
@[protected, instance]
@[simp]
(-α).f = -α.f
@[protected, instance]

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]
- β).f = α.f - β.f
@[simp]
+ β).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]