Towards Dold-Kan equivalence in mathlib

Stream: new members

[Joël Riou]

Hi. I am Joël Riou, a mathematician from University Paris-Saclay. My main mathematical interests are algebraic topology and algebraic geometry. I also have some background in various programming languages including functional languages like Scheme or Caml. Long ago, I heard a talk by V. Voevodsky about homotopy type theory, and more recently I heard about the formalisation in Coq of the Feit-Thompson theorem, but it is only very recently that I heard about Lean. As I was about to talk about the Eilenberg-Maclane-Breen-Deligne theorem in an ongoing "condensed mathematics" workshop in Orsay, Patrick Massot mentioned the formalisation process of mathematical definitions and theorems that had been going on in Lean. This was only about one month ago, and then I started to try using Lean.

While I was preparing my talk on the EM-Breen-Deligne theorem, I went into the details of the original paper by Albrecht Dold on the Dold-Kan equivalence, and thought that this result would be a nice test case for me with Lean. A starting point is already in mathlib, which is algebraic_topology.normalized_Moore_complex. Over the last few weeks, I have constructed the alternating_face_map_complex in Lean and defined almost automatically the canonical embedding of the normalized_Moore_complex in the alternating_face_map_complex, see https://github.com/joelriou/dold-kan/blob/main/alternating_face_map_complex.lean

Including this in mathlib would certainly be useful steps towards the proof of the Dold-Kan equivalence. Also, the alternating_face_map_complex is used basically everywhere in the definition of (co)homology theories, like singular homology, group cohomology, etc.

I would be happy to contribute to mathlib on this and related subjects. I would certainly be ready to do a PR on mathlib very soon. My GitHub username is "joelriou".

[Kevin Buzzard]

@maintainers

[Kevin Buzzard]

Presumably Patrick told you about Commelin's modification of the argument in analytic.pdf which avoids the full Breen-Deligne theorem?

[Joël Riou]

Yes, exactly! But, fortunately, the previous talk in the workshop had already used the Breen-Deligne theorem, so that my talk was not cancelled :-)

[Markus Himmel]

Invite sent! https://github.com/leanprover-community/mathlib/invitations

[Joël Riou]

Thank you!

[Adam Topaz]

@Joël Riou we have a fair amount of code on the alternating face map complex in the LTE repo, see e.g. https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/simplicial/complex.lean

How does your code compare to this?

[Joël Riou]

Ah, the main difference I see is that I have done the simplicial version instead of the cosimplicial version. The normalized Moore complex that is already in mathlib is the homological (simplicial) one, which is the reason why I did it this way. Also, I have not dealt with (co)-augmentations. I have split the core details of the proof of "d ≫ d = 0" in different separate lemmas, because I wanted to use finset.sum_involution. (Note: the core of the proof is also similar to a result that Shenyang Wu, a student of Kevin Buzzard had obtained when studying group cohomology
https://github.com/Shenyang1995/M4R/blob/master/src/cochain.lean which I found only a few days ago; he did it also with finset.sum_involution.)

[Patrick Massot]

I'm pretty impressed that you managed to do that without asking any question here. And the code style is very encouraging, modulo some lonely closing braces and some extra indentations (see the mathlib style guide).

[Joël Riou]

Thanks Patrick! You know, there are some great talks about Lean on YouTube ;-)

[Kevin Buzzard]

@Joël Riou did you see my group-cohomology branch? i proved d^2=0 in a better way than Shenyang: https://github.com/leanprover-community/mathlib/blob/0c62c04032fc7e3ff7e5958cec9fae5ddef30e3e/src/algebra/group/cohomology.lean#L162

[Adam Topaz]

Kevin I think the hope is to eventually use the general alternating face complex to define group cohomology?

[Joël Riou]

