Documentation

Mathlib.CategoryTheory.Quotient.Preadditive

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

Equations
Instances For
    def CategoryTheory.Quotient.Preadditive.neg {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (r : HomRel C) [CategoryTheory.Congruence r] (hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X Y), r f₁ f₂r g₁ g₂r (f₁ + g₁) (f₂ + g₂)) {X : CategoryTheory.Quotient r} {Y : CategoryTheory.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
    Instances For
      def CategoryTheory.Quotient.preadditive {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (r : HomRel C) [CategoryTheory.Congruence r] (hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X Y), r f₁ f₂r g₁ g₂r (f₁ + g₁) (f₂ + g₂)) :

      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.
      Instances For
        theorem CategoryTheory.Quotient.functor_additive {C : Type u_2} [CategoryTheory.Category.{u_1, u_2} C] [CategoryTheory.Preadditive C] (r : HomRel C) [CategoryTheory.Congruence r] (hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X Y), r f₁ f₂r g₁ g₂r (f₁ + g₁) (f₂ + g₂)) :