# Zulip Chat Archive

## Stream: homology

### Topic: Homology refactor

#### Joël Riou (Nov 28 2022 at 12:12):

I have been thinking about the homology refactor, basically how to import in mathlib3/4 some constructions done in the LTE. One of the constructions I introduced was that of "short complexes" in a category `C`

:

```
/-- A short complex in a category `C` with zero morphisms is the datum
of two composable morphisms `f : X₁ ⟶ X₂` and `g : X₂ ⟶ X₃` such that
`f ≫ g = 0`. -/
structure short_complex [has_zero_morphisms C] :=
{X₁ X₂ X₃ : C}
(f : X₁ ⟶ X₂)
(g : X₂ ⟶ X₃)
(zero : f ≫ g = 0)
```

All the API for homology should be adapted using `S : short_complex C`

as an input, and then, when we want to apply this to homological complexes, we only have to consider complexes of the form `K.X (prev i) ⟶ K.X i ⟶ K.X (next i)`

.

Another innovation in the LTE was the `has_homology`

structure. I introduced a more basic datum `homology_iso_datum`

. Following both Adam's ideas and mine, I ended up defining a `left_homology_datum`

for a short complex `S`

:

```
structure left_homology_data :=
(K H : C)
(i : K ⟶ S.X₂)
(π : K ⟶ H)
(hi₀ : i ≫ S.g = 0)
(hi : is_limit (kernel_fork.of_ι i hi₀))
(hπ₀ : hi.lift (kernel_fork.of_ι _ S.zero) ≫ π = 0)
(hπ : is_colimit (cokernel_cofork.of_π π hπ₀))
```

This basically consists of the datum of a kernel `K`

of `S.X₂ ⟶ S.X₃`

and a cokernel `H`

of the induced map `S.X₁ ⟶ K`

.

Dually, a `right_homology_datum`

can be defined as a similar datum using a cokernel `Q`

of `S.X₁ ⟶ S.X₂`

and a kernel `H`

of the induced map `Q ⟶ S.X₃`

.

Then, in a similar spirit as the `homology_gadget`

suggested by Adam at https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/homology.20refactor/near/290844887 (this is similar to the `has_homology`

that is in the LTE), I define an `homology_data`

for `S`

as :

```
structure homology_data :=
(left : S.left_homology_data)
(right : S.right_homology_data)
(iso : left.H ≅ right.H)
(comm : left.π ≫ iso.hom ≫ right.ι = left.i ≫ right.p)
```

Then, one may define `[has_homology S]`

when there exists such an `homology data`

, and define the homology of `S`

as the `left.H`

field of such a data. By construction, this notion of homology is self-dual. From that, one may define a good self-dual notion of (short) exact sequences, etc. Recently, I was able to get the snake lemma (in a slightly easier manner than in the LTE). I have developed these ideas in a (draft) branch

https://github.com/leanprover-community/mathlib/tree/homology_refactor

The relevant code is in `algebra/homology/short_complex/`

. Apart from the proof that short complexes in abelian categories have homology data, most of this code is quite straightforward and very boring, and when I tried to use this `short_complex`

API in order to redefine the homology of homological complexes, etc, the transition was quite easy, and many definitions became shorter. Besides the self-dual notions of homology and exactness we

get, this allows to define exact sequences without assuming `[has_images C] [has_kernels C]`

: for example, split short exact sequences in preadditive categories (with a zero object) are exact with my definition, but it does not make sense with the current definition in mathlib.

I would rather do this refactor before the actual port of `mathlib`

to `mathlib4`

is done, so that I guess the best would be to introduce this in `mathlib`

first. Then, I would like to do this refactor (which would start with the introduction of tidied versions of some of the files in `algebra/homology/short_complex/`

, as a sequence of small PRs, followed with a large PR when the notions of homology currently in mathlib are replaced by this API). Any comments?

#### Johan Commelin (Nov 28 2022 at 12:28):

It's great that you could simplify the snake lemma! I think that's a good test case.

#### Joël Riou (Jun 07 2023 at 09:04):

