# mathlibdocumentation

A preadditive category is a category in which X ⟶ Y is an abelian group in such a way that composition of morphisms is linear in both variables.

This file contains a definition of preadditive category that directly encodes the definition given above. The definition could also be phrased as follows: A preadditive category is a category enriched over the category of Abelian groups. Once the general framework to state this in Lean is available, the contents of this file should become obsolete.

## Main results

• Definition of preadditive categories and basic properties
• In a preadditive category, f : Q ⟶ R is mono if and only if g ≫ f = 0 → g = 0 for all composable g.
• A preadditive category with kernels has equalizers.

## Implementation notes

The simp normal form for negation and composition is to push negations as far as possible to the outside. For example, f ≫ (-g) and (-f) ≫ g both become -(f ≫ g), and (-f) ≫ (-g) is simplified to f ≫ g.

## References

• [F. Borceux, Handbook of Categorical Algebra 2][borceux-vol2]

## Tags

@[class]
structure category_theory.preadditive (C : Type u)  :
Type (max u v)
• hom_group : (Π (P Q : C), add_comm_group (P Q)) . "apply_instance"
• add_comp' : (∀ (P Q R : C) (f f' : P Q) (g : Q R), (f + f') g = f g + f' g) . "obviously"
• comp_add' : (∀ (P Q R : C) (f : P Q) (g g' : Q R), f (g + g') = f g + f g') . "obviously"

A category is called preadditive if P ⟶ Q is an abelian group such that composition is linear in both variables.

Instances
def category_theory.preadditive.left_comp {C : Type u} {P Q : C} (R : C) :
(P Q)(Q R) →+ (P R)

Composition by a fixed left argument as a group homomorphism

Equations
def category_theory.preadditive.right_comp {C : Type u} (P : C) {Q R : C} :
(Q R)(P Q) →+ (P R)

Composition by a fixed right argument as a group homomorphism

Equations
@[simp]
theorem category_theory.preadditive.sub_comp_assoc {C : Type u} {P Q R : C} (f f' : P Q) (g : Q R) {X' : C} (f'_1 : R X') :
(f - f') g f'_1 = (f g - f' g) f'_1

@[simp]
theorem category_theory.preadditive.sub_comp {C : Type u} {P Q R : C} (f f' : P Q) (g : Q R) :
(f - f') g = f g - f' g

@[simp]
theorem category_theory.preadditive.comp_sub {C : Type u} {P Q R : C} (f : P Q) (g g' : Q R) :
f (g - g') = f g - f g'

theorem category_theory.preadditive.comp_sub_assoc {C : Type u} {P Q R : C} (f : P Q) (g g' : Q R) {X' : C} (f' : R X') :
f (g - g') f' = (f g - f g') f'

@[simp]
theorem category_theory.preadditive.neg_comp_assoc {C : Type u} {P Q R : C} (f : P Q) (g : Q R) {X' : C} (f' : R X') :
(-f) g f' = (-f g) f'

@[simp]
theorem category_theory.preadditive.neg_comp {C : Type u} {P Q R : C} (f : P Q) (g : Q R) :
(-f) g = -f g

theorem category_theory.preadditive.comp_neg_assoc {C : Type u} {P Q R : C} (f : P Q) (g : Q R) {X' : C} (f' : R X') :
f (-g) f' = (-f g) f'

@[simp]
theorem category_theory.preadditive.comp_neg {C : Type u} {P Q R : C} (f : P Q) (g : Q R) :
f -g = -f g

theorem category_theory.preadditive.neg_comp_neg {C : Type u} {P Q R : C} (f : P Q) (g : Q R) :
(-f) -g = f g

theorem category_theory.preadditive.neg_comp_neg_assoc {C : Type u} {P Q R : C} (f : P Q) (g : Q R) {X' : C} (f' : R X') :
(-f) (-g) f' = f g f'

theorem category_theory.preadditive.comp_sum_assoc {C : Type u} {P Q R : C} {J : Type u_1} {s : finset J} (f : P Q) (g : J → (Q R)) {X' : C} (f' : R X') :
f s.sum g f' = (∑ (j : J) in s, f g j) f'

theorem category_theory.preadditive.comp_sum {C : Type u} {P Q R : C} {J : Type u_1} {s : finset J} (f : P Q) (g : J → (Q R)) :
f ∑ (j : J) in s, g j = ∑ (j : J) in s, f g j

theorem category_theory.preadditive.sum_comp {C : Type u} {P Q R : C} {J : Type u_1} {s : finset J} (f : J → (P Q)) (g : Q R) :
(∑ (j : J) in s, f j) g = ∑ (j : J) in s, f j g

theorem category_theory.preadditive.sum_comp_assoc {C : Type u} {P Q R : C} {J : Type u_1} {s : finset J} (f : J → (P Q)) (g : Q R) {X' : C} (f' : R X') :
s.sum f g f' = (∑ (j : J) in s, f j g) f'

@[instance]
def category_theory.preadditive.category_theory.epi {C : Type u} {P Q : C} {f : P Q}  :

@[instance]
def category_theory.preadditive.category_theory.mono {C : Type u} {P Q : C} {f : P Q}  :

theorem category_theory.preadditive.mono_of_cancel_zero {C : Type u} {Q R : C} (f : Q R) :
(∀ {P : C} (g : P Q), g f = 0g = 0)

theorem category_theory.preadditive.mono_iff_cancel_zero {C : Type u} {Q R : C} (f : Q R) :
∀ (P : C) (g : P Q), g f = 0g = 0

theorem category_theory.preadditive.mono_of_kernel_zero {C : Type u} {X Y : C} {f : X Y}  :

theorem category_theory.preadditive.epi_of_cancel_zero {C : Type u} {P Q : C} (f : P Q) :
(∀ {R : C} (g : Q R), f g = 0g = 0)

theorem category_theory.preadditive.epi_iff_cancel_zero {C : Type u} {P Q : C} (f : P Q) :
∀ (R : C) (g : Q R), f g = 0g = 0

theorem category_theory.preadditive.epi_of_cokernel_zero {C : Type u} {X Y : C} (f : X Y)  :

theorem category_theory.preadditive.has_limit_parallel_pair {C : Type u} {X Y : C} (f g : X Y)  :

A kernel of f - g is an equalizer of f and g.

If a preadditive category has all kernels, then it also has all equalizers.

theorem category_theory.preadditive.has_colimit_parallel_pair {C : Type u} {X Y : C} (f g : X Y)  :

A cokernel of f - g is a coequalizer of f and g.

If a preadditive category has all cokernels, then it also has all coequalizers.