Milestone: B_{dR}

Stream: mathlib4

[Kevin Buzzard]

I didn't see it talked about elsewhere, but #26388 by @Jiang Jiedong brings Fontaine's period ring $B_{dR}$ a.k.a docs#BDeRham to Mathlib. I think it is an extraordinary milestone. When we have etale cohomology over the line we will easily be able to state Fontaine's profound conjectures in $p$-adic Hodge theory about the relationship between etale and de Rham cohomology for $p$-adic varieties, analogous to the classical results relating singular and de Rham cohomology for real manifolds.

For many years I did not remotely think that the idea of formalizing $B_{dR}$ was a feasible goal -- in the 2010s it felt completely out of reach. But then out of the blue (for reasons that were never very clear to me but I was extremely grateful nonetheless) in 2020 @Johan Commelin and @Rob Lewis formalized the theory of Witt vectors and I quickly realised that Fontaine theory was theoretically in scope (and also would be a gigantic amount of work). @María Inés de Frutos Fernández started as my post-doc at around that time and (as well as working on global objects such as the adeles) began the task of formalizing the relevant part of the foundational book of Bosch, Guentzer and Remmert on nonarchimedean analysis which we needed to get started. Her tireless work ultimately led to $\mathbb{C}_p$ a.k.a. docs#PadicComplex, the completion of an algebraic closure of the $p$-adic numbers $\mathbb{Q}_p$ and a $p$-adic analogue of the complex numbers, as the notation suggests. Rob Lewis had defined $\mathbb{Q}_p$ in the 2010s as one of his first projects; this is the non-archimedean analogue of the real numbers. The hard work that Maria Ines did is to build a general theory of extensions of nonarchimedean norms which can be applied to extend the $p$-adic norm on $\mathbb{Q}_p$ to its algebraic closure; then @Patrick Massot 's theory of completions of topological fields, developed as part of the perfectoid project also in the 2010s, kicks in. With $\mathbb{C}_p$ formalized we could now in theory go on to construct a perfectoid space with one point; famously the perfectoid publicity stunt gave a formal definition of Scholze's revolutionary idea but in 2019 the library was sufficiently underdeveloped that it was impossible to construct any examples at all other than the empty type. Of course the main difficulty now is that nobody ported the perfectoid project from Lean 3 :-) (the correct next step towards perfectoid spaces is to develop the theory of Huber rings and Huber pairs by the way; the recent work of @Adam Topaz and others on valuations now means that we're ready for this).

After $\mathbb{C}_p$ the next natural step was $B_{dR}$ (the de Rham period ring) and $B_{cris}$ (the crystalline period ring). Maria Ines also reduced building $B_{dR}$ to the construction of the so-called "theta map", but the crystalline period ring $B_{cris}$ turned out to be far harder because the entire theory of divided power structures and divided power completions needed to be developed. Maria Ines started work on this with @Antoine Chambert-Loir , and during this time Antoine found what seems to be a genuine error in the original literature on the subject, which stunned me (not least because I was planning on using this theory in my proof of FLT at one point; I quickly changed direction), although it turned out that Brian Conrad knew another proof (which was fortunate because all of the people involved in the original development of crystalline cohomology had died). On the other hand $B_{dR}$ felt close! We just needed someone to do the hard work of getting the theta map over the line. This is where Jiang Jiedong stepped in, who in a long serious of PRs has developed the theory in the correct modern generality, namely Scholze's viewpoint of the subject, with tilting (originally formalized by @Kenny Lau as part of his Masters project under me in 2020) and untilting, more of the theory of Witt vectors, and finally the theta map, thus leading us to $B_{dR}$.

I have always been fond of getting nonarchimedean versions of mathematical objects formalized. My PhD student @Ashvni Narayanan formalized the $p$-adic zeta function in her thesis before @David Loeffler had done the classical Riemann zeta function; the FLT project aims to give a sorry-free proof of the finite-dimensionality of an exotic space of automorphic forms with $p$-adic coefficients and perhaps we'll do it before the analysts have proved finite-dimensionality of classical spaces of modular forms (edit: David Loeffler points out that we already lost -- finite-dimensionality of classical spaces of modular forms is in the sphere-packing repo thanks to @Chris Birkbeck ) . Maria Ines' work on $\mathbb{C}_p$ is another nonarchimedean version of a classical object, although mathlib has had $\mathbb{C}$ for many years now; in fact it was my very first PR to mathlib3 (and indeed my very first open source PR) which got it there! Having said that, Kazuya Kato always argued that the true $p$-adic analogue of the complex numbers was $B_{dR}$ ($\mathbb{C}_p$ does not contain the $p$-adic analogue of $2\pi i$, the classical factor which one picks up when integrating $1/z$ around the unit circle). Now we have it.

It has been an extraordinary journey getting to $B_{dR}$, and let me stress that whilst I have been encouraging people in this direction for many years now, I wrote essentially none of the relevant code; essentially all of it has been done by young people, many of whom have had to put up with me droning on about what a great milestone it would be without me actually ever doing anything about it. Thank you so much to everyone involved. Now we have even more reasons to get etale cohomology over the line!

[Ruben Van de Velde]

Sounds like someone should write a blog post!

[Kevin Buzzard]

I did think about doing that, but I felt that I wanted to namecheck so many people who had been part of the journey that I thought I'd start with the above.

[Etienne Marion]

That sounds like an incredible journey! I have no idea of what are the maths behind, but I find this kind of stories very interesting and also kind of entertaining (especially the parts where formalization uncovers errors in the literature). Congratulations to the people involved!