snake lemma

Stream: condensed mathematics

[Johan Commelin]

@Riccardo Brasca I just pushed a class has_snake_lemma.

[Johan Commelin]

Here is an excerpt:

class has_snake_lemma :=
(δ : snake_input.proj 𝒜 (0,2) ⟶ snake_input.proj 𝒜 (3,0))
(exact_δ : ∀ (D : snake_input 𝒜), exact ((0,1) ⟶[D] (0,2)) (δ.app D))
(δ_exact : ∀ (D : snake_input 𝒜), exact (δ.app D) ((3,0) ⟶[D.1] (3,1))) -- why can't I write `⟶[D]`

namespace snake_lemma

variables [has_snake_lemma 𝒜]

variables {𝒜}

def δ (D : snake_input 𝒜) : D.obj (0,2) ⟶ D.obj (3,0) := has_snake_lemma.δ.app D

lemma exact_δ (D : snake_input 𝒜) : exact ((0,1) ⟶[D] (0,2)) (δ D) :=
has_snake_lemma.exact_δ D

lemma δ_exact (D : snake_input 𝒜) : exact (δ D) ((3,0) ⟶[D] (3,1)) :=
has_snake_lemma.δ_exact D

end snake_lemma

[Johan Commelin]

The trouble with the snake lemma is that nobody shows that it is functorial.

[Johan Commelin]

But we will certainly need that.

[Johan Commelin]

So I defined a category snake_input consisting of the diagrams to which the snake lemma applies. And has_snake_lemma asserts that there is a δ that snakes through the diagram.

[Johan Commelin]

I also added some wacky definitions. For example, if D is such a diagram, then (0,1) ⟶[D] (0,2) is the arrow in the top right, between the two rightmost kernels.

[Riccardo Brasca]

You are too fast!
But it seems very good for me: we can already use in practice if we need it and I can work on the proof, right?

[Johan Commelin]

/-- The base diagram for the snake lemma. The object are indexed by `fin 4 × fin 3`:

(0,0) --> (0,1) --> (0,2)              | the kernels
  |         |         |
  v         v         v
(1,0) --> (1,1) --> (1,2)              | the first exact row
  |         |         |
  v         v         v
(2,0) --> (2,1) --> (2,2)              | the second exact row
  |         |         |
  v         v         v
(3,0) --> (3,1) --> (3,2)              | the cokernels

-/
@[derive [preorder, decidable_eq]]
def snake_diagram := fin 4 × fin 3

[Johan Commelin]

Yeah, I hope that with this notation, it is even somewhat usable when proving things.

[Johan Commelin]

If you write down 12 objects and 17 maps, you completely go crazy.

[Johan Commelin]

So now there are two subgoals:

1. show that an abelian category with enough projectives has an instance of has_snake_lemma
2. if you have has_snake_lemma then derived functors are delta functors.

[Riccardo Brasca]

OK, I can work on 1. Is this in some branch?

[Riccardo Brasca]

It's in master, thank you!

[Johan Commelin]

@Riccardo Brasca great. I'll work on (2)

[Riccardo Brasca]

I see that in is_snake_input you wrote row_exact : ∀ i, exact ((i,0) ⟶[D] (i,1)) ((i,1) ⟶[D] (i,2)). For i = 0 and i = 3 this is automatic, right? It is part of what I call the snake lemma (easier than working with δ of course). Do we know that ker is left exact?

[Riccardo Brasca]

Mh, maybe I am confused, but in is_snake_input, where is the condition that F (0,0) is the kernel of F 0 0 ⟶ F 1 0?

[Johan Commelin]

@Riccardo Brasca You are right!

[Johan Commelin]

So we should remove those conditions (and add them to has_snake_lemma)

[Johan Commelin]

The kernel condition is the combination of col_exact and mono.

[Riccardo Brasca]

Ah sure

[Johan Commelin]

@Riccardo Brasca I pushed a fix for the is_snake_input stuff.

[Johan Commelin]

