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 F is an additive endofunctor on C then algebra F is
also preadditive. Dually, the category coalgebra F is also preadditive.
@[protected, instance]
def
category_theory.endofunctor.algebra_preadditive
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(F : C ⥤ C)
[F.additive] :
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' := _}
@[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₂) :
@[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
@[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₂) :
@[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) :
@[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₂) :
@[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
@[protected, instance]
def
category_theory.algebra.forget_additive
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(F : C ⥤ C)
[F.additive] :
@[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₂) :
@[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₂) :
@[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₂) :
@[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
@[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
@[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) :
@[protected, instance]
def
category_theory.endofunctor.coalgebra_preadditive
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(F : C ⥤ C)
[F.additive] :
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' := _}
@[protected, instance]
def
category_theory.coalgebra.forget_additive
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(F : C ⥤ C)
[F.additive] :