homological todos

Stream: condensed mathematics

[Johan Commelin]

Here are the remaining bits of homological API that need to be done, afaict.

• Given a short exact sequence of objects, we get a triangle in the bounded homotopy category
• Given an object $C$ (ie complex) in the bounded homotopy category, we get a triangle $τ_{i+1}C → τ_i C → H_i(C)[i]$
• Given a triangle, we get a LES of homology groups, in terms of exact_seq.
• If f : C ⟶ C' is componentwise an epi, then the componentwise kernel complex K fits in a triangle K ⟶ C ⟶ C'.

[Johan Commelin]

The third is basically done, just needs some Lean packaging. I guess 2 and 4 are the most work.

[Johan Commelin]

Ooh, here's another one that's nontrivial:

• If $C$ is a bounded complex consisting of $\text{Ext}(\_, B)$-acyclic objects, then $\text{Ext}(C,B)$ can just be computed by applying $\text{Hom}(\_,B)$ and taking homology. In other words, we don't need to take a projective replacement.

[Kevin Buzzard]

What is an Ext(_,B)-acyclic object?

[Johan Commelin]

An object such that all higher ext groups vanish

[Johan Commelin]

https://en.wikipedia.org/wiki/Acyclic_object

[Kevin Buzzard]

Oh so it's what I'd call a Hom(_,B)-acyclic object?

[Johan Commelin]

Yeah, sorry. That's what I should have written. Let me fix it.

[Johan Commelin]

Snap! •₁ is false: https://math.stackexchange.com/a/2710380. It doesn't work in the homotopy category :sad:

[Johan Commelin]

Same problem for the distinguished triangles involving the truncation functors

[Johan Commelin]

So we might need to explicitly track some quasi-isos.

[Adam Topaz]

Johan Commelin said:

So we might need to explicitly track some quasi-isos.

If you replace everything by a K-projective, then you don't need to track quasi isos

[Johan Commelin]

But then you can't compute, right?

[Johan Commelin]

Atm, I don't see an easy way to get the LES for a short exact sequence.

[Adam Topaz]

Oh I see.

[Adam Topaz]

If you have a SES $0 \to A \to B \to C \to 0$ then you get a map from the cone $C(A \to B)$ to $C$ which is a quasi-iso.

[Johan Commelin]

Right... and we will have to fool around with it

[Adam Topaz]

And by the general nonsense (i.e. taking K-projective replacements) it should be possible to show that the induced map of functor $Ext(C,-) \to Ext(C(A \to B),-)$ is an iso

[Johan Commelin]

So we can get a LES... but we need it to be functorial in SES's. It's just a bunch of work. If we had triangles it would be "trivial".

[Adam Topaz]

Yeah of course.

[Adam Topaz]

But we can define the bounded above derived cat very quickly now. Maybe we should go ahead and do that so we can get actual triangles?

[Johan Commelin]

Hmm, you think so?

[Adam Topaz]

I don't know.

[Johan Commelin]

I guess we can define it quickly. But we also need the API

[Johan Commelin]

It might still be the path of least resistance/effort

[Johan Commelin]

What would the definition be?

[Adam Topaz]

the full subcat of the homotopy cat generated by K-projectives.

[Johan Commelin]

And what does "generated" mean?

[Adam Topaz]

Oh, just the set of K-projectives

[Adam Topaz]

I'll write it down.

[Adam Topaz]

Okay, I started a new file for_mathlib/derived/derived_cat with

noncomputable def localization_functor :
  bounded_homotopy_category A ⥤ bounded_derived_category A :=

and not much more (yet...)

[Adam Topaz]

Also this:

lemma is_iso_localization_functor_map_of_is_quasi_iso
  (X Y : bounded_homotopy_category A) (f : X ⟶ Y)
  [is_quasi_iso f] : is_iso ((localization_functor _).map f) :=

[Adam Topaz]

I've added a stub for

instance pretriangulated : triangulated.pretriangulated (bounded_derived_category A) :=
{ distinguished_triangles := { T |
    ∃ (S : triangle (bounded_homotopy_category A))
      (hS : S ∈ dist_triang (bounded_homotopy_category A))
      (f : T ⟶ replace_triangle S), is_iso f }, ...

in for_mathlib/derived/derived_cat with many MANY small sorrys that should be relatively simple. I have a bunch of meetings today, so I won't be able to work on this much more today. Any help filling in these sorry's would be much appreciated!

[Matthew Ballard]

Has exists_K_projective_replacement been promoted to 𝒦 ⥤ 𝒦 somewhere?

[Johan Commelin]

Not that I know

[Matthew Ballard]

That is the localization functor exhibiting the full subcategory of K-projectives as a model for the derived category. One needs to tell Lean it takes SES to triangles. Then functoriality is intermediated by application of the replacement functor.

[Matthew Ballard]

You won't quite prove you have a model of the derived category but you could tack that on for fun at some point.

[Adam Topaz]

The functor you want @Matthew Ballard is the composition of localization with forgetting.

[Matthew Ballard]

Sure, I was being a little careless about the codomain of the functor.

[Matthew Ballard]

(Also I forgot the notation for the K-Proj as a category)

[Adam Topaz]

But this "forgetting" functor doesn't really exist in real life, right?

[Matthew Ballard]

Abstractly, no.

[Matthew Ballard]

In practice, it underpins any localization where there is (at least) an underlying model structure.

[Andrew Yang]

Is the C in $\cdot_2$ a chain complex or a cochain complex?
Most of the stuff LTE has now are for cochain complexes though. Will we need to duplicate them?

[Johan Commelin]

In the end, it should be a functor on bounded_homotopy_category... so whichever version is used for that.

[Johan Commelin]

I always forget which direction (co)chain complexes are...

[Johan Commelin]

I have fixed about half of the sorries in the file that Adam pushed. There are still 15 sorries left.