Dold-Kan correspondence

Stream: PR reviews

[Joël Riou]

Over the last few days, I have tidied a significant part of the code of a proof of the Dold-Kan correspondence (equivalence between categories of simplicial objects and chain complex in an abelian category). As there are more than 20 files and about 3500 lines of code, I would like to be sure what is the best way how to proceed. The whole code is at https://github.com/joelriou/dold-kan
The dependency graph of the files is
dependency graph
I was thinking about PRing about one file at a time, starting with the right branch of the graph which leads to homotopy_equivalence.lean which contains a proof that the normalized Moore complex of a simplicial object in an abelian category is homotopy equivalent to the alternating face map complex. Does it sound ok?

[Riccardo Brasca]

I don't know the math well, but don't be afraid about PRing small technical lemmas. You can explain in the description what the final goal is, but there is need to a have an interesting result in all PR.

[Scott Morrison]

Yes, one file at a time is an easy default approach when you've taken the effort already to organise the work into files! Typically it results in digestible size PRs, too.

[Scott Morrison]

I'm excited to see this in mathlib!

[Scott Morrison]

(and I think Riccardo left out a critical "no" in the phrase "no need" :-) It's completely fine to have trivially small PRs.)

[Scott Morrison]

When making long strings of PRs like this, don't hesitate to keep pinging us here to review, especially whenever you're currently up to an easy one. I've done long strings of PRs before, and it can be discouraging how slow it is: you're allowed to crack the whip. :-)

[Scott Morrison]

Further, it can be tempting to make lots of the PRs at once, and labelled them all as blocked-by-other-PR. In my experience this leads to wasting lots of time merging or rebasing... Your call. :-)

[Joël Riou]

Thanks for the encouragements! The difficulty I anticipated in the process is that in my first few PR for this, I will be dealing with objects which do not obviously seem to be interesting at all (like the null homotopic maps defined in homotopies.lean): they become really interesting only after a long string of lemmas have been obtained. So this is the reason why I wanted to give the full picture here so that people can check that the whole files compile and give nontrivial theorems! I will certainly proceed one PR at a time (as my multitasking abilities are low...).

[Arthur Paulino]

I like Kyle's approach of opening a huge PR just to provide the full picture and then opening small PRs until the big PR becomes obsolete

[Kevin Buzzard]

Yes Joel, don't worry about PRing objects which don't seem interesting -- there will be maintainers who know what you're doing. I guess PRs which add a whole bunch of definitions without using them at all are a bit scary because then people don't know for sure if the definitions are appropriate or will work. But PRs which add one definition and then prove 4 lemmas about it are fine.

[Kevin Buzzard]

Also, a general rule is max 150-200 lines per PR, otherwise people don't review it because there are easier things to review :-)

[Joël Riou]

In #12742, I add three lemmas about homological complexes. After this PR, I should be able to start PRing material more directly related to the Dold-Kan correspondence.

[Joël Riou]

In #13028, I add a compatibility of the alternating face map complex functor with the application of additive functors between the underlying preadditive categories.

[Scott Morrison]

Reviewed.

[Joël Riou]

In #13085, I introduce null homotopic maps which shall play a critical role in my formalisation of the proof of the Dold-Kan correspondence.

[Joël Riou]

In PR #14044, I prove technical lemmas about face maps and the null homotopic maps defined in the previous PR #13085. This PR is presumably the most technical in the whole proof of the Dold-Kan correspondence.

[Joël Riou]

Is it possible to merge #14044 in a near future? I promise the next PR in this series will be easier to review!