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} [Category.{v_1, u_1} C] [Preadditive C] (r : HomRel C) [Congruence r] (hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)) {X Y : Quotient r} (f g : X ⟶ Y) : X ⟶ Y

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

Equations

• CategoryTheory.Quotient.Preadditive.add r hr f g = Quot.liftOn₂ f g (fun (a b : X.as ⟶ Y.as) => Quot.mk (CategoryTheory.HomRel.CompClosure r) (a + b)) ⋯ ⋯

def CategoryTheory.Quotient.Preadditive.neg {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (r : HomRel C) [Congruence r] (hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)) {X Y : Quotient r} (f : X ⟶ Y) : X ⟶ Y

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

Equations

• CategoryTheory.Quotient.Preadditive.neg r hr f = Quot.liftOn f (fun (a : X.as ⟶ Y.as) => Quot.mk (CategoryTheory.HomRel.CompClosure r) (-a)) ⋯

@[instance_reducible]

def CategoryTheory.Quotient.preadditive {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (r : HomRel C) [Congruence r] (hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)) : Preadditive (Quotient r)

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

Equations

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

theorem CategoryTheory.Quotient.functor_additive {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (r : HomRel C) [Congruence r] (hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)) : (functor r).Additive