So now row_exact₀ and row_exact₃ are sorried lemmas.

[Adam Topaz]

Looks like for_mathlib/fin_functor is missing?

[Johan Commelin]

Oops, sorry.

[Johan Commelin]

I pushed it

[Riccardo Brasca]

Is there a reason we have

variables (𝒜 : Type u) [category.{v} 𝒜] [has_images 𝒜] [has_zero_morphisms 𝒜] [has_kernels 𝒜]

instead of

variables (𝒜 : Type u) [category.{v} 𝒜] [abelian 𝒜]

? The full snake lemma surely need an abelian category, and I don't think it is a reasonable task to check which part need weaker assumptions, unless we really need it...

[Johan Commelin]

@Riccardo Brasca certainly just provide the instance under abelian assumptions

[Johan Commelin]

but the definition doesn't need more. And at some point people might want to do exact categories with snake lemmas, or something like that.

[Riccardo Brasca]

I've started the proof of row_exact₀. It's not that fun, but with the notation you introduced is quite doable. I will try a calc block instead of rewriting everything for the second part, to check which one is better.

[Adam Topaz]

@Riccardo Brasca I wanted to play around with pseudoelements to see how hard (or easy) it was and I filled in that sorry in row_exact₀. Do you want me to push, or do you already have a working proof?

I found it quite natural to do this proof along the same lines as a pen-and-paper diagram chase.

[Riccardo Brasca]

Go ahead!

[Riccardo Brasca]

Yes, the part with pseudoelements is really the same as with pen and paper, I just wanted to play with Johan's notation

[Adam Topaz]

Okay, it's pushed. One key point I added was this:

local attribute [instance] abelian.pseudoelement.over_to_sort
  abelian.pseudoelement.hom_to_fun
  abelian.pseudoelement.has_zero

which makes working with pseudoelements very natural

[Riccardo Brasca]

The definition of δ must be done using universal properties of course, but then we can again check exactness using pseudoelements.

[Riccardo Brasca]

The proof I found on the internet uses the interesting ideas that, if the category has enough projectives, then exactness can be checked using "projective pseudoelements" (meaning that the source is projective). I have the impression that working with these is really easier than with general pseudoelements (we can take literally the difference)

[Adam Topaz]

The universal properties should make it easy to construct a morphism from the kernel of the right-most map to the cokernel of the left-most map. We just need to build an isomorphhism between the corresponding objects in the diagram and these kernel/cokernels, whichh can be done using docs#category_theory.abelian.is_iso_of_mono_of_epi and the characterization of (in/bij)ectivity using pseudoelements.

[Riccardo Brasca]

We have to try, but usually at some point one take the difference of certains elements. I am not sure this works very well with pseudo elements, but I would be happy to be proven wrong

[Riccardo Brasca]

On the other hand, with enough projectives, a sequence is exact iff for all P projective hom(P, -) is exact. In particular, after having fixed P, we have a genuine sequence of abelian groups, and the usual proof works

[Riccardo Brasca]

And one can lift along epi, so it's better than usual yoneda

[Johan Commelin]

Aside. I'm quite happy with how this looks:

variables {𝒜 : Type*} [category 𝒜] [abelian 𝒜]

local notation `kernel_map`   := kernel.map _ _ _ _
local notation `cokernel_map` := cokernel.map _ _ _ _

def mk_of_short_exact_sequence_hom (A B : short_exact_sequence 𝒜) (f : A ⟶ B) :
  snake_diagram ⥤ 𝒜 :=
mk_functor
/- == Passing in the matrix of objects first, to make Lean happy == -/
![![kernel f.1, kernel f.2, kernel f.3],
  ![A.1, A.2, A.3],
  ![B.1, B.2, B.3],
  ![cokernel f.1, cokernel f.2, cokernel f.3]]
