FOM: FLT --- another expert speaks

[Mathias]

   ardm at univ-reunion.fr writes: 

       I too have consulted an anonymous expert, who replies: 

Hi. I'm in a bit of a rush, but

> There is a big discussion going on in the email group FOM 
> (Foundations of Mathematics) about whether or not Grothendieck 
> universes are used in an essential way in Wiles' proof. 

I believe that probably the technically correct response is
that they are used, but not in an essential way. The thing
about writing books/papers on abstract algebraic geometry
is that it makes things much easier notationally if one
assumes that there are arbitrarily large universes; but
if one is careful (e.g. one replaces "category of all schemes"
with "category of all schemes of cardinality at most 2^2^2^2^2^aleph_0")
then one tends to be able to get by to all intents and purposes
without universes. 


On the post you sent me:

> Friedman's anonymous expert was simply wrong.

I think this comment is a little OTT.

>         Wiles's article "Modular elliptic curves and Fermat's last theorem"
> uses Grothendieck duality over fields, and cites Altman and Kleiman
> INTRODUCTION TO GROTHENDIECK DUALITY THEORY on page 486, just about in the
> middle of the body of the paper. Altman and Kleiman use sets whose existence
> is equivalent to existence of a Grothendieck Universe.

I can certainly go and look in Altman-Kleiman for this (it's at work
and I'm not; maybe I'll get back to you on this). But my recollection
of Wiles' proof is that the only time he really uses any kind of
Grothendieck duality is just for dealing with certain integral
models of modular curves over the p-adic integers; and all the curves in
question only have rather mild singularities, so my gut feeling is that the
full force of the duality theory needed in Altman-Kleiman will
almost certainly be way too much, and one could prove all that Wiles neede
"by hand". I can't be 100% sure of this
because I don't have anything to hand at the minute---I'm not at work---but...

> >>I have been told that there is absolutely no trace back from the references
> >>used in the body of the Wiles paper to Universes (of Grothendieck).

...although one could argue that this is technically incorrect, my
guess is that any reference to Grothendieck Duality in Wiles could be
proved without universes, especially as everything is either smooth or
nearly so. Wiles is working with curves over the rationals and
everything is rather concrete. 

> It is surprising
> that Friedman would use this kind of impressionistic evidence in a serious
> investigation of foundations.

I think this is also OTT: I could certainly imagine a scenario
where Friedman's expert knew enough about the proof of FLT to know
that any appeal to Grothendieck duality within it does not use
universes in any serious way. Is the writer seriously claiming
that he knows that Wiles' use of duality really _does_ use universes in
an essential way, or is he just claiming that it's still unclear?
In the latter case his argument seems to be flawed, because
he's claiming that he doesn't know the answer but also seems
to be deducing that Friedman's expert doesn't either.