Documentation

Mathlib.CategoryTheory.Preadditive.EndoFunctor

Preadditive structure on algebras over a monad #

If C is a preadditive category and F is an additive endofunctor on C then Algebra F is also preadditive. Dually, the category Coalgebra F is also preadditive.

source
@[instance_reducible]
instance CategoryTheory.Endofunctor.algebraPreadditive (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] :
Preadditive (Algebra F)

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_add_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Algebra F) (α β : A₁ ⟶ A₂) :
(α + β).f = α.f + β.f
source
@[simp]
theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zsmul_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Algebra F) (r : ℤ) (α : A₁ ⟶ A₂) :
(r • α).f = r • α.f
source
@[simp]
theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zero_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Algebra F) :
Algebra.Hom.f 0 = 0
source
@[simp]
theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_neg_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Algebra F) (α : A₁ ⟶ A₂) :
(-α).f = -α.f
source
@[simp]
theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_sub_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Algebra F) (α β : A₁ ⟶ A₂) :
(α - β).f = α.f - β.f
source
@[simp]
theorem CategoryTheory.Endofunctor.algebraPreadditive_homGroup_nsmul_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Algebra F) (n : ℕ) (α : A₁ ⟶ A₂) :
(n • α).f = n • α.f
source
instance CategoryTheory.Algebra.forget_additive (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] :
(Endofunctor.Algebra.forget F).Additive
source
@[instance_reducible]
instance CategoryTheory.Endofunctor.coalgebraPreadditive (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] :
Preadditive (Coalgebra F)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_neg_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Coalgebra F) (α : A₁ ⟶ A₂) :
(-α).f = -α.f
source
@[simp]
theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_sub_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Coalgebra F) (α β : A₁ ⟶ A₂) :
(α - β).f = α.f - β.f
source
@[simp]
theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zsmul_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Coalgebra F) (r : ℤ) (α : A₁ ⟶ A₂) :
(r • α).f = r • α.f
source
@[simp]
theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_add_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Coalgebra F) (α β : A₁ ⟶ A₂) :
(α + β).f = α.f + β.f
source
@[simp]
theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zero_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Coalgebra F) :
Coalgebra.Hom.f 0 = 0
source
@[simp]
theorem CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_nsmul_f (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] (A₁ A₂ : Coalgebra F) (n : ℕ) (α : A₁ ⟶ A₂) :
(n • α).f = n • α.f
source
instance CategoryTheory.Coalgebra.forget_additive (C : Type u₁) [Category.{v₁, u₁} C] [Preadditive C] (F : Functor C C) [F.Additive] :
(Endofunctor.Coalgebra.forget F).Additive