# The quotient category is preadditive #

If an equivalence relation r : HomRel C on the morphisms of a preadditive category is compatible with the addition, then the quotient category Quotient r is also preadditive.

def CategoryTheory.Quotient.Preadditive.add {C : Type u_1} [] (r : ) (hr : X Y : C⦄ → (f₁ f₂ g₁ g₂ : X Y) → r X Y f₁ f₂r X Y g₁ g₂r X Y (f₁ + g₁) (f₂ + g₂)) {X : } {Y : } (f : X Y) (g : X Y) :
X Y

The addition on the morphisms in the category Quotient r when r is compatible with the addition.

Instances For
def CategoryTheory.Quotient.Preadditive.neg {C : Type u_1} [] (r : ) (hr : X Y : C⦄ → (f₁ f₂ g₁ g₂ : X Y) → r X Y f₁ f₂r X Y g₁ g₂r X Y (f₁ + g₁) (f₂ + g₂)) {X : } {Y : } (f : X Y) :
X Y

The negation on the morphisms in the category Quotient r when r is compatible with the addition.

Instances For
def CategoryTheory.Quotient.preadditive {C : Type u_1} [] (r : ) (hr : X Y : C⦄ → (f₁ f₂ g₁ g₂ : X Y) → r X Y f₁ f₂r X Y g₁ g₂r X Y (f₁ + g₁) (f₂ + g₂)) :

The preadditive structure on the category Quotient r when r is compatible with the addition.

Instances For
theorem CategoryTheory.Quotient.functor_additive {C : Type u_1} [] (r : ) (hr : X Y : C⦄ → (f₁ f₂ g₁ g₂ : X Y) → r X Y f₁ f₂r X Y g₁ g₂r X Y (f₁ + g₁) (f₂ + g₂)) :