delta functors

Stream: condensed mathematics

[Johan Commelin]

commit 0c0ee212ce0044a198dbb5691a049d4f52ce5bfe (HEAD -> master)
Author: Johan Commelin <johan@commelin.net>
Date:   Mon Sep 20 19:31:05 2021 +0000

    add category of short exact sequences, add delta functors

 src/for_mathlib/abelian_category.lean |  24 +++++++++++++++++++++--
 src/for_mathlib/delta_functor.lean    | 104 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 126 insertions(+), 2 deletions(-)

[Adam Topaz]

I added the category structure for delta functors and the definition of a universal delta functor in the branch delta_functor here:
https://github.com/leanprover-community/lean-liquid/blob/a96e297e08595aa18a81a11876714785c77b5230/src/for_mathlib/delta_functor.lean#L143
(Note that this branch bundled delta functors so that we can consider the category of delta functors, whereas Johan's code defines delta functors as a class.)

[Johan Commelin]

Do you expect to need that for LTE? Or is this "planning ahead" for mathlib?

[Adam Topaz]

Johan Commelin said:

Do you expect to need that for LTE? Or is this "planning ahead" for mathlib?

Do we not need the fact that derived functors are universal? Or even functoriality of long exact sequences (which presumably would use a category structure on delta functors)

[Johan Commelin]

No, I don't think we need functoriality of the LES

[Johan Commelin]

We'll just apply it to some explicit SES:

$$0 → ℳ(S, ℤ((T))_{r'}) \xrightarrow{⬝ f_x} ℳ(S, ℤ((T))_{r'}) → ℳ_{p'}(S) → 0$$

and some others.

[Johan Commelin]

I'm not sure anymore that we should show that Ext is a delta functor. It should be done at some point, of course. But I don't think LTE needs it. It requires a crazy amount of naturality, and I don't want to think about that for now.

All we need is the LES for single short exact sequences. We don't need naturality in the SES.

[Johan Commelin]

@Riccardo Brasca In particular, this means that we only need the "ordinary" snake lemma. Not the functorial version.

[Johan Commelin]

So you don't need to provide an instance for has_snake_lemma.

[Johan Commelin]

Because I can imagine that it might be painful as well.

[Riccardo Brasca]

Yeah... quoting Paolo Aluffi's Algebra book "proving the Snake Lemma is something that should not be done in public".

[Johan Commelin]

we could do it in a separate github repo that we make private (-;