About two weeks ago, the mathlib4 PR process started for this homology refactor (also towards derived categories; spectral sequences will soon follow...). Thanks very much @Kevin Buzzard @Johan Commelin @Scott Morrison for the reviews! The list of the relevant PR appear at !4#4197. So far, I have PRed most of the "left" homology theory of short complexes `S`

(i.e. we have two composable maps `f : X₁ ⟶ X₂`

and `g : X₂ ⟶ X₃`

such that `f ≫ g = 0`

). I have defined `S.cycles`

to be a kernel of `S.g`

and `S.leftHomology`

to be a cokernel of `S.toCycles : S.X₁ ⟶ S.cycles`

. The file `LeftHomology.lean`

will soon be finished (one more PR after !4#4787 is merged).

Then, I will dualise this to get the "right" homology theory, which involves taking a cokernel of `S.f`

and defining the "right" homology as a kernel. I am not completely sure about the names. Currently, I am using `S.cyclesCo`

for a choice of a cokernel for `S.f : X₁ ⟶ X₂`

.

This notion is dual to that of `cycles`

(there is an isomorphism `S.op.cyclesCo ≅ op S.cycles`

). I chose not to use `cocycles`

because this would be more confusing (in math terminology, "cycles/cocycles" nuance is only about whether the differentials decrease or raise the degrees).

Does this name choice sound good enough?

(The following diagram may help visualise this homology-refactor.png: `K`

is `S.cycles`

, `Q`

is `S.cyclesCo`

and `H`

and `H'`

the left and right homology.)

#### Johan Commelin (Jun 07 2023 at 09:10):

minor point: in your final sentence left/right homology occurs twice

#### Joël Riou (Jun 07 2023 at 09:13):

Thanks! I have just fixed the typos.

#### Johan Commelin (Jun 07 2023 at 09:15):

I think the first `H`

should be a `K`

#### Scott Morrison (Jun 07 2023 at 09:23):

What about `opcycles`

? `coker_cycles`

?

#### Joël Riou (Jun 07 2023 at 09:35):

`opcycles`

seems good to me!

#### Johan Commelin (Jun 07 2023 at 10:46):

`popcycles`

, `popsicles`

?

#### Joël Riou (Aug 12 2023 at 09:56):

On my draft branch `jriou_localization`

(#4197), in the files which are using homology (like group cohomology), I have managed to replace the current homology API by the new API which I have been developing. I had to refactor part of the API for projective/injective resolutions and left/right derived functors. Currently, the PRs I have done on the new homology API mainly consist of the addition of new files in `Mathlib.Algebra.Homology.ShortComplex`

because so far this is about the homology of short complexes (i.e. two composable maps whose composition is zero). Eventually, the homology of `HomologicalComplex`

shall use this new API. In order to keep the PR process into a sequence of reasonably long PRs, I think that there will be a need for a transitory situation where both API exists for the homology of homological complexes. Then, the overall plan would be as follows :

- continue developing
`Mathlib.Algebra.Homology.ShortComplex`

- when it is complete, do a PR which basically just renames
`HomologicalComplex.homology`

as`HomologicalComplex.homology'`

(and similarly for other notions for which there could be a name clash, e.g.`QuasiIso`

) - develop the new API as
`HomologicalComplex.homology`

- refactor step-by-step parts of
`mathlib4`

which are using`homology'`

in order to use`homology`

(this might be slightly longer PRs, because for example group cohomology depends on Ext groups, which also depends on left derived functors) - remove the old
`HomologicalComplex.homology'`

API when it is no longer used

Does this seem ok?

#### Johan Commelin (Aug 12 2023 at 10:04):

If you have already done all the work of refactoring the APIs, we could even consider merging a monster PR that switches over the APIs.

But it would be nice if that is the only thing that the PR does...

#### Johan Commelin (Aug 12 2023 at 10:05):

But having two APIs coexist for a while might also be nice for projects depending on the old API. (Not sure how many such projects exist...)

#### Scott Morrison (Aug 13 2023 at 03:00):

I think it will be both easier to review, and easier to understand the history, if we have an intermediate period with both APIs. Usually we would want to avoid this duplication, but I think we are sufficiently confident that this refactor is going to work that we can go ahead.

Last updated: Dec 20 2023 at 11:08 UTC