Define exact sequences

[TwoFX]

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.

[kim-em]

Why not just?

structure exact {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) :=
(zero : f ≫ g = 0)
(is_iso : is_iso (kernel_image_comparison zero))

where kernel_image_comparion f g w is the universal morphism image f ⟶ kernel g given the witness w : f ≫ g = 0.

I'm a bit wary of giving definitions which are equivalent to the general one, but only in the important special case...

I don't think it's any particular problem that this is not in Prop. We do this all over the category theory library: in this case it's just because we've decided we don't mind that is_iso is not in Prop.

We can certainly have a constructor, in abelian categories, from this equation, and then in, e.g. Module R, have easy access to f.range = g.ker.

[jcommelin]

Shouldn't we be doing exact categories as well? How easy would it be to refactor the library later to splice them in?

[jcommelin]

Here's an approach to exact sequences of finite length: https://github.com/leanprover-community/lean-liquid/blob/b01536ea4f08978e2aaa5e35df734c822a33033b/src/for_mathlib/exact_seq.lean