[FOM] Grothendieck foundations version 2.0

[Colin McLarty]

This July Harvey urged ZFC with restricted powerset as an approach for
getting the chief working tools of cohomological number into n-th
order arithmetic for some relatively low n,  That idea is still
progressing.  Already the pursuit of it, combined with the technique
of Takeuti's conservative extension of PA, has sharply improved on my
February ArXiv article.

I now formalize the entire Grothendieck tool kit at the strength of
finite order arithmetic.  In other words at the strength of simple
type theory with infinity.  This includes even the largest scale
structures.  Specifically: derived categories for duality, and the
2-category of geometric morphisms between toposes.

This does not get as low as n-th order arithmetic for some fixed
finite n, but is reasonably weak and yet quite general.  It is natural
for the Grothendieck toolkit as a whole, while of course no single
application uses the whole.

Besides that the argument is now simpler, the technical advances since
my talks in July are:

1) a proof using only bounded separation that every module, or sheaf
of modules over any Grothedieck site, has an infinite-length injective
resolution.  Of course the resolution can be 0 from some point on in
some cases, but in general it cannot.

2) a conservative extension of Mac~Lane set theory with proper classes
and collections of them, modelled on Takeuti's conservative higher
order extension of PA.

A revision of the ArXiv article, re-titled "A finite order arithmetic
foundation for cohomology," is on my web page at

http://www.cwru.edu/artsci/phil/Derived_functor.pdf

and is scheduled to go on the math arXiv tonight (Monday) at midnight,
or as arXiv puts it 00:00 Tuesday.

best, Colin