Preadditive structure on algebras over a monad #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

@[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) :

0.f = 0

source

@[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) :

(-α).f = -α.f

source

@[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

source

@[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

source

@[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) :

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

source

@[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] :

category_theory.preadditive T.algebra

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' := _}

source

@[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) :

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

source

@[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] :

T.forget.additive

source

@[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) :

(-α).f = -α.f

source

@[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] :

category_theory.preadditive U.coalgebra

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' := _}

source

@[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

source

@[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) :

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

source

@[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) :

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

source

@[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) :

0.f = 0

source

@[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

source

@[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] :

U.forget.additive