# 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`

?

Last updated: Aug 03 2023 at 10:10 UTC