# Zulip Chat Archive

## Stream: homology

### Topic: Ideas for refactor

#### Adam Topaz (Aug 31 2022 at 13:31):

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 (Aug 31 2022 at 13:36):

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

#### Johan Commelin (Aug 31 2022 at 13:41):

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 (Aug 31 2022 at 13:44):

presumably those would boil down to whiskering!

#### Johan Commelin (Aug 31 2022 at 13:44):

for "restricting" I can believe that.

#### Johan Commelin (Aug 31 2022 at 13:44):

But extending is less trivial, I think

#### Adam Topaz (Aug 31 2022 at 13:45):

maybe extending is an adjoint of restricting?

#### Johan Commelin (Aug 31 2022 at 13:51):

not exactly

#### Johan Commelin (Aug 31 2022 at 13:52):

at least not with naive resticting/extending

#### Adam Topaz (Aug 31 2022 at 13:54):

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 (Aug 31 2022 at 13:54):

You need the square in indices `-1`

and `0`

to commute.

#### Johan Commelin (Aug 31 2022 at 13:55):

But the path via `X' _{-1}`

is always `0`

.

#### Johan Commelin (Aug 31 2022 at 13:55):

whereas the other one has no reason to be `0`

.

#### Johan Commelin (Aug 31 2022 at 13:56):

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 (Aug 31 2022 at 13:57):

I'm confused. `X'_{-1}`

is zero, so any map originating from it would be zero.

#### Johan Commelin (Aug 31 2022 at 13:58):

Ooh, maybe I want chain complexes

#### Johan Commelin (Aug 31 2022 at 13:58):

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

#### Johan Commelin (Aug 31 2022 at 13:59):

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

#### Adam Topaz (Aug 31 2022 at 14:00):

I'm extending X not Y

#### Adam Topaz (Aug 31 2022 at 14:01):

So

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

#### Adam Topaz (Aug 31 2022 at 14:01):

clearly I'm an expert at ASCII art

#### Johan Commelin (Aug 31 2022 at 14:01):

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

#### Johan Commelin (Aug 31 2022 at 14:02):

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 (Aug 31 2022 at 14:02):

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

#### Johan Commelin (Aug 31 2022 at 14:03):

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 (Aug 31 2022 at 14:05):

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

#### Adam Topaz (Aug 31 2022 at 14:06):

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 (Aug 31 2022 at 14:07):

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

#### Johan Commelin (Aug 31 2022 at 14:10):

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

#### Matthew Ballard (Aug 31 2022 at 14:34):

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

#### Johan Commelin (Aug 31 2022 at 14:35):

Right. That seems like a downside.

#### Matthew Ballard (Aug 31 2022 at 14:37):

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 (Aug 31 2022 at 14:39):

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

#### Matthew Ballard (Aug 31 2022 at 14:40):

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

#### Matthew Ballard (Aug 31 2022 at 14:40):

You call the result your derived category

#### Matthew Ballard (Aug 31 2022 at 14:41):

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

#### Matthew Ballard (Aug 31 2022 at 14:41):

But in general it is not the same

#### Matthew Ballard (Aug 31 2022 at 14:42):

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

#### Matthew Ballard (Aug 31 2022 at 14:43):

At least of an object itself

#### Julian Külshammer (Aug 31 2022 at 16:21):

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 (Sep 01 2022 at 20:57):

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 (Sep 02 2022 at 04:06):

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

#### Johan Commelin (Sep 02 2022 at 04:07):

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

Last updated: Dec 20 2023 at 11:08 UTC