Using the LTE snake lemma

Stream: maths

[Brendan Seamas Murphy]

I'm trying to prove the following result:

lemma coker_of_quasi_isos_between_monic_arrows_is_quasi_iso [abelian V]
  {A B X Y : homological_complex V c}
  (i : A ⟶ X) (j : B ⟶ Y)
  (hi : mono i) (hj : mono j)
  (g : A ⟶ B) (f : X ⟶ Y)
  (hg : quasi_iso g) (hf : quasi_iso f)
  (w : g ≫ j = i ≫ f)
  : quasi_iso ((coker_functor (homological_complex V c)).map (arrow.hom_mk w : arrow.mk i ⟶ arrow.mk j)) := sorry

It seems like the right way to do this is to use homological_complex.six_term_exact_seq, then use a lemma proving naturality of the connecting homomorphism, then use short_exact_sequence.snd_is_iso (the five lemma). Is there a result already in LTE that gives the missing step?

[Adam Topaz]

We certainly have the snake lemma and the naturality of the connecting morphism in LTE (along with 37 other variants...).

[Adam Topaz]

What exactly do you mean by "the missing step"?

[Brendan Seamas Murphy]

Sorry, I mean that if you have morphism of short exact sequences of chain complexes then you get a commutative ladder diagram for the LES in homology (or more specifically between the truncation of the LES given by six_term_exact_sequence)

[Brendan Seamas Murphy]

6e40a9fa-bd80-4829-9554-5e6fed804dbe.png

[Brendan Seamas Murphy]

So given monic arrows i : A -> X and j : B -> Y and a morphism between them in the arrow category, I want this commutative diagram with exact rows

[Brendan Seamas Murphy]

(where q is after p in the complex shape)

[Adam Topaz]

Is this not just the naturality of $\delta$ in the snake lemma? Everything else should just be natural "for free".

[Brendan Seamas Murphy]

Yep, I'm just not sure what the actual lemma saying delta is natural is

[Brendan Seamas Murphy]

oh, it's under snake_lemma_naturality isn't it. For some reason I thought there would be a difference between naturality of the connecting homomorphism for the general snake lemma and for the special case of the LES in homology

[Brendan Seamas Murphy]

oh wait or is this what's done in snake_lemma_naturality2?

[Adam Topaz]

Like I said... we have 37 variants :rofl:

[Adam Topaz]

I think https://github.com/leanprover-community/lean-liquid/blob/17f13b74d4bc045e82465f86f5705a3f6e1994e3/src/for_mathlib/snake_lemma_naturality2.lean#L188 is the closest we have in LTE to the statement you want.

[Brendan Seamas Murphy]

I think this should give me exactly what I want! thanks so much

[Brendan Seamas Murphy]

...except the arrow category in mathlib is defined as a comma category and not the functor category from the walking arrow

[Brendan Seamas Murphy]

So I guess I should show equivalence of those

[Brendan Seamas Murphy]

Related question: if I have an SES 0 -> A -> B -> C -> 0 of complexes and q is an index with c.next q = none, how can I get that the sequence H_q(A) -> H_q(B) -> H_q(C) -> 0 is exact? this is true, right? Just add another element to the indexing after q and extend these complexes by 0?

[Johan Commelin]

@Brendan Seamas Murphy Are you depending on LTE? Or only mathlib?

[Johan Commelin]

There is a lot of machinery in LTE that hopefully will move to mathlib in the next few months.

[Johan Commelin]

In the c.next q = none case, I guess it is best to identify homology with a cokernel and then conclude that you get an epi on the right.

[Brendan Seamas Murphy]

On LTE, and wow, that's obvious in hindsight

[Johan Commelin]

There's an enormous amount of stuff about homology_iso_datum and has_homology that might be helpful with those identifications.

[Johan Commelin]

Also, identifying a derived functor in degree 0 with the functor that is being derived is already part of mathlib.

[Brendan Seamas Murphy]

Oh neat

[Brendan Seamas Murphy]

Do mathlib or LTE have that a functor which sends short exact sequences to right exact sequences is right exact (sends right exact sequences to right exact sequences)? I couldn't find it but wanted to check before proving it myself