/- == All the morphisms in the diagram == -/
  /- ker f.1 -/   (kernel_map f.sq1)   /- ker f.2 -/   (kernel_map f.sq2)   /- ker f.3 -/
  (kernel.ι _)                         (kernel.ι _)                         (kernel.ι _)
  /-   A.1   -/          A.f           /-   A.2   -/          A.g           /-   A.3   -/
       f.1                                  f.2                                  f.3
  /-   B.1   -/          B.f           /-   B.2   -/          B.g           /-   B.3   -/
  (cokernel.π _)                       (cokernel.π _)                       (cokernel.π _)
  /- coker f.1 -/ (cokernel_map f.sq1) /- coker f.2 -/ (cokernel_map f.sq2) /- coker f.3 -/
/- == Prove that the squares commute == -/
(by { delta kernel.map, rw [kernel.lift_ι] }) (by { delta kernel.map, rw [kernel.lift_ι] })
f.sq1 f.sq2
(by { delta cokernel.map, rw [cokernel.π_desc] }) (by { delta cokernel.map, rw [cokernel.π_desc] })

[Riccardo Brasca]

Very nice!

[Adam Topaz]

I'll work on constructing $\delta$ this afternoon.

[Adam Topaz]

I've added a general skeleton for the construction of delta here:
https://github.com/leanprover-community/lean-liquid/blob/b87355041bf779b20e4177b4300d19a7aff0ddf6/src/for_mathlib/snake_lemma.lean#L668

I'm fairly sure this definition is correct, but a second pair of eyes would be helpful :)

[Johan Commelin]

I'll take a look once I've had breakfast (-;

[Adam Topaz]

I proved one of the main maps was an isomorphism, so I'm more confident now that it's correct ;)

[Riccardo Brasca]

I am proving row_exact₃.

[Riccardo Brasca]

row_exact₃ is sorry free.

Some random comments:

• this is the first place where docs#category_theory.abelian.pseudoelement.sub_of_eq_image is used in this file. Everything worked extremely well, exactly as with pen and paper. I think this is very promising, since docs#category_theory.abelian.pseudoelement.sub_of_eq_image replace the difference of pseudoelements, that can not be done in general. So it's possible that even for δ the proof will be as the classical one.
• I did

rw [← abelian.pseudoelement.comp_apply, ← D.map_comp, map_eq hD ((hom _ _) ≫ (hom _ _)) ((hom _ _) ≫ (hom _ _)),
      D.map_comp, abelian.pseudoelement.comp_apply]

or something similar several time, and it seems that Adam had to do to the same. Maybe it's reasonable to write a tactic for that, but I have no idea if it's worth the effort.

[Johan Commelin]

