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.

source

@[simp]

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

(α + β).f = α.f + β.f

source

@[simp]

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

0.f = 0

source

@[simp]

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

(α - β).f = α.f - β.f

source

@[simp]

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

(r • α).f = r • α.f

source

@[simp]

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

(n • α).f = n • α.f

source

@[simp]

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

(-α).f = -α.f

source

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

CategoryTheory.Preadditive (CategoryTheory.Endofunctor.Algebra F)

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

source

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

CategoryTheory.Functor.Additive (CategoryTheory.Endofunctor.Algebra.forget F)

source

@[simp]

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

0.f = 0

source

@[simp]

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

(α + β).f = α.f + β.f

source

@[simp]

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

(-α).f = -α.f

source

@[simp]

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

(r • α).f = r • α.f

source

@[simp]

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

(α - β).f = α.f - β.f

source

@[simp]

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

(n • α).f = n • α.f

source

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

CategoryTheory.Preadditive (CategoryTheory.Endofunctor.Coalgebra F)

source

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

CategoryTheory.Functor.Additive (CategoryTheory.Endofunctor.Coalgebra.forget F)