LES for Ext

Stream: condensed mathematics

[Johan Commelin]

We'll also need LES for Ext groups (in the first variable). Does that sound like something you want to work on?

[Riccardo Brasca]

Sure! I can really work on anything we need. To be honest I don't understand very well how difficult it is, for example this is something we will surely want in mathlib at some point, but maybe proving it in general for derived functors is much more difficult?

[Johan Commelin]

I think it will not make much of a difference.

[Johan Commelin]

But mathlib still doesn't have the snake lemma. I think that's a bigger problem for getting the LES.

[Riccardo Brasca]

I don't think I've ever seen a real proof of the snake lemma (I mean a proof that does not go through Mitchell's embedding theorem), but this one seems quite short. It works if the category has enough projectives, but maybe this is enough for our applications.

[Johan Commelin]

@Markus Himmel What's the status of snake in lean?

[Johan Commelin]

@Riccardo Brasca Sure, for now assuming enough projectives is fine.

[Johan Commelin]

@Riccardo Brasca maybe we should start by defining δ-functors, somewhere in for_mathlib.

[Johan Commelin]

Then we claim that Ext is an example of a δ-functor. And that splits the problem into two pieces: (i) develop an API for δ-functors, and (ii) fill in the sorry that Ext is indeed an example.

[Matthew Ballard]

docs#category_theory.abelian.pseudoelement might be helpful

[Markus Himmel]

Regarding the snake lemma: there is a proof that works in all abelian categories in Borceux Vol 2 and also in PTJs category theory notes (which I am afraid are not public). Getting one of them in Lean is basically just a matter of sitting down and doing it, but it will be long and not particularly pretty. Part of that is simply due to the fact that the statement of the snake lemma is very long. I have a version of Borceux' proof at github.com/twofx/lean-homological-algebra, but it uses custom tactics which are far from mathlib-ready, so it is almost certainly faster to start from scratch with one of the two proofs. It is very unlikely that I will have time to tackle this anytime soon. Borceux' proof uses pseudoelements while Johnstone's proof is arrow-theoretic. We habe pseudoelements, but Johnstone's proof is shorter, so it might be the way to go, but it's hard to tell without trying both ways.

[Riccardo Brasca]

Yes, that's the right thing to do. In any case we need the LES to check that derived functors are δ-functors

[Johan Commelin]

@Markus Himmel is your repo building with recent mathlib?

[Markus Himmel]

Almost certainly not

[Johan Commelin]

If so, maybe we could dump the proof terms that your tactics spit out, and plug those into LTE.

[Riccardo Brasca]

I just carefully checked the proof of the snake lemma I linked above, and I am pretty confident it's doable in one or two weeks (depending on how complete is the library for abelian categories). It works if the category has enough projectives (or enough injectives).

[Johan Commelin]

In our case, we do have enough projectives. So maybe that's the best approach for LTE.

[Riccardo Brasca]

Ah, I didn't think about naturality of the morphism. I don't remember if this is more or less automatic or not

[Riccardo Brasca]

@Markus Himmel How one construct the connecting morphism using pseudoelements? I've always thought one can use them to check that a given morphism is zero or similar stuff, but not not produce one. And the main difficulty of the snake lemma is usually to construct δ rather then the exacteness.

[Matthew Ballard]

I couldn't find the cone complex in docs#homotopy_category. Is that in mathlib?

[Johan Commelin]

I don't think so

[Johan Commelin]

Relevant link: https://pp.ipd.kit.edu/uploads/publikationen/himmel20bachelorarbeit.pdf is Markus's BSc thesis on diagram chasing in Lean

[Matthew Ballard]

I am not sure about the feasibility at the moment (but it works for my graduate class in a day) is to prove that $K^-(\mathcal A)$ satisfies TR1 - TR3 for a triangulated category (which need to be stated). The fact that $\operatorname{Hom}(A,-)$ or $\operatorname{Hom}(-,A)$ takes triangles to LESs is very quick from that.

[Matthew Ballard]

There are categories of triangles already docs#triangulated but not any axioms.

[Matthew Ballard]

A triangle in the homotopy category is anything isomorphic to a triangle of the form

$$A \overset{\phi}{\to} B \to C(\phi) \to A[1]$$

[Matthew Ballard]

Almost certainly the most work would got into checking that "rotation axiom" TR2.

[Matthew Ballard]

This way the natural maps in the $\delta$-functor come from the maps in the triangle + naturality of Hom.

[Markus Himmel]

@Riccardo Brasca the connecting homomorphism is constructed via universal properties. IIRC, in the two proofs I cited above this is actually the easier half of the argument.

[Johan Commelin]

I think we need the LES for Ext in 3 or 4 places in LTE. So we should probably prioritize getting the statement formalized.

[Johan Commelin]

Maybe we should push for this LES now that snake is finished. The file horseshoe.lean contains a half-hearted attempt at the horseshoe construction.

[Johan Commelin]

I finished the horseshoe construction, although the columns aren't yet tied to ProjectiveResolution.

[Johan Commelin]

But I feel like we are now zoning in fast on the LES for derived functors.

[Johan Commelin]

lemma six_term_exact_seq (n : ℕ) (A : short_exact_sequence C) (B : C) :
  exact_seq (Module.{v} R) [
    ((«Ext» R C n).map A.g.op).app B, ((«Ext» R C n).map A.f.op).app B,
    δ R n A B,
    ((«Ext» R C (n+1)).map A.g.op).app B, ((«Ext» R C (n+1)).map A.f.op).app B
    ] :=
begin
  apply exact_seq.of_op,
  exact functor.left_derived.six_term_exact_seq _ n A,
end

[Johan Commelin]

This still depends on some sorries. Most notably exact f g → exact g.op f.op.

[Adam Topaz]

instance [exact f g] : exact g.op f.op :=
begin
  rw abelian.exact_iff,
  refine ⟨by simp [← op_comp], _⟩,
  apply_fun quiver.hom.unop,
  swap, { exact quiver.hom.unop_inj },
  simp,
end

[Adam Topaz]

(after adding the correct simp lemmas, of course ;) )

