Homology refactor

Stream: homology

[Joël Riou]

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]

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

[Joël Riou]

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]

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

[Joël Riou]

Thanks! I have just fixed the typos.

[Johan Commelin]

I think the first H should be a K

[Scott Morrison]

What about opcycles? coker_cycles?

[Joël Riou]

opcycles seems good to me!

[Johan Commelin]

popcycles, popsicles?

[Joël Riou]

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]

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]

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]

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.