Diagram chases in general abelian categories

Stream: homology

[Joël Riou]

In #7821 I introduce the notion of "refinement" which enables doing diagram chases in general abelian categories. Abstractly, this could be thought as the replacement of an object X in an abelian category C by its yoneda presheaf (maps to X) and then arguing locally for the canonical topology on C: monomorphisms, epimorphisms and exactness in C can be characterized as injectivity, surjective-like, exactness-like properties in terms of maps in C, provided we argue "up to refinements", i.e. allow precomposition with epimorphisms. (More details in the docstring of the file introduced in this PR.) This shall be used in my formalization of the snake lemma.

[Johan Commelin]

Can you please remind me how this differs from pseudo-elements?

[Joël Riou]

The pseudo-elements of X : C that are in mathlib are equivalence classes of morphisms f : A ⟶ Xby an equivalence relation. The pseudoelement of X attached tof : A ⟶ Xequals the pseudoelement attached to f' : A' ⟶ X iff f and f' have the same image. Forgetting everything but the image of f is forgetting a lot of information, which is why there is no extensionnality property for the pseudo-elements in mathlib (in the sense that a morphism X ⟶ Y is not determined by its action on pseudoelements). In my approach, I do not introduce other types, I phrase everything in terms of morphisms A ⟶ X for a given A (for which equality obviously make sense) and in the proofs we sometimes have to introduce some auxiliary epi A' ⟶ A and precompose with it.
Morphisms are easier to work with as compared to these pseudoelements because we have the whole category theory library to deal with it, and there are results which I had attempted to prove using the pseudoelements, but fail to do so mainly because of the extensionnality issue.

[Johan Commelin]

Thanks for explaining. I think this subtlety should be documented somewhere.

[Antoine Chambert-Loir]

@Joël Riou , is this a notion you coined out yourself? It deserves to be popularized, in particular, to emphasize the geometric insight that underlies it.

[Joël Riou]

No, I have just rediscovered something which appeared in unpublished notes by George Bergman in 1974, see the first page of http://math.berkeley.edu/~gbergman/papers/unpub/elem-chase.pdf

[Kevin Buzzard]

Oh so then it's best to just publicise on this thread and nowhere else, so it just remains "known to the experts" :-)

[Joël Riou]

Well, it is mentionned there too: https://ncatlab.org/nlab/show/abelian+category

[Kevin Buzzard]

Another unrefereed source :-) And subject to change at any point too!

[Joël Riou]

You suggest I should publish something about my formalization of derived categories/spectral sequences/etc...

[Kevin Buzzard]

Oh of course! Absolutely! Send it to CPP or ITP. I was being silly in my last two posts but here I'm being serious.

[Patrick Massot]

Joël, the work you did in mathlib very clearly deserves to be published. And having a written account would be useful too.

[Kevin Buzzard]

If you don't want to be limited to 14 pages or whatever then JAR is another possibility (Journal of Automated Research) (Journal of Automated Reasoning -- thanks Patrick and sorry).

[Patrick Massot]

Kevin means Journal of automated reasoning.