mathlib

mathlib copied to clipboard

The usual definition of exactness in category theory seems to be along the lines of "the image of f is a kernel of g". I have found this definition to be a bit unwieldy to use in Lean. In my project I use a definition used by Aluffi in the book "Algebra: Chapter 0":

def exact {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) : Prop :=
f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0

I like this definition for several reasons:

• It is a Prop, unlike definitions involving is_limit.
• Still, in an abelian category it is easily shown to be equivalent to the "image is kernel" definition.
• It uses only "low-power" ingredients: We do not have to know what an image is.
• It is trivial to show that exact f g ↔ f.range = g.ker in Module R.

I am interested in your thoughts and suggestions regarding this definition.