80
$\begingroup$

Vladimir Voevodsky has made several contributions in abstract algebraic geometry, focused on the homotopy theory of schemes, algebraic K-theory, and interrelations between algebraic geometry, and algebraic topology.

Voevodsky was awarded the Fields Medal in 2002. Sadly, he died September 30, 2017.

Can one draw a general picture of his works?

Any expository reference will be appreciated.

$\endgroup$
8

2 Answers 2

39
$\begingroup$

Perhaps one of the biggest ideas that VV was pursuing is the Initiality Conjecture for Martin-Löf type theory (with universes). A rough idea is that from the rules for a type theory, one can define a category (the syntactic category) that has certain structure depending on which rules are admitted to the type theory. For instance, dependent products correspond to being locally cartesian closed. For any specific type theory, the idea is that the syntactic category it gives rise to is the initial category with that specific structure, in the sense there is a unique functor (preserving appropriate structure) from it to any other such category. What this means is that if one proves a theorem using the type theory, it is automatically true in all categories with that structure. And, vice versa, if it is provable in the language of that kind of structured category, then it is provable in the type theory.

Also, to quote from VV:

"The importance of the initiality conjecture lies in the fact that it provides us with the only known way to prove that type theories such as the Martin-Lof type theories, Calculus of Constructions or Calculus of Inductive Constructions remain consistent after one adds to them axioms such as the axiom of excluded middle or the axiom of choice". (last slide here)

The Initiality Conjecture for MLTT is something that the type theory community expected to be true, based on proofs for much more restricted type theories, but the details of even those were incredibly fearsome. Thomas Streicher wrote a ~300 page book to prove the case of the Calculus of Constructions, a weak subset of the underlying type theory of Coq.

VV's work on mathematising the abstract structure of type theories, so they can be studied and worked with in a proof assistant, was a large part of what he was doing in the last few years. His papers on B- and C-systems [1] were extending work by, for example, Cartmell and others on the type of structure a syntactic category has. Moreover I believe that formal proofs were given for all results in those papers.

Here's a quote by Peter LeFanu Lumsdaine, responding to a criticism by VV of the attitude that "everyone knows the IC is true...":

But I think the second criticism [by VV], on the status of the initiality of the syntactic category, is a bit harder to dismiss. I feel, like you [Mike Shulman] do, that it’s well-established, and we all know how to prove it, it’s just so long and ugly that no-one wants to write it out (and no-one would want to read it). But the more I try to defend it in my head against an imaginary inquisitor, the less comfortable I feel with the situation. “We all know it’s true.” “How? Is it proven?” “Well, no, but it’s a straightforward extension of an existing proof.” “How can you be sure?” “Well, if you understand Streicher’s proof, then you can see it’s easy to extend it.” “Are you sure you’re not missing some details?” “No, there aren’t any tricky details.” “Then why not write it up?” “Well, there are just so many fiddly details…”

So this is one of the things VV was hoping to prove, and formally, so this niggling issue could be put to rest.


[1] Recent published papers include:

see also his arXiv papers.

$\endgroup$
4
  • 1
    $\begingroup$ "I believe that formal proofs were given for all results in those papers" : I don't think so, but it's written in a style that should allow straightforward formalizations (using the UniMath library for instance). Otherwise very good answer. $\endgroup$
    – A. Bordg
    Oct 2, 2017 at 10:36
  • 1
    $\begingroup$ Vladimir coined this style the "formalization-ready" style. $\endgroup$
    – A. Bordg
    Oct 2, 2017 at 21:02
  • 1
    $\begingroup$ @AnthonyBordg my mistake, I mis-remembered. Here's an illustrative quote from VV on the matter: The methods of this paper are fully constructive and the style we write in is the “formalization ready” style where the proofs are spelled out in detail even when the assertion may appear obvious to the practitioners of a particular tradition in mathematics. This particular paper is written having in mind the possibility of formalization both in the Zermelo-Fraenkel set theory (without the axiom of choice) and its constructive versions... $\endgroup$
    – David Roberts
    Oct 3, 2017 at 0:39
  • 1
    $\begingroup$ ...and in any type theory including Church’s type theory or HOL. (A C-system defined by a universe category, p 1183) $\endgroup$
    – David Roberts
    Oct 3, 2017 at 0:40
29
$\begingroup$

Aside from his work on the foundations of mathematics, which others have already elaborated on, earlier in his career Voevodsky also proved the Milnor conjecture in algebraic geometry. The Milnor conjecture relates Milnor K-theory to Galois cohomology (or, equivalently, etale cohomology, since we are dealing with the case of a field). It is related to Hilbert's Theorem 90, which has historical origins in number theory (going all the way back to Ernst Kummer's work in 1855).

