Preadditive structure on algebras over a monad #
If C
is a preadditive categories 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
category_theory.monad.algebra_preadditive_hom_group_zero_f
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(T : category_theory.monad C)
[↑T.additive]
(F G : T.algebra) :
@[simp]
theorem
category_theory.monad.algebra_preadditive_hom_group_neg_f
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(T : category_theory.monad C)
[↑T.additive]
(F G : T.algebra)
(α : F ⟶ G) :
@[simp]
theorem
category_theory.monad.algebra_preadditive_hom_group_zsmul_f
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(T : category_theory.monad C)
[↑T.additive]
(F G : T.algebra)
(r : ℤ)
(α : F ⟶ G) :
(add_comm_group.zsmul r α).f = r • α.f
@[simp]
theorem
category_theory.monad.algebra_preadditive_hom_group_nsmul_f
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(T : category_theory.monad C)
[↑T.additive]
(F G : T.algebra)
(n : ℕ)
(α : F ⟶ G) :
(add_comm_group.nsmul n α).f = n • α.f
@[simp]
theorem
category_theory.monad.algebra_preadditive_hom_group_sub_f
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(T : category_theory.monad C)
[↑T.additive]
(F G : T.algebra)
(α β : F ⟶ G) :
@[protected, instance]
def
category_theory.monad.algebra_preadditive
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(T : category_theory.monad C)
[↑T.additive] :
The category of algebras over an additive monad on a preadditive category is preadditive.
Equations
- category_theory.monad.algebra_preadditive C T = {hom_group := λ (F G : T.algebra), {add := λ (α β : F ⟶ G), {f := α.f + β.f, h' := _}, add_assoc := _, zero := {f := 0, h' := _}, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (α : F ⟶ G), {f := n • α.f, h' := _}, nsmul_zero' := _, nsmul_succ' := _, neg := λ (α : F ⟶ G), {f := -α.f, h' := _}, sub := λ (α β : F ⟶ G), {f := α.f - β.f, h' := _}, sub_eq_add_neg := _, zsmul := λ (r : ℤ) (α : F ⟶ G), {f := r • α.f, h' := _}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}, add_comp' := _, comp_add' := _}
@[simp]
theorem
category_theory.monad.algebra_preadditive_hom_group_add_f
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(T : category_theory.monad C)
[↑T.additive]
(F G : T.algebra)
(α β : F ⟶ G) :
@[protected, instance]
def
category_theory.monad.forget_additive
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(T : category_theory.monad C)
[↑T.additive] :
@[simp]
theorem
category_theory.comonad.coalgebra_preadditive_hom_group_neg_f
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(U : category_theory.comonad C)
[↑U.additive]
(F G : U.coalgebra)
(α : F ⟶ G) :
@[protected, instance]
def
category_theory.comonad.coalgebra_preadditive
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(U : category_theory.comonad C)
[↑U.additive] :
The category of coalgebras over an additive comonad on a preadditive category is preadditive.
Equations
- category_theory.comonad.coalgebra_preadditive C U = {hom_group := λ (F G : U.coalgebra), {add := λ (α β : F ⟶ G), {f := α.f + β.f, h' := _}, add_assoc := _, zero := {f := 0, h' := _}, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (α : F ⟶ G), {f := n • α.f, h' := _}, nsmul_zero' := _, nsmul_succ' := _, neg := λ (α : F ⟶ G), {f := -α.f, h' := _}, sub := λ (α β : F ⟶ G), {f := α.f - β.f, h' := _}, sub_eq_add_neg := _, zsmul := λ (r : ℤ) (α : F ⟶ G), {f := r • α.f, h' := _}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}, add_comp' := _, comp_add' := _}
@[simp]
theorem
category_theory.comonad.coalgebra_preadditive_hom_group_zsmul_f
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(U : category_theory.comonad C)
[↑U.additive]
(F G : U.coalgebra)
(r : ℤ)
(α : F ⟶ G) :
(add_comm_group.zsmul r α).f = r • α.f
@[simp]
theorem
category_theory.comonad.coalgebra_preadditive_hom_group_sub_f
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(U : category_theory.comonad C)
[↑U.additive]
(F G : U.coalgebra)
(α β : F ⟶ G) :
@[simp]
theorem
category_theory.comonad.coalgebra_preadditive_hom_group_add_f
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(U : category_theory.comonad C)
[↑U.additive]
(F G : U.coalgebra)
(α β : F ⟶ G) :
@[simp]
theorem
category_theory.comonad.coalgebra_preadditive_hom_group_zero_f
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(U : category_theory.comonad C)
[↑U.additive]
(F G : U.coalgebra) :
@[simp]
theorem
category_theory.comonad.coalgebra_preadditive_hom_group_nsmul_f
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(U : category_theory.comonad C)
[↑U.additive]
(F G : U.coalgebra)
(n : ℕ)
(α : F ⟶ G) :
(add_comm_group.nsmul n α).f = n • α.f
@[protected, instance]
def
category_theory.comonad.forget_additive
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(U : category_theory.comonad C)
[↑U.additive] :