long exact sequence

Stream: condensed mathematics

[Johan Commelin]

Let's recap where we are concerning homological algebra / long exact sequences. A subset of what is left to do:

• LES specialized to Ext. This will need a bit of glue, jumping through opposite categories.
• Ext where the first argument is a complex. It seems that @Adam Topaz and @Matthew Ballard started working towards this, with homological functors. Lean knows that Hom(_, V) is a homological functor.
• Projective replacements. @Andrew Yang told me that he might start working on this tomorrow.

[Adam Topaz]

Correction: Lean knows that Hom(X,-) is homological :)

[Johan Commelin]

Ooh! Thanks for correcting.

[Adam Topaz]

This is an important distinction, since we will need to take projective replacements of X in Hom(X,-).

[Johan Commelin]

• The degree-0-part of the LES.

[Riccardo Brasca]

The natural isomorphism (F.left_derived 0) ≅ F

def left_derived.zero_iso_self [enough_projectives C] [preserves_finite_colimits F] :
  (F.left_derived 0) ≅ F :=

is sorry free. Given that we have the long exact sequence for F.left_derived 0, the long exact sequence for involving F should now be really easy (and I mean Lean-easy). I will do it later today or tomorrow.

[Riccardo Brasca]

Moreover this only uses Adam's recent PR, so it can go directly to mathlib, and then it will be someone else's job to maintain it .

[Riccardo Brasca]

Hmm, this is not completely true

[Adam Topaz]

I think the only other ingredient is that thing about the cokernel we did last week, right?

[Riccardo Brasca]

I used some formalism about exact_seq, that it's not in mathlib. But translating it to only use exact should be trivial.

[Johan Commelin]

I think exact_seq has proven to be quite useful and flexible. So maybe it's time to move it to mathlib.

[Riccardo Brasca]

I just noted that I can write

lemma seven_term_exact_seq [enough_projectives C] (A : short_exact_sequence C) :
  exact_seq D [
    (F.left_derived 1).map A.f, (F.left_derived 1).map A.g,
    δ F 0 A,
    F.map A.f, F.map A.g, (0 : F.obj A.3 ⟶ F.obj A.3)] :=

and Lean does not complain. Is this intended? Note that δ F 0 A : (F.left_derived (0 + 1)).obj A.3 ⟶ (F.left_derived 0).obj A.1 and F.map A.f : F.obj A.1 ⟶ F.obj A.2, so the two cannot be composed (they really cannot, not just because of some type theory thing).

[Johan Commelin]

This is an unfortunate side effect of exact_seq.

[Johan Commelin]

So you will not be able to prove that lemma.

[Riccardo Brasca]

Sure, I didn't want to prove it (I will prove the true one, with a modified δ). I was surprised I was able to state it.

[Johan Commelin]

The way it is defined, you can only prove exact_seq L for lists L that are "well-formed": the maps must compose correctly.

[Johan Commelin]

Well, L needs to have type list (arrow 𝒜). So it's really just a list of morphisms, without any conditions on domains / codomains.

[Yaël Dillies]

Would something like docs#simple_graph.walk avoid this weirdness?

[Johan Commelin]

I think that we would end up fighting DTT more than it would help us

[Riccardo Brasca]

If a proof of exact_seq means what I have in mind I am happy with that. docs#category_theory.exact is already complicated enough...

[Adam Topaz]

Does anyone see a quick way to prove the following?

lemma _root_.category_theory.cochain_complex.exact_cone_in_cone_out
  (X Y : cochain_complex A ℤ) (f : X ⟶ Y) :
  exact ((_root_.homology_functor _ _ 0).map (cone.in f))
    ((_root_.homology_functor _ _ 0).map (cone.out f)) :=
begin
  sorry
end

[Adam Topaz]

This is more-or-less the last thing left to obtain the triangular LES for homology

[Johan Commelin]

@Adam Topaz which file is that in? I haven't used the new homology API yet, but I'm happy to take a look

[Adam Topaz]

for_mathlib/derived/K_projective

[Adam Topaz]

If the following (rotated)variant is easier...

lemma _root_.category_theory.cochain_complex.exact_to_cone_in
  (X Y : cochain_complex A ℤ) (f : X ⟶ Y) :
  exact ((_root_.homology_functor _ _ 0).map f)
    ((_root_.homology_functor _ _ 0).map (cone.in f)) :=