meta def riccardos_tactic : tactic unit :=
`[rw [← abelian.pseudoelement.comp_apply, ← D.map_comp, map_eq hD ((hom _ _) ≫ (hom _ _)) ((hom _ _) ≫ (hom _ _)),
      D.map_comp, abelian.pseudoelement.comp_apply]]

[Johan Commelin]

@Riccardo Brasca Voila: :this: is your tactic

[Riccardo Brasca]

Oh, that was fast!

[Riccardo Brasca]

Mmh, sometimes we need it for the composition of three morphisms rather than two, and we also need to specify some _... it doesn't matter, copy/paste is perfectly fine.

[Riccardo Brasca]

BTW, since we are in a "snake lemma mood", do we need also the very first and very last element of the sequence?

[Riccardo Brasca]

I mean, using the terminology in wikipedia, the kernel of the first map of the snake is $\ker(f)$, and the cokernel of the last one is $\mathrm{coker}(g')$.

[Riccardo Brasca]

So we get a 8 terms exact sequence (plus zeros at the beginning and at the end).

[Kevin Buzzard]

Do we have 8 term exact sequences in mathlib or just short exact sequences and long exact sequences?

[Riccardo Brasca]

I think we only have docs#category_theory.exact, that is about two composable morphisms

[Riccardo Brasca]

Johan (or someone else) defined

structure short_exact_sequence [has_images 𝒞] [has_zero_morphisms 𝒞] [has_kernels 𝒞] :=
(fst snd trd : 𝒞)
(f : fst ⟶ snd)
(g : snd ⟶ trd)
[mono'  : mono f]
[epi'   : epi g]
[exact' : exact f g]

in LTE

[Kevin Buzzard]

I had imagined that the snake lemma was going to be 6 separate statements of the form "I'm exact here"

[Adam Topaz]

Kevin Buzzard said:

I had imagined that the snake lemma was going to be 6 separate statements of the form "I'm exact here"

it probably will be.

[Adam Topaz]

I finished off the last few sorry's needed for the definition of $\delta$. Now we can think about the actual proof of the snake lemma ;)

[Adam Topaz]

One half of the snake lemma is now done in the following form:

theorem exact_to_δ : exact ((0,1) ⟶[D] (0,2)) hD.δ := ...

[Adam Topaz]

The other half is now done as well:

theorem exact_to_δ : exact ((0,1) ⟶[D] (0,2)) hD.δ := ...

theorem exact_from_δ : exact hD.δ ((3,0) ⟶[D] (3,1)) := ...

[Johan Commelin]

@Adam Topaz Wow, amazing work!

[Adam Topaz]

Thanks! I was a bit careless with nonterminal simps, and many of the proofs can probably be golfed a bit (and hopefully sped up as well). I'll try to do a bit of cleanup soon.

[Johan Commelin]

@Adam Topaz maybe we should ignore that cleanup for now

[Johan Commelin]

Yesterday I discovered the salamander lemma: https://ncatlab.org/nlab/show/salamander+lemma

[Johan Commelin]

Mulling over it yesterday and tonight, I'm now thinking we could have a side project that puts a big fat E back in LTE: develop a DSL for double complex diagram chases, together with an integration into the widget framework.

[Johan Commelin]

It would use some sort of proof-by-reflection technique (if I understand correctly what that means)

[Johan Commelin]

Together with integration in the widget framework, this could create pretty slick pointy-clicky proofs that also look good. And they might be quite fast as well.

[Adam Topaz]

Salamander = more evolved snake?

[Johan Commelin]

And it would be a really nice addition to mathlib, that could be used to create pretty proofs of other "double complex" lemmas as well, like the four lemmas, five lemma, 3x3 lemma, LES for a SES of chain complexes.

[Johan Commelin]

Adam Topaz said:

Salamander = more evolved snake?

More like: small snake. It provides a toolkit of small building blocks that you assemble to prove things like the snake lemma.

[Adam Topaz]

Ah I see. I'm about to go to sleep... I'll have to look tomorrow. Integrating these arguments with widgets would be amazing!

[Kevin Buzzard]

@Eric Rodriguez

[Riccardo Brasca]

@Adam Topaz Amazing!!

[Eric Rodriguez]

Can someone give me a brief explanation of how a diagram chase (especially a "double complex" one) works? I know very basic category theory (not even limits yet :[) but have been wanting to learn it for a while anyways, and from brief googling it seems to be mostly using properties of monos/epis

[Johan Commelin]

Yeah, that's right. But in this DSL, that would all be hidden away.

[Johan Commelin]

@Kevin Buzzard @Adam Topaz @Riccardo Brasca Wolfang Soergel just pointed out to me that the $\delta$ in the snake lemma is the unique map from ker c to coker a that is compatible with the natural surjective maps ker diag -> ker c and ker diag -> coker a, where diag is the diagonal map B -> C' in the second square of the snake diagram.

[Johan Commelin]

So you cannot choose $-\delta$.

[Johan Commelin]

This universal property will certainly be helpful if we want to prove naturality of $\delta$ at some point.

[Matthew Ballard]

A simple example with both a words and a picture is in the notes from my current class. There it is just proving a retract of an exact complex is exact.

The punchline is “take an element and push it around”

[Reid Barton]

but note that this picture is happening in Mod(R) or implicitly using the Freyd-Mitchell embedding theorem and not really using properties of monic/epics in the categorical sense, otherwise you can't perform the step "there exists $b'$ sent to $b$"

[Matthew Ballard]

Yes of course

[Matthew Ballard]

If you want to be completely precise, you draw some diagrams of Hom spaces instead and really use universal properties.

[Matthew Ballard]

Perhaps the biggest caveat is typos :blushing:

[Riccardo Brasca]

Ah yes, we should prove uniqueness. And it's probably not that hard!

[Riccardo Brasca]

By the way I am now in love with the salamander lemma!

[Patrick Massot]

I envy you. I've been trying to fall in love with this lemma for years and never managed. I'm always excited each time I start reading that webpage but this excitement doesn't survive until the end of the page.

[Johan Commelin]

@Patrick Massot It took a while for me to click as well.

[Johan Commelin]

Also, it's not clear how to do this in Lean. We need really good data structures to manage these diagrams.

[Johan Commelin]

That's why I think a proof by reflection might help.

[Riccardo Brasca]

Well, maybe "in love" is a little bit too much...
It's true that we should see in practice if deducing the snake lemma (for example) is really easy from the salamander or not, but at least it gives a general technique.

[Adam Topaz]

Johan Commelin said:

Also, it's not clear how to do this in Lean. We need really good data structures to manage these diagrams.

We would also need a nice way to go between e.g. $cokernel(0 \to M)$, $kernel(M \to 0)$ and $M$ and similarly silly things. I think this will be one of the main annoying points in deducing the snake lemma from the salamander lemma

[Johan Commelin]

Right, but such a DSL could hopefully take care of that

[Adam Topaz]

@Matthew Ballard this is the most accurate thing I have ever seen (from your webpage)

Learning Outcomes

After successful completion of this course, you will be able to:

    Localize abelian categories for fun and profit
    Draw confusing diagrams that claim to explain the octohedral axiom
    Day dream about stable ∞\infty∞-categories

[Matthew Ballard]

Even that has a typo: abelian triangulated

[Reid Barton]

Also, it's the octahedral axiom. :upside_down:

[Matthew Ballard]

Finally, we ignore TR4) until we actually need it (as is tradition).

[Matthew Ballard]

Though, Neeman's presentation of it is great.

[Matthew Ballard]

Perhaps to get the topic back on the rails, I would like to say I am interested in embedding commutative diagrams in some efficient data structure that can be, perhaps, be automated over. Almost any check of this type in practice is a toucan-sam type follow your nose process.

[Matthew Ballard]

I also imagine that anything developed would not be limited to bi-complexes but would be applicable to higher dimensional versions.

[Adam Topaz]

The good news is that we now have docs#prefunctor which we can use to model diagrams

[Matthew Ballard]

The most naive thing I can think of is picking a node and submodule of that component and pushing it around via images and inverse images.

[Adam Topaz]

We would also need some structure that should let us label which pairs of composable morphisms in the diagram are exact.

[Johan Commelin]

I wonder whether there is some decidable theory lurking around here...

[Matthew Ballard]

Adam Topaz said:

We would also need some structure that should let us label which pairs of composable morphisms in the diagram are exact.

Right. The question can kinda be rephrased as: pass to Grothendieck group and see if this push/pull correspondence is actually a function

[Johan Commelin]

Turning the salamander lemma into a nice proof-method is going to be a serious side project. I very much think that it should be done. It would be a beautiful spin-off of LTE.

[Johan Commelin]

But I'm not sure LTE should wait for that to finish.

[Johan Commelin]

I suggest we continue further discussion of the salamander project in this thread: https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/salamander.20tactic

[Johan Commelin]

@Riccardo Brasca Did you prove that (0,0) ⟶[D] (0,1) is a mono if (1,0) ⟶[D] (1,1) is a mono?

[Riccardo Brasca]

Not yet, I can do it today. (The most general statement is, I think, that there is a mono ker((1,0) ⟶[D] (1,1)) ⟶[D] (0,0).)

[Johan Commelin]

I pushed a bit more horseshoe stuff.

[Johan Commelin]

One bit of the construction would be to get a short exact sequence of kernels, if the snake diagram has the right shape: i.e., the first "actual" row is short exact, and the first "actual" vertical map is an epi (so that the cokernel vanishes, and δ becomes the zero map. I sketched this construction, but it still has some sorries.

[Riccardo Brasca]

I've proved

lemma ker_row₁_to_row₂ (hD : is_snake_input D) :
  (kernel.ι ((1,0) ⟶[D] (1,1))) ≫ ((1,0) ⟶[D] (2,0)) = 0 :=

From here it should be easy to define

def long_row₀ (hD : is_snake_input D) : kernel ((1,0) ⟶[D] (1,1)) ⟶ D.obj (0, 0) := sorry

but I am little bit lost in the library. If someone wants to contribute please go ahead. The proof of the exactness should be easy using pseudoelements.

[Adam Topaz]

To construct this, you probably need to identify D.obj (0,0) with ker ((1,0) \hom[D] (2,0)) and compose that with ker.map or ker.\iota and ker.lift

[Adam Topaz]

I can construct this later today

[Riccardo Brasca]

Yes, the math is clear. I just don't know which is the best path in Lean. Using subobjects? There is docs#category_theory.abelian.is_limit_image' that probably says that the image has the universal property of the kernel, but I don't know what a fork is :)

[Adam Topaz]

Oh, what I mean is that I think the path I sketched above is the best path ;)

[Adam Topaz]

I really don't like subobjects, but maybe I just haven't suffered enough in trying to use them

[Adam Topaz]

The point is that the universal property of the kernel lets you define a map from D.obj (0,0) to the kernel of (1,0) -> (2,0), and pseudoelements can hhelp you prove that this map is an isomorphism.

[Riccardo Brasca]

I'm asking because I don't see in mathlib that ker g is isomorphic to image f if exact f g (at least, not explicitly), and usually when such a basic fact is missing is just because it is formulated in a more general way.

[Riccardo Brasca]

Ah, I see what you mean, proving directly that this map is an iso!

[Adam Topaz]

Take a look for example at what I did in the other corner of the diagram :)
https://github.com/leanprover-community/lean-liquid/blob/f7435bcd76bb16f1a2748830b59f7999860d35d0/src/for_mathlib/snake_lemma.lean#L859

[Riccardo Brasca]

So exactness should follow immediately, nice!

[Adam Topaz]

(I have to teach now, but I'll be back later)

[Riccardo Brasca]

I have to stop for today :unamused:

[Adam Topaz]

Something's broken in for_mathlib/snake_lemma.lean...

[Adam Topaz]

Oh, nevemind. I just had to get the correct mathlib version

[Adam Topaz]

@Riccardo Brasca I replaced epi_iff_exact_zero_right' with docs#category_theory.abelian.tfae_epi in the epi proof for kernel_sequence, which fixed the error in for_mathlib/snake_lemma.

[Johan Commelin]

Merci. I didn't know about that tfae_epi

[Adam Topaz]

Me neither! I went to prove it for a mathlib PR and there it was!

[Adam Topaz]

the same file also has the useful docs#category_theory.abelian.exact_cokernel but it's missing the analogue for kernels.

[Riccardo Brasca]

I've added

def ker_row₁_to_top_left (hD : is_snake_input D) : kernel ((1,0) ⟶[D] (1,1)) ⟶ D.obj (0, 0) :=
by { letI := hD.col_mono 0, exact (limits.kernel.lift _ _ (ker_row₁_to_row₂ hD)) ≫
    (limits.kernel.lift _ _ (((abelian.exact_iff _ _).1 (hD.col_exact₁ 0)).2)) ≫
    inv (abelian.images.factor_thru_image ((0,0) ⟶[D] (1,0))) }

The map from the first kernel of the second row to the top left element. This become zero when composed with (0,0) ⟶[D] (0,1), but to prove this I need

lemma ker_row₁_to_top_left_comp_eq_ι (hD : is_snake_input D) : ker_row₁_to_top_left hD ≫
  ((0,0) ⟶[D] (1,0)) = kernel.ι ((1,0) ⟶[D] (1,1))

I am not sure the definition of ker_row₁_to_top_left is the best one, it goes through docs#category_theory.abelian.images.is_iso_factor_thru_image that complicates life a little. If someone wants to prove ker_row₁_to_top_left_comp_eq_ι (even changing ker_row₁_to_top_left ) please go ahead. I will resume working on this in one or two hours.

[Riccardo Brasca]

Adam Topaz said:

the same file also has the useful docs#category_theory.abelian.exact_cokernel but it's missing the analogue for kernels.

The dual is docs#category_theory.exact_kernel_ι, isn't it?

[Adam Topaz]

Yes!

[Riccardo Brasca]

I've extended the snake to the left: ker_row₁_to_top_left: kernel ((1,0) ⟶[D] (1,1)) ⟶ D.obj (0,0) is a mono, and exact (ker_row₁_to_top_left hD) ((0,0) ⟶[D] (0,1)), in particular if (1,0) ⟶[D] (1,1) is a mono then (0,0) ⟶[D] (0,1) is a mono.

[Riccardo Brasca]

The dual statement should have the same proof.

[Johan Commelin]

It's not as readable as I would like, but it works:

lemma six_term_exact_seq (hD : is_snake_input D) :
  exact_seq 𝒜 [(0,0) ⟶[D] (0,1), (0,1) ⟶[D] (0,2), hD.δ, (3,0) ⟶[D] (3,1), (3,1) ⟶[D] (3,2)] :=
begin
  refine exact_seq.cons _ _ hD.row_exact₀ _ _,
  refine exact_seq.cons _ _ hD.exact_to_δ _ _,
  refine exact_seq.cons _ _ hD.exact_from_δ _ _,
  refine exact_seq.cons _ _ hD.row_exact₃ _ _,
  refine exact_seq.single _,
end

[Adam Topaz]

I think it looks quite good actually!

[Adam Topaz]

We could develop some API for exact_seqsimilar to all the stuff we have for tfae.

[Johan Commelin]

I just wrote a congr lemma for it.

[Johan Commelin]

lemma six_term_exact_seq {C : Type*} [category C] [abelian C]
  (n : ℕ) (A : chain_complex (short_exact_sequence C) ℕ) :
  exact_seq C [
    (homology_functor _ _ (n+1)).map ((Fst_Snd C).app A), -- Hⁿ⁺¹(A₁) ⟶ Hⁿ⁺¹(A₂)
    (homology_functor _ _ (n+1)).map ((Snd_Trd C).app A), -- Hⁿ⁺¹(A₂) ⟶ Hⁿ⁺¹(A₃)
    δ n A,                                                -- Hⁿ⁺¹(A₃) ⟶ Hⁿ(A₁)
    (homology_functor _ _ n).map ((Fst_Snd C).app A),     -- Hⁿ(A₁)   ⟶ Hⁿ(A₂)
    (homology_functor _ _ n).map ((Snd_Trd C).app A)      -- Hⁿ(A₁)   ⟶ Hⁿ(A₃)
  ] :=
begin
  have key := (snake_input n A).2.six_term_exact_seq,
  dsimp only [snake_input, snake_diagram,
    snake_diagram.mk_functor'', snake_diagram.mk_functor'] at key,
  refine exact_seq.congr key _, clear key,
  iterate 5 { refine exact_seq.arrow_congr.cons _ _, rotate },
  { apply exact_seq.arrow_congr.nil },
  { apply snake_diagram.mk_functor_map_f0 },
  { apply snake_diagram.mk_functor_map_g0 },
  { refl },
  { apply snake_diagram.mk_functor_map_f3 },
  { apply snake_diagram.mk_functor_map_g3 },
end

[Johan Commelin]

The six term exact sequence for a "chain complex of short exact sequences" = "short exact sequence of chain complexes".

[Riccardo Brasca]

I've added bottom_right_to_coker_row₂ : D.obj (3, 2) ⟶ cokernel ((2,1) ⟶[D] (2,2)), the last map in the "long snake". I don't think I will have time to work on it tomorrow, so if someone wants to prove that it is an epi and exactness in the last step please go ahead, The proofs should be similar to those of ker_row₁_to_top_left_mono and long_row₀_exact.

[Johan Commelin]

Thanks!

[Riccardo Brasca]

I've proved long_row₃_exact. So the snake is an exact sequence of 10 terms (the first and the last are 0).

[Riccardo Brasca]

So this

lemma eight_term_exact_seq (hD : is_snake_input D) :
  exact_seq 𝒜 [hD.ker_row₁_to_top_left, (0,0) ⟶[D] (0,1), (0,1) ⟶[D] (0,2),
  hD.δ,
  (3,0) ⟶[D] (3,1), (3,1) ⟶[D] (3,2), hD.bottom_right_to_coker_row₂] :=
begin
  refine exact_seq.cons _ _ hD.long_row₀_exact _ _,
  refine exact_seq.cons _ _ hD.row_exact₀ _ _,
  refine exact_seq.cons _ _ hD.exact_to_δ _ _,
  refine exact_seq.cons _ _ hD.exact_from_δ _ _,
  refine exact_seq.cons _ _ hD.row_exact₃ _ _,
  refine exact_seq.cons _ _ hD.long_row₃_exact _ _,
  refine exact_seq.single _,
end

works well. I tried to add the zero at the beginning, but Lean is not happy and wants has_zero (arrow 𝒜).

[Adam Topaz]

I think if you pass in (0 : 0 \hom ??) for the correct ??, it will work (there is a coercion from morphisms to arrows)

[Adam Topaz]

E.g.

local attribute [instance] limits.has_zero_object.has_zero

lemma eight_term_exact_seq (hD : is_snake_input D) :
  exact_seq 𝒜 [
    (0 : 0 ⟶ kernel ((1,0) ⟶[D] (1,1))),
    hD.ker_row₁_to_top_left, (0,0) ⟶[D] (0,1), (0,1) ⟶[D] (0,2),
    hD.δ,
    (3,0) ⟶[D] (3,1), (3,1) ⟶[D] (3,2), hD.bottom_right_to_coker_row₂,
    (0 : cokernel ((2,1) ⟶[D] (2,2)) ⟶ 0)] :=
begin
  sorry,
  /-
  refine exact_seq.cons _ _ hD.long_row₀_exact _ _,
  refine exact_seq.cons _ _ hD.row_exact₀ _ _,
  refine exact_seq.cons _ _ hD.exact_to_δ _ _,
  refine exact_seq.cons _ _ hD.exact_from_δ _ _,
  refine exact_seq.cons _ _ hD.row_exact₃ _ _,
  refine exact_seq.cons _ _ hD.long_row₃_exact _ _,
  refine exact_seq.single _,
  -/
end

[Adam Topaz]

I added the zeros :) (and pushed)

[Johan Commelin]

Nice!

[Riccardo Brasca]

I don't see the difference with what I wrote, but your code works :)
We now have ten_term_exact_seq, eight_term_exact_seq, and six_term_exact_seq.

[Adam Topaz]

I added the local [instance] too :) That may have been missing?

[Riccardo Brasca]

Maybe... it's time to go to bed for me

[Riccardo Brasca]

Do we need naturality of the snake somewhere?

[Johan Commelin]

I don't think so

[Johan Commelin]

You know these 1-picture-proofs of Pythagoras? Like https://betterexplained.com/wp-content/uploads/2016/10/pythagorean-proof.png

https://www.3blue1brown.com/content/blog/exact-sequence-picturebook/PuzzlingThroughExactSequences.pdf by Ravi Vakil contains a proof of the snake lemma (page 23) in one picture.

[Adam Topaz]

:lizard: