Every NonPreadditiveAbelian category is preadditive

In mathlib, we define an abelian category as a preadditive category with a zero object, kernels and cokernels, products and coproducts and in which every monomorphism and epimorphism is normal.

While virtually every interesting abelian category has a natural preadditive structure (which is why it is included in the definition), preadditivity is not actually needed: Every category that has all of the other properties appearing in the definition of an abelian category admits a preadditive structure. This is the construction we carry out in this file.

The proof proceeds in roughly five steps:

1. Prove some results (for example that all equalizers exist) that would be trivial if we already had the preadditive structure but are a bit of work without it.
2. Develop images and coimages to show that every monomorphism is the kernel of its cokernel.

The results of the first two steps are also useful for the "normal" development of abelian categories, and will be used there.

3. For every object A, define a "subtraction" morphism σ : A ⨯ A ⟶ A and use it to define subtraction on morphisms as f - g := prod.lift f g ≫ σ.
4. Prove a small number of identities about this subtraction from the definition of σ.
5. From these identities, prove a large number of other identities that imply that defining f + g := f - (0 - g) indeed gives an abelian group structure on morphisms such that composition is bilinear.

The construction is non-trivial and it is quite remarkable that this abelian group structure can be constructed purely from the existence of a few limits and colimits. Even more remarkably, since abelian categories admit exactly one preadditive structure (see subsingletonPreadditiveOfHasBinaryBiproducts), the construction manages to exactly reconstruct any natural preadditive structure the category may have.

References

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

class CategoryTheory.NonPreadditiveAbelian (C : Type u) [CategoryTheory.Category.{v, u} C] extends CategoryTheory.Limits.HasZeroMorphisms , CategoryTheory.NormalMonoCategory , CategoryTheory.NormalEpiCategory : Type (max u v)

We call a category NonPreadditiveAbelian if it has a zero object, kernels, cokernels, binary products and coproducts, and every monomorphism and every epimorphism is normal.

• zero : (X Y : C) → Zero (X ⟶ Y)
• comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), CategoryTheory.CategoryStruct.comp f 0 = 0
• zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), CategoryTheory.CategoryStruct.comp 0 f = 0
• normalMonoOfMono : {X Y : C} → (f : X ⟶ Y) → [inst : CategoryTheory.Mono f] → CategoryTheory.NormalMono f
• normalEpiOfEpi : {X Y : C} → (f : X ⟶ Y) → [inst : CategoryTheory.Epi f] → CategoryTheory.NormalEpi f
• has_zero_object : CategoryTheory.Limits.HasZeroObject C
• has_kernels : CategoryTheory.Limits.HasKernels C
• has_cokernels : CategoryTheory.Limits.HasCokernels C
• has_finite_products : CategoryTheory.Limits.HasFiniteProducts C
• has_finite_coproducts : CategoryTheory.Limits.HasFiniteCoproducts C

instance CategoryTheory.NonPreadditiveAbelian.instEpiImageToHasZeroMorphismsHas_kernelsHas_cokernelsFactorThruImage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.Epi (CategoryTheory.Abelian.factorThruImage f)

The map p : P ⟶ image f is an epimorphism

Equations

• ⋯ = ⋯

instance CategoryTheory.NonPreadditiveAbelian.isIso_factorThruImage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {P : C} {Q : C} (f : P ⟶ Q) [CategoryTheory.Mono f] : CategoryTheory.IsIso (CategoryTheory.Abelian.factorThruImage f)

Equations

• ⋯ = ⋯

instance CategoryTheory.NonPreadditiveAbelian.instMonoCoimageToHasZeroMorphismsHas_kernelsHas_cokernelsFactorThruCoimage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.Mono (CategoryTheory.Abelian.factorThruCoimage f)

The canonical morphism i : coimage f ⟶ Q is a monomorphism

Equations

• ⋯ = ⋯

instance CategoryTheory.NonPreadditiveAbelian.isIso_factorThruCoimage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {P : C} {Q : C} (f : P ⟶ Q) [CategoryTheory.Epi f] : CategoryTheory.IsIso (CategoryTheory.Abelian.factorThruCoimage f)

Equations

• ⋯ = ⋯

