FOM: Grothendieck universes

[Colin McLarty]

        I said Grothendieck believes cohomology in number theory can have no
genuine mathematical meaning without universes (specifically, without
derived functor cohomology)

Steve Simpson replied:

>Did Grothendieck really say things like this?  If he did, it's
>interesting from at least a sociological point of view.

        Yes. The passages I think of are in his unpublished, and 1250 page
long, memoire "Recoltes et Semailles". Over the weekend I will look for good
examples. He opposes "excessive abstraction" and purely technical
"mathematics as sport" and feels his approach is the only salvation from that.

        I do not say all his heirs in number theory share this attitude.
They all share his apparatus of scheme theory and cohomology.

>Do you agree with ``Grothendieck and his heirs'' that the proofs in
>question are essential uses of Grothendieck universes?

        Of course "essential" here does not mean "formally ineliminable in
ZFC proofs of the theorems". It means essential to genuine mathematical meaning.

        I think it is probably true, but events could refute it. People
might find a new approach to these number theoretic proofs that does not use
cohomology (they certainly will for some theorems). Or they might find
systematic approaches to cohomology, actually usable in exposition from the
textbook level up, that do not use derived functors. 

>  Do you agree
>with ``Grothendieck and his heirs'' that the well known methods of
>eliminating Grothendieck universes from these proofs are
>mathematically meaningless?

        Grothendieck (and even I) knows the methods are *quite* meaningful
mathematically. They have real, practical importance, since they are also
the methods for calculating specific cohomology groups in particular cases.
He uses them. 

        I said Grothendieck (and not all his heirs) believes that using
these methods at all levels to eliminate all use of universes in practice,
would yield mathematically meaningless proofs. The general theorems, which
explicitly refer to universe-sized sets, are indispensible to mathematical
meaning. I see that no one yet publishes proofs in cohomological number
theory without these theorems, even though it is well known how you could in
principle. So I incline to say Grothendieck is right.