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.
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.
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:
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.