@Adam Topaz @Kevin Buzzard Indeed, once you have the classifying space of a group G (as a simplicial set), you may easily define the complex which computes the group cohomology (with constant coefficients). More generally, using the simplical set EG (the universal cover of BG), which is equipped with a G-action and a morphism EG -> BG, if we have a G-module M, one may construct a cosimplicial group "Hom_G(EG,M)" whose alternating (co)face map complex computes the group cohomology. Then, the idea would be to identify (easy part) this group with the explicit construction of G-cochains, and then, via this isomorphism, recover the formulas for the differentials... (This is not the way it is done in standard textbooks on group cohomology or Galois cohomology [like Serre, _Galois cohomology_], so that the more explicit approach has its own beauty. Also, if some people want to do continous cohomology or l^2-cohomology, it seems important to keep the explicit G-cochains approach.)

Anyway, regarding my first attempt on the alternating face map complex, before anything goes into mathlib, it seems it might be better to wait until I do some more progress towards the Dold-Kan equivalence between the categories of simplicial abelian groups and homological chain complexes. Then, we could see which parts may factor one another...

[Scott Morrison]

I think it's a good idea to PR initial segments of your work as often as possible, to avoid work getting stranded / orphaned. There's also a good social dynamic getting regular feedback on your progress -- both because it improves the contributions, and it's fun. :-) It's remarkably easy to refactor mathlib, so don't get hung up on the idea that you should only PR some work once the subsequent stage has already been done.

[Adam Topaz]

I'll second what Scott said. The alternating face complex along with the normalized Moore complex would be more than enough for one PR

[Anatole Dedecker]

A bit off-topic, but it's nice to see the Lean team of Orsay growing ! :smile:

[Johan Commelin]

@Joël Riou I left a first set of comments on your PR. Please let me know if you have any questions.

[Joël Riou]

@Johan Commelin Thanks you very much. I am working at reducing the length of the proof a bit, following the ideas of the proof in the LTE repository. This is an occasion for me to learn some more Lean and mathlib :-) Should be ok within a few days.

[Joël Riou]

Well, it seems I have just obtained the following :

noncomputable def algebraic_topology.dold_kan.NΓ_equivalence : Π {C : Type u_1} [_inst_1 : category C] [_inst_2 : additive_category C],
  karoubi (simplicial_object C) ≌ karoubi (chain_complex C ℕ)

Here, karoubi is the pseudoabelianisation of a (pre)additive category. Then, if C is pseudoabelian (e.g. abelian), this easily gives the usual formulation of the Dold-Kan equivalence : simplicial_object C ≌ chain_complex C ℕ.

The code is at https://github.com/joelriou/dold-kan
It needs a lot of tidying... and it depends on some local modifications to other parts of mathlib, like the matter the definition of homotopy of complexes.

In order to do this, I have defined various notions related to pseudoabelian categories and I have slightly developped simplex_category (e.g. epi/mono factorisations). As I had noticed beforehand that the result would apply to general additive categories rather than only abelian categories, I have chosen a quite constructive approach of the (iso)morphisms that are involved. The plan is as follows:

• dold_kan1.lean: constructing a direct factor of the alternating face map complex which coincides with the normalized chain complex (and incidentaly prove that the inclusion is an homotopy equivalence),
• dold_kan2.lean: proving that the functor N : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ) reflects isomorphisms,
• dold_kan3.lean: constructing the functor Γ : chain_complex C ℕ ⥤ simplicial_object C in the other direction
• dold_kan4.lean/dold_kan5.lean: getting the equivalence by computing compositions in both ways of N and Γ

Before I consider PR-ing the core of this, I will have to reorganise a little bit the code (better names of lemmas, some more thinking about namespaces and location of files). The first thing I would PR in the more near future might be the parts about epi/mono factorisation in simplex_category and some results about pseudoabelisanisation (for which I would suggest the shorter name "karoubi").

[Kevin Buzzard]

@Amelia Livingston didn't you mention Dold-Kan in your talk last Thurs?

[Johan Commelin]

@Joël Riou Wow! That's a nice result