def CategoryTheory.NonPreadditiveAbelian.epiIsCokernelOfKernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} {f : X ⟶ Y} [CategoryTheory.Epi f] (s : CategoryTheory.Limits.Fork f 0) (h : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ f ⋯)

In a NonPreadditiveAbelian category, an epi is the cokernel of its kernel. More precisely: If f is an epimorphism and s is some limit kernel cone on f, then f is a cokernel of Fork.ι s.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.NonPreadditiveAbelian.monoIsKernelOfCokernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} {f : X ⟶ Y} [CategoryTheory.Mono f] (s : CategoryTheory.Limits.Cofork f 0) (h : CategoryTheory.Limits.IsColimit s) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f ⋯)

In a NonPreadditiveAbelian category, a mono is the kernel of its cokernel. More precisely: If f is a monomorphism and s is some colimit cokernel cocone on f, then f is a kernel of Cofork.π s.

Equations

• One or more equations did not get rendered due to their size.

@[inline, reducible]

abbrev CategoryTheory.NonPreadditiveAbelian.r {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] (A : C) : A ⟶ CategoryTheory.Limits.cokernel (CategoryTheory.Limits.diag A)

The composite A ⟶ A ⨯ A ⟶ cokernel (Δ A), where the first map is (𝟙 A, 0) and the second map is the canonical projection into the cokernel.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.NonPreadditiveAbelian.mono_Δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {A : C} : CategoryTheory.Mono (CategoryTheory.Limits.diag A)

Equations

• ⋯ = ⋯

instance CategoryTheory.NonPreadditiveAbelian.mono_r {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {A : C} : CategoryTheory.Mono (CategoryTheory.NonPreadditiveAbelian.r A)

Equations

• ⋯ = ⋯

instance CategoryTheory.NonPreadditiveAbelian.epi_r {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {A : C} : CategoryTheory.Epi (CategoryTheory.NonPreadditiveAbelian.r A)

Equations

• ⋯ = ⋯

instance CategoryTheory.NonPreadditiveAbelian.isIso_r {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {A : C} : CategoryTheory.IsIso (CategoryTheory.NonPreadditiveAbelian.r A)

Equations

• ⋯ = ⋯

@[inline, reducible]

abbrev CategoryTheory.NonPreadditiveAbelian.σ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {A : C} : A ⨯ A ⟶ A

The composite A ⨯ A ⟶ cokernel (diag A) ⟶ A given by the natural projection into the cokernel followed by the inverse of r. In the category of modules, using the normal kernels and cokernels, this map is equal to the map (a, b) ↦ a - b, hence the name σ for "subtraction".

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.NonPreadditiveAbelian.diag_σ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.diag X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.NonPreadditiveAbelian.r X)) h)) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.NonPreadditiveAbelian.diag_σ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag X) CategoryTheory.NonPreadditiveAbelian.σ = 0

@[simp]

theorem CategoryTheory.NonPreadditiveAbelian.lift_σ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) 0) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.diag X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.NonPreadditiveAbelian.r X)) h)) = h

@[simp]

theorem CategoryTheory.NonPreadditiveAbelian.lift_σ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) 0) CategoryTheory.NonPreadditiveAbelian.σ = CategoryTheory.CategoryStruct.id X

theorem CategoryTheory.NonPreadditiveAbelian.lift_map_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⨯ Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) 0) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id Y) 0) h)

theorem CategoryTheory.NonPreadditiveAbelian.lift_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) 0) (CategoryTheory.Limits.prod.map f f) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id Y) 0)

def CategoryTheory.NonPreadditiveAbelian.isColimitσ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ CategoryTheory.NonPreadditiveAbelian.σ ⋯)

σ is a cokernel of Δ X.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.NonPreadditiveAbelian.σ_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp CategoryTheory.NonPreadditiveAbelian.σ f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f f) CategoryTheory.NonPreadditiveAbelian.σ

This is the key identity satisfied by σ.

def CategoryTheory.NonPreadditiveAbelian.hasSub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} : Sub (X ⟶ Y)

Subtraction of morphisms in a NonPreadditiveAbelian category.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.NonPreadditiveAbelian.hasNeg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} : Neg (X ⟶ Y)

Negation of morphisms in a NonPreadditiveAbelian category.

Equations

