Preadditive structure on algebras over a monad

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₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (T : CategoryTheory.Monad C) [CategoryTheory.Functor.Additive T.toFunctor] (F : CategoryTheory.Monad.Algebra T) (G : CategoryTheory.Monad.Algebra T) (r : ℤ) (α : F ⟶ G) : (r • α).f = r • α.f

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Monad.algebraPreadditive_homGroup_zero_f (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (T : CategoryTheory.Monad C) [CategoryTheory.Functor.Additive T.toFunctor] (F : CategoryTheory.Monad.Algebra T) (G : CategoryTheory.Monad.Algebra T) : 0.f = 0

@[simp]

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

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

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

Equations

• CategoryTheory.Monad.algebraPreadditive C T = { homGroup := fun (F G : CategoryTheory.Monad.Algebra T) => AddCommGroup.mk ⋯, add_comp := ⋯, comp_add := ⋯ }

instance CategoryTheory.Monad.forget_additive (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (T : CategoryTheory.Monad C) [CategoryTheory.Functor.Additive T.toFunctor] : CategoryTheory.Functor.Additive (CategoryTheory.Monad.forget T)

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zero_f (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (U : CategoryTheory.Comonad C) [CategoryTheory.Functor.Additive U.toFunctor] (F : CategoryTheory.Comonad.Coalgebra U) (G : CategoryTheory.Comonad.Coalgebra U) : 0.f = 0

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

The category of coalgebras over an additive comonad on a preadditive category is preadditive.

Equations

• CategoryTheory.Comonad.coalgebraPreadditive C U = { homGroup := fun (F G : CategoryTheory.Comonad.Coalgebra U) => AddCommGroup.mk ⋯, add_comp := ⋯, comp_add := ⋯ }

instance CategoryTheory.Comonad.forget_additive (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (U : CategoryTheory.Comonad C) [CategoryTheory.Functor.Additive U.toFunctor] : CategoryTheory.Functor.Additive (CategoryTheory.Comonad.forget U)

Equations

• ⋯ = ⋯