Zulip Chat Archive

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.)