• CategoryTheory.NonPreadditiveAbelian.hasNeg = { neg := fun (f : X ⟶ Y) => 0 - f }

def CategoryTheory.NonPreadditiveAbelian.hasAdd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} : Add (X ⟶ Y)

Addition of morphisms in a NonPreadditiveAbelian category.

Equations

• CategoryTheory.NonPreadditiveAbelian.hasAdd = { add := fun (f g : X ⟶ Y) => f - -g }

theorem CategoryTheory.NonPreadditiveAbelian.sub_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) (b : X ⟶ Y) : a - b = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift a b) CategoryTheory.NonPreadditiveAbelian.σ

theorem CategoryTheory.NonPreadditiveAbelian.add_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) (b : X ⟶ Y) : a + b = a - -b

theorem CategoryTheory.NonPreadditiveAbelian.neg_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) : -a = 0 - a

theorem CategoryTheory.NonPreadditiveAbelian.sub_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) : a - 0 = a

theorem CategoryTheory.NonPreadditiveAbelian.sub_self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) : a - a = 0

theorem CategoryTheory.NonPreadditiveAbelian.lift_sub_lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) (b : X ⟶ Y) (c : X ⟶ Y) (d : X ⟶ Y) : CategoryTheory.Limits.prod.lift a b - CategoryTheory.Limits.prod.lift c d = CategoryTheory.Limits.prod.lift (a - c) (b - d)

theorem CategoryTheory.NonPreadditiveAbelian.sub_sub_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) (b : X ⟶ Y) (c : X ⟶ Y) (d : X ⟶ Y) : a - c - (b - d) = a - b - (c - d)

theorem CategoryTheory.NonPreadditiveAbelian.neg_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) (b : X ⟶ Y) : -a - b = -b - a

theorem CategoryTheory.NonPreadditiveAbelian.neg_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) : - -a = a

theorem CategoryTheory.NonPreadditiveAbelian.add_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) (b : X ⟶ Y) : a + b = b + a

theorem CategoryTheory.NonPreadditiveAbelian.add_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) (b : X ⟶ Y) : a + -b = a - b

theorem CategoryTheory.NonPreadditiveAbelian.add_neg_self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) : a + -a = 0

theorem CategoryTheory.NonPreadditiveAbelian.neg_add_self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) : -a + a = 0

theorem CategoryTheory.NonPreadditiveAbelian.neg_sub' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) (b : X ⟶ Y) : -(a - b) = -a + b

theorem CategoryTheory.NonPreadditiveAbelian.neg_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) (b : X ⟶ Y) : -(a + b) = -a - b

theorem CategoryTheory.NonPreadditiveAbelian.sub_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) (b : X ⟶ Y) (c : X ⟶ Y) : a - b + c = a - (b - c)

theorem CategoryTheory.NonPreadditiveAbelian.add_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) (b : X ⟶ Y) (c : X ⟶ Y) : a + b + c = a + (b + c)

theorem CategoryTheory.NonPreadditiveAbelian.add_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} (a : X ⟶ Y) : a + 0 = a

theorem CategoryTheory.NonPreadditiveAbelian.comp_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f (g - h) = CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.comp f h

theorem CategoryTheory.NonPreadditiveAbelian.sub_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (f - g) h = CategoryTheory.CategoryStruct.comp f h - CategoryTheory.CategoryStruct.comp g h

theorem CategoryTheory.NonPreadditiveAbelian.comp_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] (X : C) (Y : C) (Z : C) (f : X ⟶ Y) (g : Y ⟶ Z) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f (g + h) = CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f h

theorem CategoryTheory.NonPreadditiveAbelian.add_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] (X : C) (Y : C) (Z : C) (f : X ⟶ Y) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (f + g) h = CategoryTheory.CategoryStruct.comp f h + CategoryTheory.CategoryStruct.comp g h

def CategoryTheory.NonPreadditiveAbelian.preadditive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] : CategoryTheory.Preadditive C

Every NonPreadditiveAbelian category is preadditive.

Equations

• CategoryTheory.NonPreadditiveAbelian.preadditive = { homGroup := fun (X Y : C) => AddCommGroup.mk ⋯, add_comp := ⋯, comp_add := ⋯ }