# Documentation

If C is a preadditive category and F is an additive endofunctor on C then Algebra F is also preadditive. Dually, the category Coalgebra F is also preadditive.

@[simp]
theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_add_f (C : Type u₁) [] (F : ) [F.Additive] (α : A₁ A₂) (β : A₁ A₂) :
(α + β).f = α.f + β.f
@[simp]
theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zero_f (C : Type u₁) [] (F : ) [F.Additive] :
@[simp]
theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_sub_f (C : Type u₁) [] (F : ) [F.Additive] (α : A₁ A₂) (β : A₁ A₂) :
(α - β).f = α.f - β.f
@[simp]
theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zsmul_f (C : Type u₁) [] (F : ) [F.Additive] (r : ) (α : A₁ A₂) :
(r α).f = r α.f
@[simp]
theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_nsmul_f (C : Type u₁) [] (F : ) [F.Additive] (n : ) (α : A₁ A₂) :
(n α).f = n α.f
@[simp]
theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_neg_f (C : Type u₁) [] (F : ) [F.Additive] (α : A₁ A₂) :
(-α).f = -α.f
instance CategoryTheory.Endofunctor.algebraPreadditive (C : Type u₁) [] (F : ) [F.Additive] :

Equations
• = { homGroup := fun (A₁ A₂ : ) => , add_comp := , comp_add := }
instance CategoryTheory.Algebra.forget_additive (C : Type u₁) [] (F : ) [F.Additive] :
Equations
• =
@[simp]
theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zero_f (C : Type u₁) [] (F : ) [F.Additive] :
@[simp]
theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_add_f (C : Type u₁) [] (F : ) [F.Additive] (α : A₁ A₂) (β : A₁ A₂) :
(α + β).f = α.f + β.f
@[simp]
theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_neg_f (C : Type u₁) [] (F : ) [F.Additive] (α : A₁ A₂) :
(-α).f = -α.f
@[simp]
theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zsmul_f (C : Type u₁) [] (F : ) [F.Additive] (r : ) (α : A₁ A₂) :
(r α).f = r α.f
@[simp]
theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_sub_f (C : Type u₁) [] (F : ) [F.Additive] (α : A₁ A₂) (β : A₁ A₂) :
(α - β).f = α.f - β.f
@[simp]
theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_nsmul_f (C : Type u₁) [] (F : ) [F.Additive] (n : ) (α : A₁ A₂) :
(n α).f = n α.f
instance CategoryTheory.Endofunctor.coalgebraPreadditive (C : Type u₁) [] (F : ) [F.Additive] :
Equations
• = { homGroup := fun (A₁ A₂ : ) => , add_comp := , comp_add := }
instance CategoryTheory.Coalgebra.forget_additive (C : Type u₁) [] (F : ) [F.Additive] :