[FOM] FLT and ZFC, again

[Timothy Y. Chow]

Here are some further comments by the anonymous number theorist.

> Let me say a little more about the issue, as I understand it.
> 
> If X is a topological space and F is a sheaf of abelian groups on X, how
> are we going to compute the cohomology of F? Here are 3 (count 'em!)
> definitions of the cohomology groups.
> 
> 1) Consider the global sections functor on the (hugely gigantic) category
> of all sheaves of ab gps on X. It's left exact so by some mystical
> meta-mathematics (which can be formalised within ZFC if one assumes that
> a universe exists) it will have derived functors R^n; define the
> cohomology H^n(F) of F to be R^n(F).
> 
> 2) Let's write down (even though it'll be really messy to do explicitly)
> an injective resolution of F: 0->F->I0->I1->I2->.... Now let's take global

> sections I0(X)->I1(X)->I2(X)...and take the homology of this complex; 
> the group we get in degree n will be H^n(F). Now check that the 
> definition is independent of choices and satisfies the usual things that 
> cohomology is suppose to do. Note that in this definition I am not
> even *using* the notion of a *functor* or a *category*! Given a sheaf F
> and an integer n>=0 I am constructing a group H^n(F). I am not even going
> to attempt to formalise the statement that H^n is a "map" from "all sheaves"
> to "all abelian groups", because in the end, in the proof of any theorem I
> write down I'll only be taking the cohomology of all the sheaves in some
> *set*---I can be absolutely sure of this because the cardinality of the
> data comprising any sheaves that I will consider in any proof of any paper
> I've written will be at most
> powerset(powerset(powerset(powerset(powerset(reals))). That is a fact that
> *needs to be checked* if you're going to be super-pedantic, but is
> *absolutely trivial to check* in *any* given case. Any
> "working" mathematician will see instantly if suddenly some construction
> is going to throw up sets of arbitrarily large cardinality---and outside
> of logic does this really ever happen??
> 
> 3) Let's do the classical thing: let's write down a cover and compute
> Cech cocycles modulo coboundaries. This might not give the right answer,
> because the cover might not have been fine enough. So let's take the limit
> over all covers and define H^n(F) to be this limit; this is OK because the
> class of all covers of a top space has a set which is cofinal in it, and
> we can take limits over sets. And again I will not attempt to formalise
> the notion that H^n is a "functor": it suffices to think of it as a map on
> a huge set, for my applications.
> 
> Now if you give me a top space and a sheaf I can "prove" that all three
> constructions give the same answer. But secretly, I can't, because
> secretly I know that (1) "doesn't make sense". But I can prove that
> 2 and 3 give the same answer! I secretly know that I might have dabbled a
> little bit with mathematics outside of ZFC in definition 1, and I nearly
> did in definition 3 as well, but I was OK because although strictly
> speaking a cover of X can just be X itself, taken aleph_999 times, I can
> just throw out duplicates in my covers, and then every cover of X can be
> thought of as a set of subsets of X, so an element of the power set of the
> power set of X, so I never left the world of ZFC, and indeed I only even
> iterated the power set axiom twice.
> 
> Now let's imagine the next day someone wants me to compute some fppf or
> etale cohomology groups. We're in exactly the same situation here: (1) is
> "meta-mathematics" but 2 is still fine and furthermore 3 is as well,
> although one has to think a little bit more about 3; one needs to check
> that the isomorphism classes of ***finitely-presented*** faithfully flat
> ring extensions of a ring R form a set---if one is so inclined. But again
> they *trivially* form a set: we're not even close to getting big here.
> 
> Furthermore, and somehow this is the crucial thing---I don't *care* that
> the class of all sheaves of ab gps on a top space aren't a set, because I
> never need to consider all of them. All the *constructions* I ever make
> only involve sets of size at most powerset(powerset(powerset(stuff I
> started with))), and all the theorems I use about these cohomology groups
> are "basic axiomatic properties of cohomology", every one of which can be
> explicitly verified to be *theorems* if you use definition (2) or (3)
> above [whereas they are basic consequences of the definitions if you use
> meta-definition (1)]. But secretly I am never using (1) because I secretly
> know that it goes beyond the boundaries of ZFC. But I never *tell* people
> that this is how I think:  because there are two kinds of people, right?
> Those that don't care about the issue, and those that do care, and the
> ones that do care have done the same as me: spent a day or two checking
> that there is nothing remotely resembling a problem in formalising the
> proof of FLT within ZFC. In fact I bet one can even jettison the axiom of
> replacement and formalise the proof within V_{omega+omega} or some such
> place, although I confess that I've never spent any time whatsoever
> checking _that_ statement!


And in response to William Messing's comments:

> Heh :-) Bill Messing is a bright guy! Our points of view are not
> inconsistent though; what he's saying is that one has to think about
> foundations when formulating certain statements involving morphisms of
> sites etc. What I'm saying is in an "application" of
> such results, i.e. when I'm talking about computing the
> cohomology of an algebraic variety or a set of algebraic
> varieties, the set-theoretic issues go away, because the details of the
> construction can all be reformulated at the very bottom of the hierarchy
> of sets, nowhere near universe-level.
> 
> I think I'm just repeating myself :-)

Tim