# 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.

## 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 of this typeclass
Instances of other typeclasses for category_theory.preadditive
@[simp]
theorem category_theory.preadditive.add_comp {C : Type u} [self : category_theory.preadditive C] (P Q R : C) (f f' : P Q) (g : Q R) :
(f + f') g = f g + f' g
@[simp]
theorem category_theory.preadditive.comp_add {C : Type u} [self : category_theory.preadditive C] (P Q R : C) (f : P Q) (g g' : Q R) :
f (g + g') = f g + f g'
@[simp]
theorem category_theory.preadditive.add_comp_assoc {C : Type u} [self : category_theory.preadditive C] (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
theorem category_theory.preadditive.comp_add_assoc {C : Type u} [self : category_theory.preadditive C] (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'
@[protected, instance]
def category_theory.preadditive.induced_category.category {C : Type u} {D : Type u'} (F : D → C) :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def category_theory.preadditive.left_comp {C : Type u} {P Q : C} (R : C) (f : 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} (g : Q R) :
(P Q) →+ (P R)

Composition by a fixed right argument as a group homomorphism

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

Composition as a bilinear 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.nsmul_comp {C : Type u} {P Q R : C} (f : P Q) (g : Q R) (n : ) :
(n f) g = n f g
theorem category_theory.preadditive.comp_nsmul {C : Type u} {P Q R : C} (f : P Q) (g : Q R) (n : ) :
f (n g) = n f g
theorem category_theory.preadditive.zsmul_comp {C : Type u} {P Q R : C} (f : P Q) (g : Q R) (n : ) :
(n f) g = n f g
theorem category_theory.preadditive.comp_zsmul {C : Type u} {P Q R : C} (f : P Q) (g : Q R) (n : ) :
f (n g) = n f g
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' = s.sum (λ (j : J), 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 s.sum (λ (j : J), g j) = s.sum (λ (j : J), 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) :
s.sum (λ (j : J), f j) g = s.sum (λ (j : J), 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' = s.sum (λ (j : J), f j g) f'
@[protected, instance]
def category_theory.preadditive.has_neg.neg.category_theory.epi {C : Type u} {P Q : C} {f : P Q}  :
@[protected, instance]
def category_theory.preadditive.has_neg.neg.category_theory.mono {C : Type u} {P Q : C} {f : P Q}  :
@[protected, instance]
def category_theory.preadditive.module_End_right {C : Type u} {X Y : C} :
(X Y)
Equations
theorem category_theory.preadditive.mono_of_cancel_zero {C : Type u} {Q R : C} (f : Q R) (h : ∀ {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} (w : = 0) :
theorem category_theory.preadditive.epi_of_cancel_zero {C : Type u} {P Q : C} (f : P Q) (h : ∀ {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}  :
@[simp]
theorem category_theory.preadditive.is_iso.comp_left_eq_zero {C : Type u} {P Q R : C} (f : P Q) (g : Q R)  :
f g = 0 g = 0
@[simp]
theorem category_theory.preadditive.is_iso.comp_right_eq_zero {C : Type u} {P Q R : C} (f : P Q) (g : Q R)  :
f g = 0 f = 0
theorem category_theory.preadditive.mono_of_kernel_iso_zero {C : Type u} {X Y : C} {f : X Y} (w : 0) :
theorem category_theory.preadditive.epi_of_cokernel_iso_zero {C : Type u} {X Y : C} {f : X Y} (w : 0) :
def category_theory.preadditive.fork_of_kernel_fork {C : Type u} {X Y : C} {f g : X Y} (c : category_theory.limits.kernel_fork (f - g)) :

Map a kernel cone on the difference of two morphisms to the equalizer fork.

Equations
def category_theory.preadditive.kernel_fork_of_fork {C : Type u} {X Y : C} {f g : X Y} (c : g) :

Map any equalizer fork to a cone on the difference of the two morphisms.

Equations
@[simp]
theorem category_theory.preadditive.kernel_fork_of_fork_ι {C : Type u} {X Y : C} {f g : X Y} (c : g) :
@[simp]
theorem category_theory.preadditive.kernel_fork_of_fork_of_ι {C : Type u} {X Y : C} {f g : X Y} {P : C} (ι : P X) (w : ι f = ι g) :

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

Equations
@[simp]
theorem category_theory.preadditive.is_limit_fork_of_kernel_fork_lift {C : Type u} {X Y : C} {f g : X Y} {c : category_theory.limits.kernel_fork (f - g)} (s : g) :
def category_theory.preadditive.is_limit_kernel_fork_of_fork {C : Type u} {X Y : C} {f g : X Y} {c : g}  :

An equalizer of f and g is a kernel of f - g.

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

A preadditive category has an equalizer for f and g if it has a kernel for f - g.

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

A preadditive category has a kernel for f - g if it has an equalizer for f and g.

Map a cokernel cocone on the difference of two morphisms to the coequalizer cofork.

Equations
def category_theory.preadditive.cokernel_cofork_of_cofork {C : Type u} {X Y : C} {f g : X Y} (c : g) :

Map any coequalizer cofork to a cocone on the difference of the two morphisms.

Equations
@[simp]
theorem category_theory.preadditive.cokernel_cofork_of_cofork_π {C : Type u} {X Y : C} {f g : X Y} (c : g) :
@[simp]
theorem category_theory.preadditive.cokernel_cofork_of_cofork_of_π {C : Type u} {X Y : C} {f g : X Y} {P : C} (π : Y P) (w : f π = g π) :

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

Equations
@[simp]
def category_theory.preadditive.is_colimit_cokernel_cofork_of_cofork {C : Type u} {X Y : C} {f g : X Y} {c : g}  :

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

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

A preadditive category has a coequalizer for f and g if it has a cokernel for f - g.

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

A preadditive category has a cokernel for f - g if it has a coequalizer for f and g.

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

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