begin
  sorry
end

I could make the proof work with that as well

[Andrew Yang]

If we know that additive functors preserves split exact-ness, we have cone.termwise_split in mapping_cone.lean.

[Riccardo Brasca]

We know that.

[Riccardo Brasca]

It's somewhere in the project

[Johan Commelin]

We have

src/for_mathlib/short_exact_sequence.lean:def map_short_exact_sequence_of_split

which is for bundled SES's

[Riccardo Brasca]

lemma seven_term_exact_seq [enough_projectives C] [preserves_finite_colimits F]
  (A : short_exact_sequence C) :
  exact_seq D [
    (F.left_derived 1).map A.f, (F.left_derived 1).map A.g,
    δ₀ F A,
    F.map A.f, F.map A.g, (0 : F.obj A.3 ⟶ F.obj A.3)]

is done.

[Johan Commelin]

Andrew Yang said:

If we know that additive functors preserves split exact-ness, we have cone.termwise_split in mapping_cone.lean.

Do we know that exactness is something that can be checked termwise?

[Johan Commelin]

@Adam Topaz I pushed some miniwip

[Adam Topaz]

I have to do some admin stuff for a little while :sad: but I'll try to take a look later

[Adam Topaz]

I should say that I don't know if the splitting is helpful here. This is essentially the exactness in the first three terms of the snake lemma, if it's set up properly.

[Johan Commelin]

Yeah, I didn't think properly about the maths. I agree that this should essentially follow from the LES for homology that is done in another file

[Adam Topaz]

I pushed a skeleton for this.
The sorrys are in for_mathlib/snake_lemma3 and the following in for_mathlib/derived/K_projective:

lemma _root_.category_theory.cochain_complex.exact_cone_in_cone_out
  (X Y : cochain_complex A ℤ) (f : X ⟶ Y) :
  exact ((_root_.homology_functor _ _ 0).map (cone.in f))
    ((_root_.homology_functor _ _ 0).map (cone.out f)) :=
begin
  haveI : exact ((cone.in f).f (-1)) ((cone.out f).f (-1)) := sorry,
  haveI : exact ((cone.in f).f 0) ((cone.out f).f 0) := sorry,
  haveI : exact ((cone.in f).f 1) ((cone.out f).f 1) := sorry,
  haveI : epi ((cone.out f).f (-1)) := sorry,
  haveI : epi ((cone.out f).f 0) := sorry,
  haveI : epi ((cone.out f).f 1) := sorry,
  haveI : mono ((cone.in f).f (-1)) := sorry,
  haveI : mono ((cone.in f).f 0) := sorry,
  haveI : mono ((cone.in f).f 1) := sorry,
  let S := snake.mk_of_homology Y (cone f) _ (cone.in _) (cone.out _),
  rw exact_iff_exact_seq,
  exact S.six_term_exact_seq.extract 3 4,
end

These should all be relatively straightforward.

[Johan Commelin]

I will take care of this.

[Johan Commelin]

It has basically all been done already. We just need the correct glue

[Adam Topaz]

There is one sorry left in snake_lemma3

[Adam Topaz]

Hmmmm.... I may need to change some of the kernels involved.

[Adam Topaz]

nevermind. it was fine. I just killed the last sorry in snake_lemma3

[Johan Commelin]

@Adam Topaz I refactored the LES for homology so that it now applies to arbitrary homological complexes (so chain and cochain complexes) indexed by arbitrary types (endowed with a complex_shape).
After that, proving your cochain_complex.exact_cone_in_cone_out was a 3-liner.

[Adam Topaz]

Awesome! Although it seems like you suffered a bit in for_mathlib/les_homology.lean, judging by some of the names there :wink:

[Johan Commelin]

All the suffering was already present in the case of chain_complex C ℕ.

[Adam Topaz]

Ah!

[Adam Topaz]

Well, I'm all for deduplicating suffering

[Riccardo Brasca]

If nobody has objections I will see tomorrow if it is reasonable to PR the natural iso from left_derived 0 F to F.

[Johan Commelin]

Sounds good to me.

[Riccardo Brasca]

@Adam Topaz I think you forgot to merge your #12171 after Scott delegated it to you...

[Adam Topaz]

Oops! I'll do it in a few hours.

[Riccardo Brasca]

#12403