[FOM] Grothendieck foundations in second order arithmetic

[Colin McLarty]

For a while I worked with limited comprehension, which got the whole
Grothendieck toolkit into simple type theory.  Harvey urged a
different strategy for going much lower by using all of replacement
but limited power set in the form of  ZFC[n] which is ZFC with power
set restricted to just n successive power sets of omega.  And Jeff
Hirst urged the importance of considering multiple different proofs of
the theorems to be reduced.

That has worked to get the central device of cohomological number
theory into second order arithmetic -- in the proof-theoretically
equivalent form ZFC[0].  So this part of cohomology reaches the
territory of reverse math but I have not gone there.

The result, as I have it so far, is that ZFC[0] supports derived
functor cohomology over any Noetherian ring.

I expect this to extend directly to standard scheme cohomologies for
Noetherian schemes, and so most uses of cohomology in number theory.
But of course lower-strength foundations require checking many more
details and I have not finished this yet.

The key step is to show every module embeds in an injective module.
Baer originally proved this by transfinite induction later used by
Grothendieck.  Eckmann-Schopf proved it by adjoint functors.
Eckmann-Schopf works more naturally than Baer (so far as I have seen)
in a context with limited comprehension.  So it gets the whole tookit
for arbitrary sites into simple type theory.  But number theory does
not use arbitrary sites and Baer's proof works well here.

Baer takes any module M on any ring R and expands it a suitable
transfinite number of times.  He needs to show every homomorphism from
an ideal of R into the union of the expanded modules actually goes
through one of the expanded ones.  Working over arbitrary rings, he
iterates as many times as the successor cardinal to the cardinality of
R so a cofinality argument finishes the proof.  But even if R is
countable this is induction on Aleph-1.

For R Noetherian, since each ideal is finitely generated, it suffices
to expand M all finite numbers of times.   We need axiom of infinity
but no larger cardinal.

The uncanny thing about working with ZFC[0], to me, is that you
(usually) do not pose cardinality restrictions in statements of
theorems.  You state theorems quite generally and merely do without
any means of getting uncountable sets.  This makes a real difference
since it lets you posit one or more successive powersets of omega if
you want to -- either as new axioms, or as hypothesis to some theorem
-- and the theorems still hold.

Noetherianness is a kind of cardinality condition, but the proof on
injectives poses no restrictions at all on the modules and none on the
size of the ring R.

best, Colin