Ideas for refactor

Stream: homology

[Adam Topaz]

Just a quick message to kick off the discussion concerning the impending refactor of chain complexes and homology.

What do people think about the following manuscript?
https://arxiv.org/pdf/2208.13282.pdf

[Adam Topaz]

And the paper that this depends on: https://arxiv.org/abs/2101.06176

[Johan Commelin]

Interesting. I couldn't find any discussion about "change of Q". Would this framework make it easy to "extend a complex by 0" or to restrict to a subcomplex (eg from int-indexed to nat-indexed)?

[Adam Topaz]

presumably those would boil down to whiskering!

[Johan Commelin]

for "restricting" I can believe that.

[Johan Commelin]

But extending is less trivial, I think

[Adam Topaz]

maybe extending is an adjoint of restricting?

[Johan Commelin]

not exactly

[Johan Commelin]

at least not with naive resticting/extending

[Adam Topaz]

Let $X$ be a nat-indexed cochain complex and $X'$ its extension to a Z-cochain complex, and let $Y'$ be any Z-cochain complex and $Y$ its restriction to N. Is it not the case that $Hom(X,Y) = Hom(X',Y')$?

[Johan Commelin]

You need the square in indices -1 and 0 to commute.

[Johan Commelin]

But the path via X' _{-1} is always 0.

[Johan Commelin]

whereas the other one has no reason to be 0.

[Johan Commelin]

Other point: Those two papers are going full model category. They only ever talk about the homotopy category, but I didn't find a hands-on notion of homotopy between two complexes. I'm not sure what to make of that.

[Adam Topaz]

I'm confused. X'_{-1} is zero, so any map originating from it would be zero.

[Johan Commelin]

Ooh, maybe I want chain complexes

[Johan Commelin]

Or whatever. A little variation on this situation will cause a problem.

[Johan Commelin]

X_{-1} ---> X_0
  |          |
  v          v
  0 ------> Y_0

[Adam Topaz]

I'm extending X not Y

[Adam Topaz]

So

  0  ---> X_0
   |           |
  v          v
Y_{-1} -----> Y_0

[Adam Topaz]

clearly I'm an expert at ASCII art

[Johan Commelin]

Sure, but if you flip the direction of the differentials then you are in trouble.

[Johan Commelin]

Which means that you need specific conditions on your Q -> Q' before you can extend/restrict from one to the other with an adjunction.

[Adam Topaz]

okay, yes, but if you flip for the extension, you also need to flip for the restriction

[Johan Commelin]

Take the inclusion of fin n into int. You will either get problems close to 0 or close to n, depending on the direction of the differentials.

[Adam Topaz]

right in this case there will be an issue at n for the cochain direction

[Adam Topaz]

well, this is not much of an issue since we can define some extension functor in a similar way to what we do now, by saying that "everything which is not in the image should be set to zero"

[Adam Topaz]

this is still something that can be checked on the quiver level

[Johan Commelin]

So what about homotopies? Do they admit a clean definition?

[Matthew Ballard]

They need a theorem to describe the weak equivalences :grumpy:

[Johan Commelin]

Right. That seems like a downside.

[Matthew Ballard]

The first idea that occurred to me when forming a derived category of $F := \operatorname{Fun}(Q,A)$ for some abelian category was something a'la Positselski

[Matthew Ballard]

You start with the pointwise abelian category structure on $F$

[Matthew Ballard]

Then you quotient by the subcategory of objects coming from totalizations of exact sequences.

[Matthew Ballard]

You call the result your derived category

[Matthew Ballard]

It relates to the usual derived category because totalizations of exact sequences of complexes are acyclic, hence $0$ when inverting quasi-isomorphisms

[Matthew Ballard]

But in general it is not the same

[Matthew Ballard]

But generally in either of these approaches is there really a notion of 'homology'?

[Matthew Ballard]

At least of an object itself

[Julian Külshammer]

In both papers, the authors assume for most of the results that Q has a Serre functor (some abstract version of Q being selfinjective). This should not be satisfied for the N-indexed version of complexes. It lets the authors however deal with things like "circular" complexes, or even N-complexes, in the sense that d^N=0 in a uniform fashion.

[Joël Riou]

Johan Commelin said:

Other point: Those two papers are going full model category. They only ever talk about the homotopy category, but I didn't find a hands-on notion of homotopy between two complexes. I'm not sure what to make of that.

I did not go into the details of these two papers, but there are ways to do computations in derived categories by using model category structures as it seems they do. For example, the category of bounded above complexes in an abelian category with enough projectives has a model category structure whose weak equivalences are the quasi-isomorphisms, cofibrant objects are complexes that are degreewise projective and all objects are fibrant. Then, for this model category, the fundamental lemma of homotopical algebra (which I have implemented in Lean and [some previous version of...] mathlib) precisely says that in the derived category, morphisms from a degreewise projective complex can be computed as "homotopy classes" of actual morphisms of complexes. There, "homotopy classes" of morphisms is to be understood in the context of Quillen's homotopical algebra, using cylinders or path objects. In the case of complexes, there are natural constructions of cylinders which makes it so that the homotopy relation using such a cylinder is almost by definition equiv to the usual notion of homotopy of morphisms of complexes.

Then, using my work on homotopical algebra, we could do computations in the derived category ($D^-$) in Lean/Mathlib if we could also show the axioms of model categories in the case I have mentionned above. I have done a significant part of the work for this, and some of the missing lemmas are presumably in some form or another in the LTE.

However, if this would give a good first example of model category, I do not think that it would be the right way to do homological algebra with in Lean/Mathlib. I would think a better approach is to develop the notion of triangulated category, e.g. showing it is possible to localize a triangulated with respect to a triangulated subcategory, e.g. when we formally invert quasimorphisms in the homotopy category of an abelian category, the morphisms in the localized category can be described by a certain calculus of fractions. Then, the derived category of an abelian category (defined by localization) would be additive, triangulated, etc, and we could redefine Ext group using these, show we can compute them using projective or injective resolutions, etc.

If "homology" could certainly be refactored, I do not think we need to consider significant changes to the definitions of complexes or homotopies.
Anyway, I would favour approaches which are based on standard "mainstream" mathematical works that have passed the test of time.

[Johan Commelin]

Yes, I agree that we should make an effort to stay "mainstream".

[Johan Commelin]

Also, thanks for explaining some of the abstract machinery. I'm not that familiar with it, so that's very helpful.