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