# Documentation

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 CategoryTheory.Preadditive (C : Type u) :
Type (max u v)

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

• homGroup : (P Q : C) → AddCommGroup (P Q)

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

• add_comp : ∀ (P Q R : C) (f f' : P Q) (g : Q R),

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

• comp_add : ∀ (P Q R : C) (f : P Q) (g g' : Q R),

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

Instances
@[simp]
theorem CategoryTheory.Preadditive.add_comp {C : Type u} [self : ] (P : C) (Q : C) (R : C) (f : P Q) (f' : P Q) (g : Q R) :

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

@[simp]
theorem CategoryTheory.Preadditive.comp_add {C : Type u} [self : ] (P : C) (Q : C) (R : C) (f : P Q) (g : Q R) (g' : Q R) :

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

theorem CategoryTheory.Preadditive.add_comp_assoc {C : Type u} [self : ] (P : C) (Q : C) (R : C) (f : P Q) (f' : P Q) (g : Q R) {Z : C} (h : R Z) :
theorem CategoryTheory.Preadditive.comp_add_assoc {C : Type u} [self : ] (P : C) (Q : C) (R : C) (f : P Q) (g : Q R) (g' : Q R) {Z : C} (h : R Z) :
instance CategoryTheory.Preadditive.inducedCategory {C : Type u} {D : Type u'} (F : DC) :
Equations
Equations
Equations
• = id inferInstance
def CategoryTheory.Preadditive.leftComp {C : Type u} {P : C} {Q : C} (R : C) (f : P Q) :
(Q R) →+ (P R)

Composition by a fixed left argument as a group homomorphism

Equations
Instances For
def CategoryTheory.Preadditive.rightComp {C : Type u} (P : C) {Q : C} {R : C} (g : Q R) :
(P Q) →+ (P R)

Composition by a fixed right argument as a group homomorphism

Equations
Instances For
def CategoryTheory.Preadditive.compHom {C : Type u} {P : C} {Q : C} {R : C} :
(P Q) →+ (Q R) →+ (P R)

Composition as a bilinear group homomorphism

Equations
Instances For
theorem CategoryTheory.Preadditive.sub_comp_assoc {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (f' : P Q) (g : Q R) {Z : C} (h : R Z) :
@[simp]
theorem CategoryTheory.Preadditive.sub_comp {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (f' : P Q) (g : Q R) :
theorem CategoryTheory.Preadditive.comp_sub_assoc {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) (g' : Q R) {Z : C} (h : R Z) :
@[simp]
theorem CategoryTheory.Preadditive.comp_sub {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) (g' : Q R) :
theorem CategoryTheory.Preadditive.neg_comp_assoc {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) {Z : C} (h : R Z) :
@[simp]
theorem CategoryTheory.Preadditive.neg_comp {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) :
theorem CategoryTheory.Preadditive.comp_neg_assoc {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) {Z : C} (h : R Z) :
@[simp]
theorem CategoryTheory.Preadditive.comp_neg {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) :
theorem CategoryTheory.Preadditive.neg_comp_neg_assoc {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) {Z : C} (h : R Z) :
theorem CategoryTheory.Preadditive.neg_comp_neg {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) :
theorem CategoryTheory.Preadditive.nsmul_comp {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) (n : ) :
theorem CategoryTheory.Preadditive.comp_nsmul {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) (n : ) :
theorem CategoryTheory.Preadditive.zsmul_comp {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) (n : ) :
theorem CategoryTheory.Preadditive.comp_zsmul {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) (n : ) :
theorem CategoryTheory.Preadditive.comp_sum_assoc {C : Type u} {P : C} {Q : C} {R : C} {J : Type u_1} (s : ) (f : P Q) (g : J(Q R)) {Z : C} (h : R Z) :
theorem CategoryTheory.Preadditive.comp_sum {C : Type u} {P : C} {Q : C} {R : C} {J : Type u_1} (s : ) (f : P Q) (g : J(Q R)) :
CategoryTheory.CategoryStruct.comp f (∑ js, g j) = js,
theorem CategoryTheory.Preadditive.sum_comp_assoc {C : Type u} {P : C} {Q : C} {R : C} {J : Type u_1} (s : ) (f : J(P Q)) (g : Q R) {Z : C} (h : R Z) :
theorem CategoryTheory.Preadditive.sum_comp {C : Type u} {P : C} {Q : C} {R : C} {J : Type u_1} (s : ) (f : J(P Q)) (g : Q R) :
CategoryTheory.CategoryStruct.comp (∑ js, f j) g = js,
instance CategoryTheory.Preadditive.instEpiNegHom {C : Type u} {P : C} {Q : C} {f : P Q} :
Equations
• =
instance CategoryTheory.Preadditive.instMonoNegHom {C : Type u} {P : C} {Q : C} {f : P Q} :
Equations
• =
@[instance 100]
Equations

Porting note: adding this before the ring instance allowed moduleEndRight to find the correct Monoid structure on End. Moved both down after preadditiveHasZeroMorphisms to make use of them

Equations
• CategoryTheory.Preadditive.instSemiringEnd = let __src := CategoryTheory.End.monoid; Semiring.mk Monoid.npow
instance CategoryTheory.Preadditive.instRingEnd {C : Type u} {X : C} :

Porting note: It looks like Ring's parent classes changed in Lean 4 so the previous instance needed modification. Was following my nose here.

Equations
• CategoryTheory.Preadditive.instRingEnd = let __src := inferInstance; let __src_1 := inferInstance; Ring.mk SubNegMonoid.zsmul
instance CategoryTheory.Preadditive.moduleEndRight {C : Type u} {X : C} {Y : C} :
Module (X Y)
Equations
theorem CategoryTheory.Preadditive.mono_of_cancel_zero {C : Type u} {Q : C} {R : C} (f : Q R) (h : ∀ {P : C} (g : P Q), g = 0) :
theorem CategoryTheory.Preadditive.mono_iff_cancel_zero {C : Type u} {Q : C} {R : C} (f : Q R) :
∀ (P : C) (g : P Q), g = 0
theorem CategoryTheory.Preadditive.mono_of_kernel_zero {C : Type u} {X : C} {Y : C} {f : X Y} (w : ) :
theorem CategoryTheory.Preadditive.mono_of_isZero_kernel' {C : Type u} {X : C} {Y : C} {f : X Y} (hc : ) (h : ) :
theorem CategoryTheory.Preadditive.mono_of_isZero_kernel {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Preadditive.epi_of_cancel_zero {C : Type u} {P : C} {Q : C} (f : P Q) (h : ∀ {R : C} (g : Q R), g = 0) :
theorem CategoryTheory.Preadditive.epi_iff_cancel_zero {C : Type u} {P : C} {Q : C} (f : P Q) :
∀ (R : C) (g : Q R), g = 0
theorem CategoryTheory.Preadditive.epi_of_cokernel_zero {C : Type u} {X : C} {Y : C} {f : X Y} (w : ) :
theorem CategoryTheory.Preadditive.epi_of_isZero_cokernel' {C : Type u} {X : C} {Y : C} {f : X Y} (hc : ) (h : ) :
theorem CategoryTheory.Preadditive.epi_of_isZero_cokernel {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.Preadditive.IsIso.comp_left_eq_zero {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) :
g = 0
@[simp]
theorem CategoryTheory.Preadditive.IsIso.comp_right_eq_zero {C : Type u} {P : C} {Q : C} {R : C} (f : P Q) (g : Q R) :
f = 0
theorem CategoryTheory.Preadditive.mono_of_kernel_iso_zero {C : Type u} {X : C} {Y : C} {f : X Y} (w : ) :
theorem CategoryTheory.Preadditive.epi_of_cokernel_iso_zero {C : Type u} {X : C} {Y : C} {f : X Y} (w : ) :
@[simp]
theorem CategoryTheory.Preadditive.forkOfKernelFork_pt {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} (c : ) :
= c.pt
def CategoryTheory.Preadditive.forkOfKernelFork {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} (c : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Preadditive.forkOfKernelFork_ι {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} (c : ) :
def CategoryTheory.Preadditive.kernelForkOfFork {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} (c : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Preadditive.kernelForkOfFork_ι {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} (c : ) :
@[simp]
theorem CategoryTheory.Preadditive.kernelForkOfFork_ofι {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} {P : C} (ι : P X) :
def CategoryTheory.Preadditive.isLimitForkOfKernelFork {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} {c : } :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} {c : } (s : ) :
def CategoryTheory.Preadditive.isLimitKernelForkOfFork {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} {c : } :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Preadditive.hasEqualizer_of_hasKernel {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) [] :

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

theorem CategoryTheory.Preadditive.hasKernel_of_hasEqualizer {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) :

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

@[simp]
theorem CategoryTheory.Preadditive.coforkOfCokernelCofork_pt {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} (c : ) :
def CategoryTheory.Preadditive.coforkOfCokernelCofork {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} (c : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Preadditive.coforkOfCokernelCofork_π {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} (c : ) :
def CategoryTheory.Preadditive.cokernelCoforkOfCofork {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} (c : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Preadditive.cokernelCoforkOfCofork_π {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} (c : ) :
@[simp]
theorem CategoryTheory.Preadditive.cokernelCoforkOfCofork_ofπ {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} {P : C} (π : Y P) :
def CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} {c : } :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} {c : } (s : ) :
def CategoryTheory.Preadditive.isColimitCokernelCoforkOfCofork {C : Type u} {X : C} {Y : C} {f : X Y} {g : X Y} {c : } :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Preadditive.hasCoequalizer_of_hasCokernel {C : Type u} {X : C} {Y : C} (f : X Y) (g : X Y) [] :

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

theorem CategoryTheory.Preadditive.hasCokernel_of_hasCoequalizer {C : Type u} {X : C} {Y : C} (f : X Y) (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.

instance CategoryTheory.Preadditive.instSMulUnitsIntIso {C : Type u_1} [] {X : C} {Y : C} :
SMul (X Y)
Equations
• CategoryTheory.Preadditive.instSMulUnitsIntIso = { smul := fun (a : ) (e : X Y) => { hom := a e.hom, inv := a⁻¹ e.inv, hom_inv_id := , inv_hom_id := } }
@[simp]
theorem CategoryTheory.Preadditive.smul_iso_hom {C : Type u_1} [] {X : C} {Y : C} (a : ) (e : X Y) :
(a e).hom = a e.hom
@[simp]
theorem CategoryTheory.Preadditive.smul_iso_inv {C : Type u_1} [] {X : C} {Y : C} (a : ) (e : X Y) :
(a e).inv = a⁻¹ e.inv
instance CategoryTheory.Preadditive.instNegIso {C : Type u_1} [] {X : C} {Y : C} :
Neg (X Y)
Equations
• CategoryTheory.Preadditive.instNegIso = { neg := fun (e : X Y) => { hom := -e.hom, inv := -e.inv, hom_inv_id := , inv_hom_id := } }
@[simp]
theorem CategoryTheory.Preadditive.neg_iso_hom {C : Type u_1} [] {X : C} {Y : C} (e : X Y) :
(-e).hom = -e.hom
@[simp]
theorem CategoryTheory.Preadditive.neg_iso_inv {C : Type u_1} [] {X : C} {Y : C} (e : X Y) :
(-e).inv = -e.inv