category_theory.preadditive.endo_functor

@[protected, instance]

def category_theory.endofunctor.algebra_preadditive (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] :

category_theory.preadditive (category_theory.endofunctor.algebra F)

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

Equations

category_theory.endofunctor.algebra_preadditive C F = {hom_group := λ (A₁ A₂ : category_theory.endofunctor.algebra F), {add := λ (α β : A₁ ⟶ A₂), {f := α.f + β.f, h' := _}, add_assoc := _, zero := {f := 0, h' := _}, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (α : A₁ ⟶ A₂), {f := n • α.f, h' := _}, nsmul_zero' := _, nsmul_succ' := _, neg := λ (α : A₁ ⟶ A₂), {f := -α.f, h' := _}, sub := λ (α β : A₁ ⟶ A₂), {f := α.f - β.f, h' := _}, sub_eq_add_neg := _, zsmul := λ (r : ℤ) (α : A₁ ⟶ A₂), {f := r • α.f, h' := _}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}, add_comp' := _, comp_add' := _}

source

@[simp]

theorem category_theory.endofunctor.algebra_preadditive_hom_group_neg_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] (A₁ A₂ : category_theory.endofunctor.algebra F) (α : A₁ ⟶ A₂) :

(-α).f = -α.f

source

@[simp]

theorem category_theory.endofunctor.algebra_preadditive_hom_group_nsmul_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] (A₁ A₂ : category_theory.endofunctor.algebra F) (n : ℕ) (α : A₁ ⟶ A₂) :

(add_comm_group.nsmul n α).f = n • α.f

source

@[simp]

theorem category_theory.endofunctor.algebra_preadditive_hom_group_add_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] (A₁ A₂ : category_theory.endofunctor.algebra F) (α β : A₁ ⟶ A₂) :

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

source

@[simp]

theorem category_theory.endofunctor.algebra_preadditive_hom_group_zero_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] (A₁ A₂ : category_theory.endofunctor.algebra F) :

0.f = 0

source

@[simp]

theorem category_theory.endofunctor.algebra_preadditive_hom_group_sub_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] (A₁ A₂ : category_theory.endofunctor.algebra F) (α β : A₁ ⟶ A₂) :

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

source

@[simp]

theorem category_theory.endofunctor.algebra_preadditive_hom_group_zsmul_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] (A₁ A₂ : category_theory.endofunctor.algebra F) (r : ℤ) (α : A₁ ⟶ A₂) :

(add_comm_group.zsmul r α).f = r • α.f

source

@[protected, instance]

def category_theory.algebra.forget_additive (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] :

(category_theory.endofunctor.algebra.forget F).additive

source

@[simp]

theorem category_theory.endofunctor.coalgebra_preadditive_hom_group_neg_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] (A₁ A₂ : category_theory.endofunctor.coalgebra F) (α : A₁ ⟶ A₂) :

(-α).f = -α.f

source

@[simp]

theorem category_theory.endofunctor.coalgebra_preadditive_hom_group_add_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] (A₁ A₂ : category_theory.endofunctor.coalgebra F) (α β : A₁ ⟶ A₂) :

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

source

@[simp]

theorem category_theory.endofunctor.coalgebra_preadditive_hom_group_sub_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] (A₁ A₂ : category_theory.endofunctor.coalgebra F) (α β : A₁ ⟶ A₂) :

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

source

@[simp]

theorem category_theory.endofunctor.coalgebra_preadditive_hom_group_nsmul_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] (A₁ A₂ : category_theory.endofunctor.coalgebra F) (n : ℕ) (α : A₁ ⟶ A₂) :

(add_comm_group.nsmul n α).f = n • α.f

source

@[simp]

theorem category_theory.endofunctor.coalgebra_preadditive_hom_group_zsmul_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] (A₁ A₂ : category_theory.endofunctor.coalgebra F) (r : ℤ) (α : A₁ ⟶ A₂) :

(add_comm_group.zsmul r α).f = r • α.f

source

@[simp]

theorem category_theory.endofunctor.coalgebra_preadditive_hom_group_zero_f (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] (A₁ A₂ : category_theory.endofunctor.coalgebra F) :

0.f = 0

source

@[protected, instance]

def category_theory.endofunctor.coalgebra_preadditive (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] :

category_theory.preadditive (category_theory.endofunctor.coalgebra F)

Equations

category_theory.endofunctor.coalgebra_preadditive C F = {hom_group := λ (A₁ A₂ : category_theory.endofunctor.coalgebra F), {add := λ (α β : A₁ ⟶ A₂), {f := α.f + β.f, h' := _}, add_assoc := _, zero := {f := 0, h' := _}, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (α : A₁ ⟶ A₂), {f := n • α.f, h' := _}, nsmul_zero' := _, nsmul_succ' := _, neg := λ (α : A₁ ⟶ A₂), {f := -α.f, h' := _}, sub := λ (α β : A₁ ⟶ A₂), {f := α.f - β.f, h' := _}, sub_eq_add_neg := _, zsmul := λ (r : ℤ) (α : A₁ ⟶ A₂), {f := r • α.f, h' := _}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}, add_comp' := _, comp_add' := _}

source

@[protected, instance]

def category_theory.coalgebra.forget_additive (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (F : C ⥤ C) [F.additive] :

(category_theory.endofunctor.coalgebra.forget F).additive

mathlib documentation

Preadditive structure on algebras over a monad #