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
- CategoryTheory.Quotient.Preadditive.add r hr f g = Quot.liftOn₂ f g (fun (a b : X.as ⟶ Y.as) => Quot.mk (CategoryTheory.Quotient.CompClosure r) (a + b)) ⋯ ⋯
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
- CategoryTheory.Quotient.Preadditive.neg r hr f = Quot.liftOn f (fun (a : X.as ⟶ Y.as) => Quot.mk (CategoryTheory.Quotient.CompClosure r) (-a)) ⋯
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₂))
:
(CategoryTheory.Quotient.functor r).Additive