[Johan Commelin]

I guess not. Note that we've been spelling right exactness as preserves_finite_colimits.

[Joël Riou]

In LTE's for_mathlib/exact_functor.lean, there are statements about exact functors (in the sense that they preserves short exact sequences): they preserve finite colimits and finite limits. From the code in this file, it should not be too hard to split the exactness assumption into only right exactness (resp. only left exactness) and obtain more equivalent characterizations.

[Brendan Seamas Murphy]

I've shown that taking the cokernel (considered as a functor on the arrow category) is right exact and I want to deduce from this that homology at a terminal index (ie 0th homology for N graded chain complexes) is right exact, by identifying the homology of A at i with the cokernel of A.d_from i. Is this easily doable with stuff from homology_iso_datum and has_homology? I tried reading through but didn't totally understand what was going on

[Brendan Seamas Murphy]

Note that the identification H_i(A) ≈ coker(A.d_from i) must be natural in A in order to deduce right exactness of H_i from right exactness of coker

[Brendan Seamas Murphy]

7a1d76d8-d87a-406c-aec1-0629388d9b20.jpg

[Brendan Seamas Murphy]

I was able to manually define a projection A -> H_i(A) but I get a very spooky goal when I try to show naturality

[Adam Topaz]

I would use homology.map_eq_lift... and homology.hom_to_ext (or something like that) to make some progress.

[Adam Topaz]

Oh no, you used homology.\pi instead of homology.\pi' GOOD LUCK!

[Adam Topaz]

Also, what's going on with those eq_to_homs? They might cause you some troubles

[Adam Topaz]

Here's some code that I hope will be helpful

import algebra.homology.homology
import category_theory.abelian.homology

open category_theory
open category_theory.limits
variables {A : Type*} [category A] [abelian A] (X : homological_complex A (complex_shape.down ℕ))

noncomputable theory

def homology_iso_cokernel :
  X.homology 0 ≅ cokernel (X.d_to 0) :=
{ hom := homology.desc' _ _ _ (kernel.ι _ ≫ cokernel.π _) $ by simp,
  inv := cokernel.desc _ (homology.lift _ _ _ (cokernel.π _) $ by simp) $ begin
    apply homology.hom_to_ext,
    simp,
  end,
  hom_inv_id' := begin
    apply homology.hom_from_ext,
    apply homology.hom_to_ext,
    simp,
  end,
  inv_hom_id' := begin
    apply coequalizer.hom_ext,
    simp,
    let t := _, change _ ≫ t = _,
    have ht : t = homology.ι _ _ _,
    { apply homology.hom_from_ext, simp, },
    simp [ht],
  end }

def homology_iso_cokernel_natural {X Y : homological_complex A (complex_shape.down ℕ)}
  (f : X ⟶ Y) :
  (homology_iso_cokernel X).hom ≫ cokernel.map _ _ (f.prev _) (f.f _) (by simp) =
  (homology_functor _ _ _).map f ≫ (homology_iso_cokernel Y).hom :=
begin
  dsimp [homology_iso_cokernel],
  apply homology.hom_from_ext,
  simp,
end

[Brendan Seamas Murphy]

This looks much better haha

[Brendan Seamas Murphy]

It's been difficult trying to understand how the whole homological algebra API works and how you're supposed to use it. I wish I had started asking questions here earlier

[Adam Topaz]

Keep in mind that we're gearing up for a big refactor in mathlib's homology based on what we learned from LTE, so the "official" api is likely to change in the next few weeks.

[Brendan Seamas Murphy]

That's good to hear, it hasn't felt super user friendly

[Brendan Seamas Murphy]

Last question (hopefully) before I finish out this homological algebra stuff: say I have a ladder diagram where the vertical maps are isomorphisms and an exact_seq [f_1, ..., f_n] where the f_i are the maps on the top row. how can I get the corresponding exact_seq for the bottom row?

[Brendan Seamas Murphy]

I assume this was needed at some point in LTE...

[Brendan Seamas Murphy]