[Filippo A. E. Nuccio]

Oh great, I was planning to work a little bit on this of_op but it seems it has been unsorried. I am sorry for not being very active this week, I'm at a conference.

[Filippo A. E. Nuccio]

At any rate I will rather work on the SES with real measures.

[Riccardo Brasca]

So is there any sorry left for LES or you guys are really too fast? :grinning:

[Johan Commelin]

@Riccardo Brasca There are still 3 of them in horseshoe.lean

[Johan Commelin]

I haven't looked at them in the last few days. But I hope they are math-easy.

[Riccardo Brasca]

I will have a look

[Riccardo Brasca]

First sorry killed

[Riccardo Brasca]

I've done one and half of the last two sorry in horseshoe_is_projective_resolution₁. The last one is probably the more annoying, but it is just a matter of sitting down and unfolding all the definition I think. I will do it tomorrow if nobody wants to work on it.

[Johan Commelin]

Thanks so much. I will probably not have time to work on this tomorrow. Did you hit any pain points?

[Riccardo Brasca]

Not yet, but for the last sorry I will probably need eq_to_hom, so it's probably necessary to be a little careful

[Kevin Buzzard]

I bet you never realised that diagram chases were so difficult Riccardo ;-) Are these things in other systems? I remember looking at unimath once and just seeing a ton of category theory

[Riccardo Brasca]

OK, maybe this last lemma is a little painful... and I got the scary "motive is not type correct". I guess I really have to use eq_to_hom everywhere.

[Johan Commelin]

Hmm, this horseshoe construction is quite annoying.

[Johan Commelin]

I wonder if it was a good idea to do a hands-on definition of SES.

[Johan Commelin]

It would probably have been better to consider functors fin 3 ==> A (together with exactness conditions)

[Johan Commelin]

Because the sorry that is left, is only proving that the first column in the horseshoe construction is a proj resolution. And we'll have to repeat it for row 2 and 3. We can't quantify over fin 3. With the other definition, that would be possible.

[Johan Commelin]

Anyway, copy-paste isn't that hard either... so maybe it's not a very big problem.

[Riccardo Brasca]

Let me try a little bit. Maybe using pseudoelements was not a good idea

[Johan Commelin]

Well, this shouldn't really impact the horseshoe sorry.

[Johan Commelin]

And it will be a refactor that takes some time

[Johan Commelin]

Somehow this sorry should boil down to: exact f g following from: f factors through an epi onto the kernel of g.

[Johan Commelin]

Because that's basically how the f and g in this case are defined.

[Johan Commelin]

But since several constructions are pasted on top of this, it might not be so easy to apply that observation.

[Riccardo Brasca]

There must be something I don't understand about eq_to_hom (or something else). For example, do you why the following doesn't work?

  begin
    dsimp [horseshoe_to_single₁],
    erw [chain_complex.of_d, chain_complex.of_d],
    dsimp [horseshoe_d, horseshoe_step],

    set f := horseshoe_base_π (horseshoe_step A n).1,
    set g := (horseshoe_step A n).2.2.2.1,

    --now the goal is
    --exact (horseshoe_base_π (horseshoe_ker f) ≫ eq_to_hom _ ≫ horseshoe_ker_ι f).fst
    --(f ≫ eq_to_hom _ ≫ g).fst

    rw [short_exact_sequence.comp_fst], --this doesn't work

  end,

where

lemma comp_fst : (f ≫ g).1 = f.1 ≫ g.1 := rfl

[Johan Commelin]

Very strange.

[Johan Commelin]

@Riccardo Brasca This seems to work:

lemma aux {X Y Z W : C} (g : Y ⟶ Z) (h : Z ⟶ W) (f : X ⟶ kernel g) (i : kernel g ⟶ Y)
  (hf : epi f) (hh : mono h) (hi : i = kernel.ι g) :
  exact (f ≫ i) (g ≫ h) :=
sorry

lemma horseshoe_exact₁ (A : short_exact_sequence C) (n : ℕ) :
  exact (((homological_complex.Fst C).obj (horseshoe A)).d (n + 2) (n + 1))
    (((homological_complex.Fst C).obj (horseshoe A)).d (n + 1) n) :=
begin
  dsimp [horseshoe_to_single₁],
  erw [chain_complex.of_d, chain_complex.of_d],
  dsimp [horseshoe_d, horseshoe_step],

  set f := horseshoe_base_π (horseshoe_step A n).1,
  set g := (horseshoe_step A n).2.2.2.1,

  cases n;
  convert aux f.1 _ (horseshoe_base_π (horseshoe_ker f)).1 _ _ _ _ using 1,
end

[Johan Commelin]

Also, I think the cases n is crucial.

[Johan Commelin]

It might work as a first step in the original problem as well.

[Riccardo Brasca]

Ah yes, doing cases n makes rw short_exact_sequence.comp_fst working! I don't really understand why, but I am happy with your solution.

[Johan Commelin]

@Riccardo Brasca probably because

