Documentation

Mathlib.CategoryTheory.Preadditive.EilenbergMoore

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.

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

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

Equations
@[simp]
theorem CategoryTheory.Monad.algebraPreadditive_homGroup_nsmul_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (T : Monad C) [T.Additive] (F G : T.Algebra) (n : ) (α : F G) :
(n α).f = n α.f
@[simp]
theorem CategoryTheory.Monad.algebraPreadditive_homGroup_sub_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (T : Monad C) [T.Additive] (F G : T.Algebra) (α β : F G) :
(α - β).f = α.f - β.f
@[simp]
theorem CategoryTheory.Monad.algebraPreadditive_homGroup_zero_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (T : Monad C) [T.Additive] (F G : T.Algebra) :
@[simp]
theorem CategoryTheory.Monad.algebraPreadditive_homGroup_neg_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (T : Monad C) [T.Additive] (F G : T.Algebra) (α : F G) :
(-α).f = -α.f
@[simp]
theorem CategoryTheory.Monad.algebraPreadditive_homGroup_zsmul_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (T : Monad C) [T.Additive] (F G : T.Algebra) (r : ) (α : F G) :
(r α).f = r α.f
@[simp]
theorem CategoryTheory.Monad.algebraPreadditive_homGroup_add_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (T : Monad C) [T.Additive] (F G : T.Algebra) (α β : F G) :
(α + β).f = α.f + β.f
instance CategoryTheory.Monad.forget_additive (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (T : Monad C) [T.Additive] :
T.forget.Additive
instance CategoryTheory.Comonad.coalgebraPreadditive (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (U : Comonad C) [U.Additive] :
Preadditive U.Coalgebra

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

Equations
@[simp]
theorem CategoryTheory.Comonad.coalgebraPreadditive_homGroup_neg_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (U : Comonad C) [U.Additive] (F G : U.Coalgebra) (α : F G) :
(-α).f = -α.f
@[simp]
theorem CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zero_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (U : Comonad C) [U.Additive] (F G : U.Coalgebra) :
@[simp]
theorem CategoryTheory.Comonad.coalgebraPreadditive_homGroup_sub_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (U : Comonad C) [U.Additive] (F G : U.Coalgebra) (α β : F G) :
(α - β).f = α.f - β.f
@[simp]
theorem CategoryTheory.Comonad.coalgebraPreadditive_homGroup_nsmul_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (U : Comonad C) [U.Additive] (F G : U.Coalgebra) (n : ) (α : F G) :
(n α).f = n α.f
@[simp]
theorem CategoryTheory.Comonad.coalgebraPreadditive_homGroup_add_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (U : Comonad C) [U.Additive] (F G : U.Coalgebra) (α β : F G) :
(α + β).f = α.f + β.f
@[simp]
theorem CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zsmul_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (U : Comonad C) [U.Additive] (F G : U.Coalgebra) (r : ) (α : F G) :
(r α).f = r α.f
instance CategoryTheory.Comonad.forget_additive (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (U : Comonad C) [U.Additive] :
U.forget.Additive