Namely, in its modern formulation, Hilbert's Theorem 90 says that $H^{1}(G(k_{s}|k);k_{s}^{*})$ is trivial. By the Kummer exact sequence, we then get the result that

$k^{*}/2\cong H^{1}(G(k_{s}|k);\mathbb{Z}/2)$.

Milnor's conjecture states that

$K_{n}^{M}(k)/2\cong H^{n}(G(k_{s}|k);\mathbb{Z}/2)$

for $k$ of characteristic not equal to $2$, where $K_{n}^{M}(k)$ is the Milnor K-theory, defined as the quotient of the tensor algebra of $k^{*}$ by the ideal generated by $a\otimes(1-a)$ for $a\in k^{*}-\{1\}$. For $n=1$ we have $K_{1}^{M}(k)=k^{*}$, and the statement of the Milnor conjecture is the same as the result given above. We can therefore think of the Milnor conjecture as its generalization to higher $n$.

As a side comment, I'll mention that Milnor K-theory may be viewed as an "approximation" to algebraic K-theory, and agrees with Quillen's later definition of algebraic K-theory for $n\leq 2$. Algebraic K-theory is very much related to ideas in homotopy theory in algebraic topology.

A survey of Voevodsky's proof can be found here:

Voevodsky's Proof of Milnor's Conjecture by Fabien Morel

Later on Voevodsky also worked on the more general version of the Milnor conjecture, the Bloch-Kato conjecture, also now known as the norm residue isomorphism theorem. Material on the Bloch-Kato conjecture may be found on Charles Weibel's website:

Charles Weibel's Home Page

In the course of his work on the Milnor conjecture and the Bloch-Kato conjecture, Voevodsky developed motivic homotopy theory. This is a version of homotopy theory for algebraic geometry, and in order to transplant this theory from algebraic topology certain technical obstacles must first be surmounted, such as the unit interval not being an algebraic variety, and so it must be replaced by the affine line $\mathbb{A}^{1}$. A nice introduction to these ideas may be found in the book "Motivic Homotopy Theory" by Dundas, Levine, Rondigs, Ostvaer, and Voevodsky himself.

Voevodsky also developed, for the same purpose, a triangulated category of "mixed motives". Mixed motives are a generalization of pure motives, which is related to the search for a "universal cohomology theory". An introduction to the theory of motives, which however stops just short of mixed motives, is here (I'm linking to the top level of the site, as per the author's request, so just look for the article in the sidebar):

Motives - Grothendieck's Dream by James S. Milne

It is worth noting that a theory of mixed motives does not exist at the moment - the triangulated category of mixed motives is kind of the "next best thing". Other approaches were made by Huber-Klawitter, Hanamura, and Levine. A more thorough discussion of these ideas can be found in the book Une Introduction aux Motifs by Yves Andre, or, for an English reference, there's also a brief discussion in the book Feynman Motives by Matilde Marcolli, or the following book available online:

Noncommutative Geometry, Quantum Fields, and Motives by Alain Connes and Matilde Marcolli

Finally, this is much more elementary, but I've found the following popular exposition (on video) by Voevodsky to be an abstract, yet intuitive, and ultimately elegant presentation of homotopy theory:

An Intuitive Introduction to Motivic Homotopy Theory by Vladimir Voevodsky

There's also a pdf transcript of that talk.

$\endgroup$
3
  • 2
    $\begingroup$ To say that the Milnor conjecture is "an analogue of Hilbert's Theorem 90 in number theory" is not correct. Hilbert 90 is a result in algebra, not number theory. Hilbert 90 has natural generalizations to Milnor K-groups. These are closely related to the Bloch-Kato (=BK-)conjecture. Voevodsky was not the only person involved in the proof of the BK-conjecture. A proof was announced in the early noughties, though a paper was published only years later in 2011. Whether a proof existed already several years earlier seems now questionable. $\endgroup$
    – user115371
    Oct 5, 2017 at 1:25
  • 2
    $\begingroup$ One person involved in the story claims that a gap was found (not in his contribution) that was never openly acknowledged until it was fixed years later. That the publication of a complete proof of BK took a very long time and was finally done by the mathematicians who did not contribute to the proof themselves seems to be caused by the fact that the main people involved were not all inclined to properly acknowledge the work of the other contributor and at some point stopped communicating. $\endgroup$
    – user115371
    Oct 5, 2017 at 1:25
  • $\begingroup$ Thank you very much for your comments. I have edited my answer to reflect your corrections. $\endgroup$ Oct 6, 2017 at 7:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.