def horseshoe_to_single₁ :=
(chain_complex.to_single₀_equiv

is using a match on a natural number, under the hood

[Riccardo Brasca]

for_mathlib/horseshoe is sorry free.

[Johan Commelin]

Wow, that's awesome!

[Johan Commelin]

@Riccardo Brasca would you mind copy-pasting the final bit to show that Snd and Trd also give projective resolutions?

[Johan Commelin]

I think that should really be copy-pastable

[Riccardo Brasca]

Sure! But let me have a coffee first.

[Riccardo Brasca]

No problem for Trd, but Snd is different. I am maybe tired, but I don't see how to prove

instance epi_horseshoe_base_π_2 : epi (horseshoe_base_π A).2

[Johan Commelin]

hmm, I need to run, but I will think about it.

[Riccardo Brasca]

I mean, even with pen and paper it doesn't seem obvious. It's probably OK with elements, but I have to try

[Riccardo Brasca]

Ah, of course it is because of the snake lemma!

[Johan Commelin]

Yeah, I realised it just when I stepped in the car.

[Johan Commelin]

Now it will be interesting to see how easy it is to deduce this from the snake lemma in Lean.

[Johan Commelin]

Note that you can construct a snake_input from hom of SES.

[Johan Commelin]

mk_of_short_exact_sequence_hom

[Riccardo Brasca]

Yes, it's a good test for our API. We will need cokernel_sequence (currently we only have kernel_sequence), and things like epi f iff is_zero (cokernel f)

[Riccardo Brasca]

But I'm done for today :)

[Johan Commelin]

I think we could use six_term_exact_sequence and exact_seq.extract to get the relevant bit.

[Adam Topaz]

Can't you just use row_exact₃?

[Adam Topaz]

(with mk_of_short_exact_sequence_hom)

[Riccardo Brasca]

I just realized we already have docs#category_theory.abelian.epi_of_epi_of_epi_of_mono

[Johan Commelin]

tada!

[Riccardo Brasca]

It worked like a charm!

[Riccardo Brasca]

We now have the three projective resolutions.

[Johan Commelin]

Cool. Seems like we are very close to a sorry-free LES then!

[Riccardo Brasca]

I am trying to prove snake_diagram_is_snake_input in src/for_mathlib/homological_complex.lean, but I am getting again the "motive is not type correct" error.

lemma snake_diagram_is_snake_input (C : Type u) [category.{v} C] [abelian C]
  (A : chain_complex (short_exact_sequence C) ℕ) (n : ℕ) : is_snake_input (snake_diagram C n A) :=
  { row_exact₁ :=
    begin
      dsimp [snake_diagram, snake_diagram.mk_functor'', snake_diagram.mk_functor'],
      simp,

    --Now the goal is:
    --exact ((![homology_functor C (complex_shape.down ℕ) (n + 1), mod_boundaries_functor (n + 1),
    --cycles_functor C (complex_shape.down ℕ) n, homology_functor C (complex_shape.down ℕ) n] 1).map
    --(--(Fst_Snd C).app A)) ((![homology_functor C (complex_shape.down ℕ) (n + 1),
    --mod_boundaries_functor (n + 1), cycles_functor C (complex_shape.down ℕ) n,
    --homology_functor C (complex_shape.down ℕ) n] 1).map ((Snd_Trd C).app A))

    -- Note the ![homology_functor C (complex_shape.down ℕ) (n + 1), mod_boundaries_functor (n + 1),
    --cycles_functor C (complex_shape.down ℕ) n, homology_functor C (complex_shape.down ℕ) n] 1
    --that is not simplified



      have : ![homology_functor C (complex_shape.down ℕ) (n + 1), mod_boundaries_functor (n + 1),
        cycles_functor C (complex_shape.down ℕ) n, homology_functor C (complex_shape.down ℕ) n] 1 =
        mod_boundaries_functor (n + 1) := rfl,
    rw [this], --this fails with motive is not type correct
   end,
   row_exact₂ := sorry,
   col_exact₁ := sorry,
   col_exact₂ := sorry,
   col_mono := sorry,
   col_epi := sorry,
   row_mono := sorry,
   row_epi := sorry }

I didn't tried very hard to solve this, but it is maybe an indication that we did something wrong ? (I've tried cases n, just because it solved the problem in another lemma, but it doesn't work.)

[Johan Commelin]

    dsimp [snake_diagram, snake_diagram.mk_functor'', snake_diagram.mk_functor'],
    simp only [snake_diagram.mk_functor_map_g1, snake_diagram.mk_functor_map_f1],
    show exact ((mod_boundaries_functor (n+1)).map _) ((mod_boundaries_functor (n+1)).map _),

works to get a reasonable goal state.

[Johan Commelin]

@Riccardo Brasca Maybe we should wait with these sorries.

[Johan Commelin]

The point is: for the BD lemma we'll need triangles like $\tau_{\ge i+1}C \to \tau_{\ge i} C \to H_i(C)[i]$, and we will also need long exact sequences for those.

[Johan Commelin]

So I think we should tell Lean what the distinguished triangles in the homotopy category are, and get a LES for those.

[Johan Commelin]

Maybe that will boil down to this same lemma, but I'm not sure if it will be defeq the same lemma.

[Johan Commelin]

The relevant sections of the stacks project seem to be https://stacks.math.columbia.edu/tag/014D and https://stacks.math.columbia.edu/tag/014P

[Riccardo Brasca]

Ah OK, if we need it in greater generality I agree it's better to wait.

[Johan Commelin]

I have a construction of the mapping cone. But not yet the map that completes the triangle, because we don't yet have an instance of has_shift (homological_complex A c)

[Johan Commelin]

Pushed

[Johan Commelin]

About this shift: there seem to be several conventions. Is there an orthodox convention that unifies chain complexes and cochain complexes?

[Johan Commelin]

https://doc.sagemath.org/html/en/reference/homology/sage/homology/chain_complex.html#sage.homology.chain_complex.ChainComplex_class.shift says that the shift always goes in the opposite direction as the differential

[Johan Commelin]

But I have no idea if this is an accepted standard. I think that https://stacks.math.columbia.edu/tag/0119 does something else

[Riccardo Brasca]

I am always confused by this, but usually at the end I expect that, $H^i(\mathcal{F}[-i]) = H^0(\mathcal{F})$.

[Johan Commelin]

I guess that follows the Stacks convention. But the Sage convention only agrees for one of the two: chain or cochain complexes. (I didn't yet check which one, because I'm also confused.)

[Johan Commelin]

But if we want a triangle

$$A \xrightarrow{f} B → \text{Cone}(f) → A[1]$$

for both chain and cochain complexes, then I guess this forces what the shift should be, right?

[Johan Commelin]

And we probably want the homotopy category of both versions to be a triangulated category in the end.

[Riccardo Brasca]

Stack project says that the homotopy category is built using cochain complexes. I have no idea if there is some convention that works only in this case.

[Riccardo Brasca]

In my opinion following them is a good idea: they are aware of these annoyances and we can be reasonably sure what they say is really correct, and not only correct up to sign or something

[Riccardo Brasca]

There is also this :face_palm:

[Johan Commelin]

@Riccardo Brasca Great! That's a useful link!

[Patrick Massot]

What a nice read when you have difficulties finding sleep...

[Scott Morrison]

I think you can reproduce all these sign rules if you:

1. write [1]A instead of A[1] for grading shifts
2. insert a sign every time a "graded symbol" (a differential, an element, or a shift functor) moves past another graded symbol (in the purely syntactic sense of formulas written on the page).

[Kevin Buzzard]

It's a bit terrifying that "random" sign choices are being deemed "canonical"

[Julian Külshammer]

I know 2 as the Koszul sign rule, not sure who gave it its name, but in the literature I'm reading it is the standard choice for the "random" sign conventions.

[Scott Morrison]

I really don't think they are random. If you draw the relevant string diagram in the monoidal category SVect (or super-whatever), and remember that the braiding there is not the braiding in Z/2Z graded Vect, then the number of minus signs is always the number of times you use the nontrivial part of the braiding. In normal langauge, this just compiles down the the usual Koszul sign rule --- read the literal order of symbols appearing on either side of an equation, calculate the permutation that has been applied, and put in a minus sign every time you transposed two odd symbols.

[Scott Morrison]

As I said above, this only reproduces the rules in Stacks if you write grading shifts "on the left", i.e. as [1]A instead of A[1].

[Scott Morrison]

(One could even imagine a type-checker for the Koszul sign rule, given that it is purely syntactic...)

[Reid Barton]

While you're at it, you could also use a less confusing notation for the shift like ΣA... oops maybe not a great idea in Lean

[Scott Morrison]

There are lots of unicode variants: 𝛴A, ⅀A, ⨊A, ...

[Scott Morrison]

The italic sigma is actually pretty nice.

[Johan Commelin]

Hmm, I like the idea of refactoring has_shift to use a sigma-like notation

[Peter Scholze]

Wait, do you actually think that $\Sigma A$ is a good notation for the shift? (Well, maybe my dislike for the topologists' $\Sigma$ notation stems more from disliking $\Sigma^\infty_+$ as a way to denote what is essentially a free abelian group. But it also has an unfortunate clash with "sum".)

[Kevin Buzzard]

The notation for quadratic residues has an unfortunate clash with fractions in brackets, but we don't seem to get confused.

[Reid Barton]

Peter Scholze said:

Wait, do you actually think that $\Sigma A$ is a good notation for the shift?

No, I think it's a good notation for the suspension :upside_down:
I can never remember which direction is "the shift", or which direction is $A[1]$. But $\Sigma A$ has to be the thing in the cofiber sequence $A \to B \to C \to \Sigma A$, and so $\pi_{n+1}(\Sigma A) = \pi_n(A)$.
From my perspective the Stacks project is doing something strange, writing $A \to B \to C \to A[-1]$ for a cofiber sequence of chain complexes, but $A \to B \to C \to A[1]$ for a cofiber sequence of cochain complexes. I would rather think of both chain complexes and cochain complexes as sitting inside unbounded complexes, with the cochain complexes in negative degree. So, those conventions don't really work for me. Luckily, it doesn't affect the sign conventions because $i$ and $-i$ have the same parity.

[Matthew Ballard]

Another standard one is $S^nA$

[Johan Commelin]

https://unicode-table.com/en/search/?q=shift lists some unicode symbols related to "shift". All of them will be considered unorthodox :rofl:

[Johan Commelin]

Does anyone know how to get the LES for the distinguished triangle $τ_{≥ i+1} C → τ_{≥ i} C → H_i(C)[-i]$ in a hands-on manner? Currently, the only way I see is to show that the homotopy category of complexes is a pre-triangulated category and setup the general machinery. Are there viable shortcuts?

[Matthew Ballard]

:point_left:${}^nA$ has my vote

[Matthew Ballard]

Johan Commelin said:

Does anyone know how to get the LES for the distinguished triangle $τ_{≥ i+1} C → τ_{≥ i} C → H_i(C)[-i]$ in a hands-on manner? Currently, the only way I see is to show that the homotopy category of complexes is a pre-triangulated category and setup the general machinery. Are there viable shortcuts?

Does this arise from a SES of complexes? I always get my truncations confused

[Johan Commelin]

I guess you can see it as $τ_{≥ i+1} (τ_{≥ i} C) → τ_{≥ i} C → τ_{≤ i} (τ_{≥ i} C)$

[Johan Commelin]

Not sure if that helps.

[Matthew Ballard]

$$\begin{CD} @. \ker d^i @>=>> \ker d^i @. \\ @. @V=VV @VVV @. \\ 0 @>>> \ker d^i @>>> C^i @>d^i>> C^{i+1} \\ @. @VVV @Vd^iVV @V=VV \\ @. 0 @>>> \ker d^{i+1} @>>> C^{i+1} \\ @. @. @VVV @. \\ @. @. H^{i+1}(C) @. \end{CD}$$

This?

[Johan Commelin]

Your CD skills are impressive! I didn't know Zulip could do this!

[Matthew Ballard]

It is only the commutative diagram package handled by KaTeX. :cry:

[Johan Commelin]

You will have to help me a bit with understanding how this helps us with getting the LES for Ext(_, V) applied to that triangle.

[Matthew Ballard]

If I pretend the top row is $0$, then I have a short exact sequence of complexes

[Johan Commelin]

But it isn't termwise split, so we would still need to work, right?

[Matthew Ballard]

Good point. I was thinking of just homology in my head

[Matthew Ballard]

Do you have injectives?

[Patrick Massot]

This CD code brings back very old memories...

[Johan Commelin]

@Matthew Ballard Mathlib only knows about projectives and projective resolutions atm

[Johan Commelin]

It doesn't yet know how to apply a derived functor to a complex, but we will certainly need to teach it that.

[Matthew Ballard]

I guess assume that each $C^i$ is projective then.

[Johan Commelin]

I don't think we can do that. So we'll have to replace the complexes with quasi-isomorphic complexes consisting of projectives.

[Matthew Ballard]

There are a lot of equalities in the diagram. The only issue is whether the middle column can be kept exact.

[Johan Commelin]

But how does a SES of complexes help, if it's not termwise split?

[Johan Commelin]

After applying Hom(_, V) you end up with a SneS of complexes, and then what do you do?

[Matthew Ballard]

SES of complexes => LES of homology requires some assumptions on the complex?

[Johan Commelin]

I dunno. Whatever we do, it will need to be explained to Lean.

[Matthew Ballard]

$$\begin{CD} 0 @. 0 \\ @VVV @VVV \\ C^{i-1} @>>> C^i \\ @VVV @VwVV \\ D^{i-1} @>v>> D^i \\ @VuVV @VyVV \\ E^{i-1} @>x>> E^i \\ @VVV @VVV \\ 0 @. 0 \end{CD}$$

Given $e \in E^{i-1}$ with $x(e) = 0$, pick some $d \in D^{i-1}$ with $u(d) = e$. Then $yv(d) = 0$ so there is a $c \in C^i$ with $w(c) = v(d)$. This should induce the map

$$H^{i-1}(E) \to H^i(C)$$

[Johan Commelin]

Aah, sure. So a SES of complexes gives you a LES of homology. We almost have this in Lean.

[Matthew Ballard]

I thought so.

[Johan Commelin]

But if you have that triangle of truncations, you first need to apply Hom(_, V). And that will destroy all SESiness, unless you have split SES's.

[Matthew Ballard]

I store this in the same part of my brain with :five:

[Matthew Ballard]

Since everyone other column is an identity map, you only need to worry about exactness of

$$0 \leftarrow \operatorname{Hom}(\ker d^i, V) \leftarrow \operatorname{Hom}(C^i,V) \leftarrow \operatorname{Hom}(\ker d^{i+1},V) \leftarrow \operatorname{Hom}(H^{i+1}(C),V) \leftarrow 0$$

But in general, this is probably not exact without some conditions on $V$.

[Matthew Ballard]

Perhaps you can say that

[Johan Commelin]

Yup, exactly

[Johan Commelin]

But to do that, we might need to develop quite some machinery

[Johan Commelin]

Note that it's not clear to me that C consists of projective objects in our application. So even that $$\text{Cone}(_ → _)$$ will require some extra help, when we want to take Ext(_, V)

[Matthew Ballard]

It would be very nice if some version of Lemma 1.2 is true in this setting.

[Peter Scholze]

Reid Barton said:

From my perspective the Stacks project is doing something strange, writing $A \to B \to C \to A[-1]$ for a cofiber sequence of chain complexes, but $A \to B \to C \to A[1]$ for a cofiber sequence of cochain complexes.

Wait, this is what the Stacks Project does? That's awkward indeed. I always thought that shifts are normalized so that there are triangles

$A\to B\to C\to A[1]$

no matter what your other conventions are. This means that $M[n]$ puts an object $M$ into homological degree $n$ (=cohomological degree $-n$), so this gives a slight bias to homological conventions, which I'm fine with. [Drinfeld recently wrote a paper about DG algebras in cohomological degrees $0$ and $-1$...]

(Aaah, the Stacks project is even weirder: It adapts its shift according to whether things are homological or cohomological, but it uses the unintuitive normalization in both cases! runs away screaming :running: :scream: )

[Johan Commelin]

Right, the axioms of a triangulated category basically force these conventions on you (which might not even be the best reason out there).

[Riccardo Brasca]

I am working on the LES for derived functor. Specifically on the following lemma.

lemma six_term_exact_seq [F.additive] (n : ℕ) (A : short_exact_sequence C) :
  exact_seq D [
    (F.left_derived (n+1)).map A.f, (F.left_derived (n+1)).map A.g,
    δ F n A,
    (F.left_derived n).map A.f, (F.left_derived n).map A.g]

[Adam Topaz]

There is one more thing that has been lingering in the background.... It's hard to compute Ext.

Here is the current definition of Ext:

/--
`Ext R C n` is defined by deriving in the frst argument of `(X, Y) ↦ Module.of R (unop X ⟶ Y)`
(which is the second argument of `linear_yoneda`).
-/
@[simps]
def Ext (n : ℕ) : Cᵒᵖ ⥤ C ⥤ Module R :=
functor.flip
{ obj := λ Y, (((linear_yoneda R C).obj Y).right_op.left_derived n).left_op,
  map := λ Y Y' f, (nat_trans.left_derived ((linear_yoneda R C).map f).right_op n).left_op,
  map_id' := ...,
  map_comp' := ... }.

So, essentially, you take an opposite, compute a left derived functor, and take another opposite.

As far as I know, we still don't really have a good way of identifying Ext with the homology of Hom(P,B) where P is a projective resolution, because of this really annoying issue of going between homology f.op g.op and op (homology g f)..

[Johan Commelin]

In for_mathlib/derived_functor there is now a completely sorry-free proof of LES for left derived functors, except for the degree 0 part.

[Johan Commelin]

lemma six_term_exact_seq [F.additive] (n : ℕ) (A : short_exact_sequence C) :
  exact_seq D [
    (F.left_derived (n+1)).map A.f, (F.left_derived (n+1)).map A.g,
    δ F n A,
    (F.left_derived n).map A.f, (F.left_derived n).map A.g] :=
begin
  refine exact_seq.cons _ _ (exact_of_short_exact _ _ _) _ _,
  refine exact_seq.cons _ _ (exact_of_short_exact.δ_right _ _ _) _ _,
  refine exact_seq.cons _ _ (exact_of_short_exact.δ_left _ _ _) _ _,
  refine exact_seq.cons _ _ (exact_of_short_exact _ _ _) _ _,
  apply exact_seq.single,
end

[Johan Commelin]

For the degree 0 part, we will actually need to tell Lean what a right exact functor is :rofl:

[Adam Topaz]

docs#category_theory.limits.preserves_finite_colimits ?

[Riccardo Brasca]

What we need is that it sends a short exact sequence to a short(er) exact sequence, but this should follows from that definition without too much trouble I hope.

[Adam Topaz]

Well, what I mean is that preserving finite colimits is a more general way to phrase right exactness.

[Johan Commelin]

Yeah, we should just use that.

[Johan Commelin]

Do we already know that between abelian cats, such a functor preserves epis?

[Adam Topaz]

Johan Commelin said:

Do we already know that between abelian cats, such a functor preserves epis?

I'm not sure...

[Johan Commelin]

The tail of the LES should now be really easy.

[Andrew Yang]

I think we know that pushout-preserving functors preserve epis. But there might be universe issues?

[Adam Topaz]

@Andrew Yang do you remember what the lemma is called?

[Johan Commelin]

But there might be universe issues?

I hope not!

[Adam Topaz]

I mean, we can always use docs#category_theory.limits.epi_of_is_colimit_parallel_pair

[Andrew Yang]

Oh we don't. But this should be an easy dualization of docs#category_theory.preserves_mono.
Looking at the code I think I might have solved the universe issue some weeks ago.

[Adam Topaz]

Express your epi as a coequalizer, and use the fact that coequalizers are preserved, etc..

[Andrew Yang]

Done in #12084.

[Riccardo Brasca]

Maybe someone wants to help to prove that if $A \to B \to C \to 0$ is exact then also $F(A) \to F(B) \to F(C) \to 0$ is exact? The fact that $F$ preserves epi takes care of the last exactness, but I am a little bit lost in the API to prove exactness at $F(B)$.

[Adam Topaz]

Since $B \to C$ is a cokernel of $A \to B$ and $F$ preserves finite colimits (in particular, cokernels), you should get that $F(B) \to F(C)$ is the cokernel of $F(A) \to F(B)$.

[Adam Topaz]

Which file are you working on? I can write down this proof.

[Riccardo Brasca]

Yes, this is the math proof I have. It's probably my fault, but I am getting a little bit crazy about stating this in mathlib.

[Riccardo Brasca]

Yes please, it's probably more helpful for me to read your proof later.

[Adam Topaz]

Is this in for_mathlib/exact_seq.lean?

[Riccardo Brasca]

Yes, I am pushing what I've written, but it is essentially a random mess.

[Adam Topaz]

Okay. I'll get some coffee first :coffee:

[Riccardo Brasca]

It's at the end of the file

[Riccardo Brasca]

Thanks!

[Riccardo Brasca]

The lemma we want is preserves_exact_seq, I am not sure the one before is true/needed.

[Adam Topaz]

Okay, there is one sorry left for this:

def cokernel_comparison : cokernel f ⟶ A₃ :=
  cokernel.desc f g $ comp_eq_zero ex

instance : is_iso (cokernel_comparison ex) := sorry

I.e. if $A \to B \to C \to 0$ is exact, then the canonical map from the cokernel of $A \to B$ to $C$ is an isomorphism.
This can be proved (in a somewhat clunky way) using pseudoelements.

My class has a midterm in an hour or so, so I can't finish this off right now, but it should be doable.

[Riccardo Brasca]

I am having a look, thanks a lot!

[Adam Topaz]

It would be nice to build some more api around exact_seq [f, g, 0], which should essentially encapsulate the fact that A_3 is the cokernel of f (e..g. have a exact_seq.desc, etc.)

[Riccardo Brasca]

The proof is probably not the best one, but it is done.

[Johan Commelin]

Awesome! Does that mean that the degree 0 part is completely done? Or do you still need some glue?

[Riccardo Brasca]

Ah no, you are overestimating me! Now F sends the final part of the projective resolution to an exact sequence. I think this easily implies that left_derived F 0 A ≅ A, so we have a square. We need to prove it commutes.

[Riccardo Brasca]

Andrew Yang said:

But there might be universe issues?

I am not sure you were talking about this, but to use docs#category_theory.limits.preserves_finite_colimits I had to write

variables {C : Type u} {D : Type v} [category.{w} C] [category.{w} D]

Note the w that is there twice.

[Andrew Yang]

Oh I did not know that this is not yet generalized. Does this cause any problem?

[Riccardo Brasca]

I don't know what it will happen at the end. At the moment I am using w twice, but sooner or later we will want to apply the general machinery to a concrete situation.

[Riccardo Brasca]

Does anyone see a quick way of closing the goal here?

import category_theory.abelian.exact
import category_theory.preadditive.additive_functor
import category_theory.preadditive.projective

universes w u v

noncomputable theory

open category_theory category_theory.functor category_theory.limits

variables {C : Type u} {D : Type v} [category.{w} C] [category.{w} D] [abelian C] [abelian D]
variables (F : C ⥤ D) [additive F] {X : C}
variables [limits.preserves_finite_colimits F] [enough_projectives C]

def cokernel_homology {X Y Z : C} (f : X ⟶ Y) :
  cokernel f ⟶ homology f (0 : Y ⟶ Z) (by simp) :=
cokernel.desc _ (limits.factor_thru_kernel_subobject _ (𝟙 _) (by simp) ≫ (homology.π _ _ _))
begin
  sorry
end

(Or another way of constructing the morphism). I need an iso, but I already have the morphism in the other direction.

[Adam Topaz]

Ugh... this should be easy if we defined homology without subobjects.

[Riccardo Brasca]

Yes, I HATE this image_to_kernel stuff...

[Adam Topaz]

You can use docs#homology_iso_cokernel_lift

[Adam Topaz]

https://github.com/leanprover-community/lean-salamander/blob/master/src/homology.lean

[Adam Topaz]

I think homology should be defined as cokernel (kernel.lift g f w)..

[Filippo A. E. Nuccio]

Adam Topaz said:

https://github.com/leanprover-community/lean-salamander/blob/master/src/homology.lean

I can't click this link...

[Riccardo Brasca]

It works for me, it must be some permission.

[Adam Topaz]

Ooops... here is the content:

import category_theory.abelian.pseudoelements
import category_theory.abelian.opposite

namespace category_theory.abelian


noncomputable theory

open category_theory
open category_theory.limits

variables {C : Type*} [category C] [abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)

def homology_c (w : f ≫ g = 0) : C :=
cokernel (kernel.lift g f w)

def homology_k (w : f ≫ g = 0) : C :=
kernel (cokernel.desc f g w)

def homology_c_to_k (w : f ≫ g = 0) : homology_c f g w ⟶ homology_k f g w :=
cokernel.desc _ (kernel.lift _ (kernel.ι _ ≫ cokernel.π _) (by simp)) begin
  apply limits.equalizer.hom_ext,
  simp,
end

local attribute [instance] pseudoelement.hom_to_fun pseudoelement.has_zero

instance (w : f ≫ g = 0) : mono (homology_c_to_k f g w) :=
begin
  apply pseudoelement.mono_of_zero_of_map_zero,
  dsimp [homology_c, homology_c_to_k],
  intros a ha,
  obtain ⟨a,rfl⟩ := pseudoelement.pseudo_surjective_of_epi (cokernel.π (kernel.lift g f w)) a,
  apply_fun (kernel.ι (cokernel.desc f g w)) at ha,
  simp [← pseudoelement.comp_apply] at ha,
  simp [pseudoelement.comp_apply] at ha,
  haveI : exact f (cokernel.π f) := exact_cokernel f,
  obtain ⟨b,hb⟩ : ∃ b, f b = _ := pseudoelement.pseudo_exact_of_exact.2 _ ha,
  suffices : ∃ c, kernel.lift g f w c = a,
  { obtain ⟨c,rfl⟩ := this,
    simp [← pseudoelement.comp_apply] },
  use b,
  apply_fun kernel.ι g,
  swap, { apply pseudoelement.pseudo_injective_of_mono },
  simpa [← pseudoelement.comp_apply]
end

instance (w : f ≫ g = 0) : epi (homology_c_to_k f g w) :=
begin
  apply pseudoelement.epi_of_pseudo_surjective,
  dsimp [homology_k, homology_c, homology_c_to_k],
  intros a,
  let b := kernel.ι (cokernel.desc f g w) a,
  haveI : exact f (cokernel.π f) := exact_cokernel f,
  obtain ⟨c,hc⟩ : ∃ c, cokernel.π f c = b, apply pseudoelement.pseudo_surjective_of_epi (cokernel.π f),
  have : g c = 0,
  { dsimp [b] at hc,
    rw [(show g = cokernel.π f ≫ cokernel.desc f g w, by simp), pseudoelement.comp_apply, hc],
    simp [← pseudoelement.comp_apply] },
  obtain ⟨d,hd⟩ : ∃ d, kernel.ι g d = c,
  { apply pseudoelement.pseudo_exact_of_exact.2 _ this,
    apply exact_kernel_ι },
  use cokernel.π (kernel.lift g f w) d,
  apply_fun kernel.ι (cokernel.desc f g w),
  swap, { apply pseudoelement.pseudo_injective_of_mono },
  simp [← pseudoelement.comp_apply],
  simp [pseudoelement.comp_apply, hd, hc],
end

instance (w : f ≫ g = 0) : is_iso (homology_c_to_k f g w) := is_iso_of_mono_of_epi _

section homology

def homology (w : f ≫ g = 0) : C := homology_c f g w

def homology.π (w : f ≫ g = 0) : kernel g ⟶ homology f g w := cokernel.π _

def homology.desc {A} (w : f ≫ g = 0) (e : kernel g ⟶ A)
  (he : kernel.lift g f w ≫ e = 0) : homology f g w ⟶ A := cokernel.desc _ e he

@[simp, reassoc]
lemma homology.desc_π {A} (w : f ≫ g = 0) (e : kernel g ⟶ A)
  (he : kernel.lift g f w ≫ e = 0) : homology.π f g w ≫ homology.desc f g w e he = e :=
cokernel.π_desc _ _ _

@[simp, reassoc]
lemma homology.condition_π (w : f ≫ g = 0) : kernel.lift g f w ≫ homology.π f g w = 0 :=
cokernel.condition _

def homology.ι (w : f ≫ g = 0) : homology f g w ⟶ cokernel f :=
homology_c_to_k f g w ≫ kernel.ι (cokernel.desc f g w)

def homology.lift {A} (w : f ≫ g = 0) (e : A ⟶ cokernel f)
  (he : e ≫ cokernel.desc f g w = 0) : A ⟶ homology f g w :=
kernel.lift _ e he ≫ inv (homology_c_to_k f g w)

@[simp, reassoc]
lemma homology.ι_lift {A} (w : f ≫ g = 0) (e : A ⟶ cokernel f)
  (he : e ≫ cokernel.desc f g w = 0) : homology.lift f g w e he ≫ homology.ι f g w = e :=
by simp [homology.lift, homology.ι]

@[simp, reassoc]
lemma homology.ι_condition (w : f ≫ g = 0) : homology.ι f g w ≫ cokernel.desc f g w = 0 :=
by simp [homology.ι]

lemma homology.hom_from_ext {A} {w} (a b : homology f g w ⟶ A) :
  homology.π f g w ≫ a = homology.π f g w ≫ b → a = b :=
coequalizer.hom_ext

lemma homology.hom_to_ext {A} {w} (a b : A ⟶ homology f g w) :
  a ≫ homology.ι f g w = b ≫ homology.ι f g w → a = b :=
begin
  intro h,
  dsimp [homology.ι] at h,
  simp_rw ← category.assoc at h,
  replace h := equalizer.hom_ext h,
  apply_fun (λ e, e ≫ (inv (homology_c_to_k f g w))) at h,
  simpa using h,
end

end homology

lemma w_op (w : f ≫ g = 0) : g.op ≫ f.op = 0 := by { rw ← op_comp, simp [w] }

def kernel_op : (kernel f.op).unop ≅ cokernel f :=
{ hom := (kernel.lift _ (cokernel.π f).op $ by simp [← op_comp]).unop ≫ eq_to_hom (opposite.unop_op _),
  inv := cokernel.desc _ (eq_to_hom (opposite.unop_op _).symm ≫ (kernel.ι f.op).unop) begin
    simp only [category.id_comp, eq_to_hom_refl],
    rw [← f.unop_op, ← unop_comp, f.op.op_unop, kernel.condition],
    refl,
  end,
  hom_inv_id' := begin
    simp only [category.id_comp, eq_to_hom_refl, category.comp_id, ← unop_id, ← unop_comp],
    rw [← (cokernel.desc f (kernel.ι f.op).unop _).unop_op, ← unop_comp],
    congr' 1,
    apply limits.equalizer.hom_ext,
    dsimp,
    simp [← op_comp],
  end,
  inv_hom_id' := begin
    apply limits.coequalizer.hom_ext,
    dsimp,
    simp [← unop_comp],
  end }

def cokernel_op : (cokernel f.op).unop ≅ kernel f :=
{ hom := kernel.lift _ ((cokernel.π f.op).unop ≫ eq_to_hom (opposite.unop_op _)) begin
    simp only [eq_to_hom_refl, category.comp_id],
    rw [← f.unop_op, ← unop_comp, f.op.op_unop, cokernel.condition],
    refl,
  end,
  inv := eq_to_hom (opposite.unop_op _).symm ≫ (cokernel.desc _ (kernel.ι f).op (by simp [← op_comp])).unop,
  hom_inv_id' := begin
    simp only [category.id_comp, eq_to_hom_refl, category.comp_id, ← unop_id, ← unop_comp],
    rw [← (kernel.lift f (cokernel.π f.op).unop _).unop_op, ← unop_comp],
    congr' 1,
    apply limits.coequalizer.hom_ext,
    dsimp,
    simp [← op_comp],
  end,
  inv_hom_id' := begin
    apply limits.equalizer.hom_ext,
    dsimp,
    simp [← unop_comp]
  end }

end category_theory.abelian

[Riccardo Brasca]

In any case thanks a lot! I have to stop now, but I will have a close look later.

[Riccardo Brasca]

You redefined homology but you didn't prove it's the same as in mathlib, right? In any case I hope using docs#homology_iso_cokernel_lift will help.

[Adam Topaz]

Right, I'm not suggesting to use that other file. In this case you can get by with docs#homology_iso_cokernel_lift together with cokernel.desc and/or cokernel.map.

[Riccardo Brasca]

def functor.left_derived.zero_iso [enough_projectives C] : (F.left_derived 0).obj X ≅ F.obj X

is sorry free, but it is quite slow and it is defined in tactic mode, that it's bad. I am done for today, if someone wants to have a look it is derived_functor.lean, at the end.

[Riccardo Brasca]

Of course what we really want is an iso of functors, but this is a start.

[Riccardo Brasca]

It's even possible that defining the natural transformation and showing that its component are iso will be less cumbersome.

[Johan Commelin]

Thanks a lot for hacking on this!