The comma category is preadditive

If we have additive functors L : A ⥤ T and R : B ⥤ T between preadditive categories, then there is a structure of preadditive category on Comma L R such that addition commutes with the left and right projections.

We then apply this to Arrow T for T a preadditive category.

Tags

comma, arrow, preadditive

@[implicit_reducible]

instance CategoryTheory.CommaMorphism.instAddHomComma {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} : Add (u ⟶ v)

Equations

• CategoryTheory.CommaMorphism.instAddHomComma L R = { add := fun (α β : u ⟶ v) => { left := α.left + β.left, right := α.right + β.right, w := ⋯ } }

@[simp]

theorem CategoryTheory.CommaMorphism.add_left {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} (α β : u ⟶ v) : (α + β).left = α.left + β.left

@[simp]

theorem CategoryTheory.CommaMorphism.add_right {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} (α β : u ⟶ v) : (α + β).right = α.right + β.right

@[implicit_reducible]

instance CategoryTheory.CommaMorphism.instSubHomComma {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} : Sub (u ⟶ v)

Equations

• CategoryTheory.CommaMorphism.instSubHomComma L R = { sub := fun (α β : u ⟶ v) => { left := α.left - β.left, right := α.right - β.right, w := ⋯ } }

@[simp]

theorem CategoryTheory.CommaMorphism.sub_left {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} (α β : u ⟶ v) : (α - β).left = α.left - β.left

@[simp]

theorem CategoryTheory.CommaMorphism.sub_right {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} (α β : u ⟶ v) : (α - β).right = α.right - β.right

@[implicit_reducible]

instance CategoryTheory.CommaMorphism.instZeroHomComma {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} : Zero (u ⟶ v)

Equations

• CategoryTheory.CommaMorphism.instZeroHomComma L R = { zero := { left := 0, right := 0, w := ⋯ } }

@[simp]

theorem CategoryTheory.CommaMorphism.zero_left {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} : left 0 = 0

@[simp]

theorem CategoryTheory.CommaMorphism.zero_right {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} : right 0 = 0

@[implicit_reducible]

instance CategoryTheory.CommaMorphism.instNegHomComma {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} : Neg (u ⟶ v)

Equations

• CategoryTheory.CommaMorphism.instNegHomComma L R = { neg := fun (α : u ⟶ v) => { left := -α.left, right := -α.right, w := ⋯ } }

@[simp]

theorem CategoryTheory.CommaMorphism.neg_left {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} (α : u ⟶ v) : (-α).left = -α.left

@[simp]

theorem CategoryTheory.CommaMorphism.neg_right {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} (α : u ⟶ v) : (-α).right = -α.right

@[implicit_reducible]

instance CategoryTheory.instAddCommGroupHomComma {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] {u v : Comma L R} : AddCommGroup (u ⟶ v)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CategoryTheory.instPreadditiveComma {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] : Preadditive (Comma L R)

If we have additive functors L : A ⥤ T and R : B ⥤ T between preadditive categories, then the category Comma L R is preadditive.

Equations

• CategoryTheory.instPreadditiveComma L R = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

instance CategoryTheory.instAdditiveCommaFst {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] : (Comma.fst L R).Additive

instance CategoryTheory.instAdditiveCommaSnd {A : Type u₁} [Category.{v₁, u₁} A] [Preadditive A] {B : Type u₂} [Category.{v₂, u₂} B] [Preadditive B] {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] (L : Functor A T) [L.Additive] (R : Functor B T) [R.Additive] : (Comma.snd L R).Additive

@[implicit_reducible]

instance CategoryTheory.instPreadditiveArrow {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] : Preadditive (Arrow T)

If a category T is preadditive, then so is its category of arrows.

Equations

• CategoryTheory.instPreadditiveArrow = { homGroup := CategoryTheory.instPreadditiveArrow._aux_1, add_comp := ⋯, comp_add := ⋯ }

instance CategoryTheory.instAdditiveArrowLeftFunc {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] : Arrow.leftFunc.Additive

instance CategoryTheory.instAdditiveArrowRightFunc {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] : Arrow.rightFunc.Additive

@[simp]

theorem CategoryTheory.Arrow.Hom.add_left {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] {u v : Arrow T} (α β : u ⟶ v) : left (α + β) = left α + left β

@[simp]

theorem CategoryTheory.Arrow.Hom.add_right {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] {u v : Arrow T} (α β : u ⟶ v) : right (α + β) = right α + right β

@[simp]

theorem CategoryTheory.Arrow.Hom.zero_left {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] {u v : Arrow T} : left 0 = 0

@[simp]

theorem CategoryTheory.Arrow.Hom.zero_right {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] {u v : Arrow T} : right 0 = 0

@[simp]

theorem CategoryTheory.Arrow.Hom.neg_left {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] {u v : Arrow T} (α : u ⟶ v) : left (-α) = -left α

@[simp]

theorem CategoryTheory.Arrow.Hom.neg_right {T : Type u₃} [Category.{v₃, u₃} T] [Preadditive T] {u v : Arrow T} (α : u ⟶ v) : right (-α) = -right α