I see that there's a lemma category_theory.preadditive.exact_of_iso_of_exact' in mathlib for the n = 2 case, so it should be pretty easy to prove inductively if I have to

[Adam Topaz]

I don't remember whether we have a way to transport exact_seq along isomorphisms...

[Brendan Seamas Murphy]

Something I'll try to pr in after I finish this project and start working on a bunch of prs

[Adam Topaz]

If we do then it would be somewhere in for_mathlib/exact_seq* (* = wildcard)

[Brendan Seamas Murphy]

(assuming exact_seq is coming in the rewrite of the homological algebra api)

[Adam Topaz]

We still need to port exact_seq to mathlib :-/

[Adam Topaz]

It would be nice if we can come up with a version of exact_seq that has a category structure, so we could talk about such ladder diagrams simply as morphisms in some category. But that's not really possible with the current implementation of exact_seq

[Brendan Seamas Murphy]

well, one way to do what I was suggesting is to reinterpret the sequences as chain complexes and then use the fact that an isomorphism of chain complexes descends to an iso in homology. I'm not really sure what category this should happen in other than like chain_complex V (fin n)

[Brendan Seamas Murphy]

Or are you thinking of a category which has exact sequences of length n for all finite n?

[Brendan Seamas Murphy]

Verified :tada:. I should have excision done by tonight

[Adam Topaz]

Nice!

[Johan Commelin]

@Brendan Seamas Murphy excision of what? Now I'm curious!!

[Brendan Seamas Murphy]

Singular homology!

[Johan Commelin]

That's cool!

[Brendan Seamas Murphy]

The work so far is here: https://github.com/Shamrock-Frost/BrouwerFixedPoint

[Brendan Seamas Murphy]

(warning: it is very bad code. I had a 1 month deadline that's nearing the end and it got sloppy at the end)

[Johan Commelin]

You are basing your work on a project that got very very sloppy at the end as well :see_no_evil:

[Brendan Seamas Murphy]

It's so tempting when it feels like you'll get it any day now...

[Brendan Seamas Murphy]

Excision tonight may have been a bit ambitious, but definitely tomorrow! Literally the only part of the argument I have to do is shuffling around the chain complexes and applying the second isomorphism theorem, all the hard homological algebra and topology is complete :)

[Brendan Seamas Murphy]

Definitely tomorrow was also too ambitious... But soon. I have the main proof of excision complete but it relies on three sorry'd out lemmas (the identity (M+N)/M = N/(M ∩ N) in an abelian category and criterions for checking certain squares of modules are pullbacks/pushouts)

[Brendan Seamas Murphy]

Proof of excision is complete!!! Calculating H_n(S^n) and deducing the Brouwer Fixed Point theorem should be easy from here :)

[Patrick Massot]

Brendan Seamas Murphy said:

should be easy from here :)

Famous last words :grinning_face_with_smiling_eyes:

[Damiano Testa]

It feels like when I read "Clearly,..." in math papers.

[Kevin Buzzard]

If that's a proof that the definition of singular homology that you currently have is usable, then can you PR the definition? It would be great for lean to finally have a homology/cohomology theory

[Guillermo Martin]

I could take on trying to implement singular cohomology

[Kevin Buzzard]

My feeling is that if people feel confident that they know the correct Lean implementation of a mathematical definition should be then they should PR it even if they don't have time to develop an API for it. One of my longer term goals with Lean is to get mathlib into a position where it's thought of as "normal" that it can state a theorem from modern research mathematics, and definitions are the key stumbling block here.

[Junyan Xu]

Singular homology in Lean is definitely an important milestone. Congratulations! Would be nice to compare with the HOL story.

[Brendan Seamas Murphy]

Definitely planning to PR, I just wanted to get to a certain point on my own before then. It's also going to be a little annoying because of some issues with the simplex category in mathlib which I'd like to fix in the PR (there's universe issues with the singular simplicial set functor and also I think the standard cosimplicial object in Top should be defined using std_simplex, which is how I do it in this project)

[Kevin Buzzard]

Don't change too many things at once in the first PR.