Preadditive structure on algebras over a monad

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.

instance CategoryTheory.Endofunctor.algebraPreadditive (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] : Preadditive (Algebra F)

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

Equations

• CategoryTheory.Endofunctor.algebraPreadditive C F = { homGroup := fun (A₁ A₂ : CategoryTheory.Endofunctor.Algebra F) => AddCommGroup.mk ⋯, add_comp := ⋯, comp_add := ⋯ }

@[simp]

theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_add_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Algebra F) (α β : A₁ ⟶ A₂) : (α + β).f = α.f + β.f

@[simp]

theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zero_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Algebra F) : Algebra.Hom.f 0 = 0

@[simp]

theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_neg_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Algebra F) (α : A₁ ⟶ A₂) : (-α).f = -α.f

@[simp]

theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zsmul_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Algebra F) (r : ℤ) (α : A₁ ⟶ A₂) : (r • α).f = r • α.f

@[simp]

theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_sub_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Algebra F) (α β : A₁ ⟶ A₂) : (α - β).f = α.f - β.f

@[simp]

theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_nsmul_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Algebra F) (n : ℕ) (α : A₁ ⟶ A₂) : (n • α).f = n • α.f

instance CategoryTheory.Algebra.forget_additive (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] : (Endofunctor.Algebra.forget F).Additive

instance CategoryTheory.Endofunctor.coalgebraPreadditive (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] : Preadditive (Coalgebra F)

Equations

• CategoryTheory.Endofunctor.coalgebraPreadditive C F = { homGroup := fun (A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F) => AddCommGroup.mk ⋯, add_comp := ⋯, comp_add := ⋯ }

@[simp]

theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_sub_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Coalgebra F) (α β : A₁ ⟶ A₂) : (α - β).f = α.f - β.f

@[simp]

theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_add_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Coalgebra F) (α β : A₁ ⟶ A₂) : (α + β).f = α.f + β.f

@[simp]

theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_neg_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Coalgebra F) (α : A₁ ⟶ A₂) : (-α).f = -α.f

@[simp]

theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zsmul_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Coalgebra F) (r : ℤ) (α : A₁ ⟶ A₂) : (r • α).f = r • α.f

@[simp]

theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zero_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Coalgebra F) : Coalgebra.Hom.f 0 = 0

@[simp]

theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_nsmul_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Coalgebra F) (n : ℕ) (α : A₁ ⟶ A₂) : (n • α).f = n • α.f

instance CategoryTheory.Coalgebra.forget_additive (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] : (Endofunctor.Coalgebra.forget F).Additive