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)
[T.Additive]
(F : T.Algebra)
(G : T.Algebra)
(r : ℤ)
(α : F ⟶ G)
:
@[simp]
theorem
CategoryTheory.Monad.algebraPreadditive_homGroup_sub_f
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(T : CategoryTheory.Monad C)
[T.Additive]
(F : T.Algebra)
(G : T.Algebra)
(α : F ⟶ G)
(β : F ⟶ G)
:
@[simp]
theorem
CategoryTheory.Monad.algebraPreadditive_homGroup_neg_f
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(T : CategoryTheory.Monad C)
[T.Additive]
(F : T.Algebra)
(G : T.Algebra)
(α : F ⟶ G)
:
@[simp]
theorem
CategoryTheory.Monad.algebraPreadditive_homGroup_add_f
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(T : CategoryTheory.Monad C)
[T.Additive]
(F : T.Algebra)
(G : T.Algebra)
(α : F ⟶ G)
(β : F ⟶ G)
:
@[simp]
theorem
CategoryTheory.Monad.algebraPreadditive_homGroup_zero_f
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(T : CategoryTheory.Monad C)
[T.Additive]
(F : T.Algebra)
(G : T.Algebra)
:
@[simp]
theorem
CategoryTheory.Monad.algebraPreadditive_homGroup_nsmul_f
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(T : CategoryTheory.Monad C)
[T.Additive]
(F : T.Algebra)
(G : T.Algebra)
(n : ℕ)
(α : F ⟶ G)
:
instance
CategoryTheory.Monad.algebraPreadditive
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(T : CategoryTheory.Monad C)
[T.Additive]
:
CategoryTheory.Preadditive T.Algebra
The category of algebras over an additive monad on a preadditive category is preadditive.
Equations
- CategoryTheory.Monad.algebraPreadditive C T = { homGroup := fun (F G : T.Algebra) => 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)
[T.Additive]
:
T.forget.Additive
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Comonad.coalgebraPreadditive_homGroup_neg_f
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(U : CategoryTheory.Comonad C)
[U.Additive]
(F : U.Coalgebra)
(G : U.Coalgebra)
(α : F ⟶ G)
:
@[simp]
theorem
CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zsmul_f
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(U : CategoryTheory.Comonad C)
[U.Additive]
(F : U.Coalgebra)
(G : U.Coalgebra)
(r : ℤ)
(α : F ⟶ G)
:
@[simp]
theorem
CategoryTheory.Comonad.coalgebraPreadditive_homGroup_sub_f
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(U : CategoryTheory.Comonad C)
[U.Additive]
(F : U.Coalgebra)
(G : U.Coalgebra)
(α : F ⟶ G)
(β : F ⟶ G)
:
@[simp]
theorem
CategoryTheory.Comonad.coalgebraPreadditive_homGroup_nsmul_f
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(U : CategoryTheory.Comonad C)
[U.Additive]
(F : U.Coalgebra)
(G : U.Coalgebra)
(n : ℕ)
(α : F ⟶ G)
:
@[simp]
theorem
CategoryTheory.Comonad.coalgebraPreadditive_homGroup_add_f
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(U : CategoryTheory.Comonad C)
[U.Additive]
(F : U.Coalgebra)
(G : U.Coalgebra)
(α : F ⟶ G)
(β : F ⟶ G)
:
@[simp]
theorem
CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zero_f
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(U : CategoryTheory.Comonad C)
[U.Additive]
(F : U.Coalgebra)
(G : U.Coalgebra)
:
instance
CategoryTheory.Comonad.coalgebraPreadditive
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
(U : CategoryTheory.Comonad C)
[U.Additive]
:
CategoryTheory.Preadditive U.Coalgebra
The category of coalgebras over an additive comonad on a preadditive category is preadditive.
Equations
- CategoryTheory.Comonad.coalgebraPreadditive C U = { homGroup := fun (F G : U.Coalgebra) => 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)
[U.Additive]
:
U.forget.Additive
Equations
- ⋯ = ⋯