Preadditive structure on functor categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
If C and D are categories and D is preadditive,
then C ⥤ D is also preadditive.
@[protected, instance]
def
category_theory.functor_category_preadditive
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
[category_theory.preadditive D] :
category_theory.preadditive (C ⥤ D)
Equations
- category_theory.functor_category_preadditive = {hom_group := λ (F G : C ⥤ D), {add := λ (α β : F ⟶ G), {app := λ (X : C), α.app X + β.app X, naturality' := _}, add_assoc := _, zero := {app := λ (X : C), 0, naturality' := _}, zero_add := _, add_zero := _, nsmul := add_group.nsmul._default {app := λ (X : C), 0, naturality' := _} (λ (α β : F ⟶ G), {app := λ (X : C), α.app X + β.app X, naturality' := _}) _ _, nsmul_zero' := _, nsmul_succ' := _, neg := λ (α : F ⟶ G), {app := λ (X : C), -α.app X, naturality' := _}, sub := λ (α β : F ⟶ G), {app := λ (X : C), α.app X - β.app X, naturality' := _}, sub_eq_add_neg := _, zsmul := add_group.zsmul._default (λ (α β : F ⟶ G), {app := λ (X : C), α.app X + β.app X, naturality' := _}) _ {app := λ (X : C), 0, naturality' := _} _ _ (add_group.nsmul._default {app := λ (X : C), 0, naturality' := _} (λ (α β : F ⟶ G), {app := λ (X : C), α.app X + β.app X, naturality' := _}) _ _) _ _ (λ (α : F ⟶ G), {app := λ (X : C), -α.app X, naturality' := _}), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}, add_comp' := _, comp_add' := _}
def
category_theory.nat_trans.app_hom
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
[category_theory.preadditive D]
{F G : C ⥤ D}
(X : C) :
Application of a natural transformation at a fixed object, as group homomorphism
@[simp]
theorem
category_theory.nat_trans.app_hom_apply
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
[category_theory.preadditive D]
{F G : C ⥤ D}
(X : C)
(α : F ⟶ G) :
⇑(category_theory.nat_trans.app_hom X) α = α.app X
@[simp]
theorem
category_theory.nat_trans.app_zero
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
[category_theory.preadditive D]
{F G : C ⥤ D}
(X : C) :
@[simp]
theorem
category_theory.nat_trans.app_add
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
[category_theory.preadditive D]
{F G : C ⥤ D}
(X : C)
(α β : F ⟶ G) :
@[simp]
theorem
category_theory.nat_trans.app_sub
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
[category_theory.preadditive D]
{F G : C ⥤ D}
(X : C)
(α β : F ⟶ G) :
@[simp]
theorem
category_theory.nat_trans.app_neg
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
[category_theory.preadditive D]
{F G : C ⥤ D}
(X : C)
(α : F ⟶ G) :
@[simp]
theorem
category_theory.nat_trans.app_nsmul
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
[category_theory.preadditive D]
{F G : C ⥤ D}
(X : C)
(α : F ⟶ G)
(n : ℕ) :
@[simp]
theorem
category_theory.nat_trans.app_zsmul
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
[category_theory.preadditive D]
{F G : C ⥤ D}
(X : C)
(α : F ⟶ G)
(n : ℤ) :
@[simp]
theorem
category_theory.nat_trans.app_sum
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
[category_theory.preadditive D]
{F G : C ⥤ D}
{ι : Type u_5}
(s : finset ι)
(X : C)
(α : ι → (F ⟶ G)) :