13
$\begingroup$

Is it known how much of ZFC is actually necessary for the basic, familiar constructions and theorems in sheaf theory, along the lines of section II.1 (and its exercises) in Hartshorne's "Algebraic Geometry" textbook?

I apologize for this strange question. Here is the motivation behind it: I am a mathematician who works automatically and implicitly in ZFC, like most users of this website. Last year some members of the philosophy department at my university showed me some old questions in metaphysics which seemed to me as though they ought to be approachable axiomatically. Indeed they were, and some of the structures studied by the philosophers turn out to be (non-obviously) equivalent to sheaves of sets on a certain topological space. I was able to make some progress on those problems by using some classical, elementary ideas in sheaf theory, particularly the equivalence of sheaves of sets and local homeomorphisms. My colleagues in philosophy are supportive of this, but they suggest that unrestrained use of the ZFC axioms to resolve questions in philosophy may open the door for argument from philosophers who have various kinds of skepticism about set theory, and that it is best to offer the argument in a way that uses only as weak of a fragment of ZFC as possible.

I spent a while looking over the proofs of the theorems from sheaf theory that I am using, and it appears to me that the proofs all work in ZAC (Zermelo set theory with choice), but perhaps one can go weaker still. The outcome will be better if this kind of work is done by someone that knows more set theory than I do, so I would be happiest if someone else has already figured out how strong a set theory is necessary for elementary sheaf theory. Is this already out there, somewhere, in the literature? I am not even aware of a journal where investigations of this kind would appear, but perhaps people working in some areas of foundations of mathematics have someplace where they figure out such things.

I apologize for my ignorance of foundations of mathematics, and I also apologize again for this very strange question.

Improve this question
$\endgroup$
8
  • $\begingroup$ Which “elementary ideas in sheaf theory” require the axiom of choice? It can probably be thrown away too. $\endgroup$
    – Dmitri Pavlov
    Commented May 14, 2020 at 3:04
  • $\begingroup$ I recall doing simple point-set manipulations with the topological spaces on which certain sheaves were defined, and finding that I was using AC to write every topological space as a disjoint union of connected open subsets. Should be easy, and perhaps you can do this without AC, though. I also used AC to get a well-ordering in order to make a transfinite induction work, in proving that an arbitrary union of connected open subsets, each of which can be connected to each other by a finite sequence of pairwise intersections, is also connected. But perhaps AC is not really necessary here either. $\endgroup$
    – user158035
    Commented May 14, 2020 at 15:35
  • $\begingroup$ You do not need the axiom of choice for either of these statements. The first statement is only true for locally connected spaces. In this case, the collection of all connected open subsets is disjoint and its union equals the entire space. The axiom of choice is not used in this argument. For the second statement, assume the union is not connected, and split it into two disjoint open subsets. For both subsets, find some element of the collection that has a nontrivial intersection with it (hence is fully contained within). The chain that connects these two subsets yields a contradiction. $\endgroup$
    – Dmitri Pavlov
    Commented May 14, 2020 at 17:27
  • 1
    $\begingroup$ No need to apologize! This a perfectly good, research-level question. I am myself curious if there is any choice hiding in more advanced parts of sheaf theory. $\endgroup$
    – Dmitri Pavlov
    Commented May 14, 2020 at 20:30
  • 1
    $\begingroup$ You should definitely not delete this question, or your account. It was an excellent question, well-motivated, showing your thinking etc. Others may well be wondering the same thing without the courage to ask. $\endgroup$
    – David Roberts ♦
    Commented May 14, 2020 at 20:43

1 Answer 1

Reset to default
13
$\begingroup$

Colin McLarty has looked into this

The large structures of Grothendieck founded on finite order arithmetic, Review of Symbolic Logic 13 issue 2 (2020) pp. 296--325, doi:10.1017/S1755020319000340, arXiv:1102.1773.

with abstract (emphasis added):

The large-structure tools of cohomology including toposes and derived categories stay close to arithmetic in practice, yet published foundations for them go beyond ZFC in logical strength. We reduce the gap by founding all the theorems of Grothendieck’s SGA, plus derived categories, at the level of Finite-Order Arithmetic, far below ZFC. This is the weakest possible foundation for the large-structure tools because one elementary topos of sets with infinity is already this strong.

In the arXiv version the abstract claimed all of EGA's theorems as well, but I haven't investigated why this was removed. Certainly it is generally considered that the axiom of Replacement is not needed for 'generic' (i.e. non-logical/set-theory) mathematics, hence for algebraic geometry generally. In particular, it's generally accepted (though one might have to check specific statements that seem very strong) that ETCS is sufficient as a foundation, roughly equivalent to, but slightly weaker than, what you call ZAC.

Improve this answer
$\endgroup$
5
  • $\begingroup$ I think he does still claim EGA, but doesn't mention it in the abstract "The first technical key here is: no theorem in Grothendieck’s Elements of Algebraic Geometry (EGA) or Seminar on Algebraic Geometry (SGA), outside of the appendix on set theory in SGA 4, needs either the unbounded axiom scheme of separation or the axiom scheme of replacement for its proof. §2.3 discusses those unneeded axioms". He also mentions in the introduction that ETCS is a suitable foundation for EGA and SGA. $\endgroup$
    – Will Sawin
    Commented May 14, 2020 at 2:01
  • $\begingroup$ @WillSawin thanks. I didn't bother to fight to get the published version to check. $\endgroup$
    – David Roberts ♦
    Commented May 14, 2020 at 2:02
  • 1
    $\begingroup$ Thank you David. This paper of McLarty's is really remarkable, and seems to be what I asked for, and then much more as well. $\endgroup$
    – user158035
    Commented May 14, 2020 at 15:24
  • $\begingroup$ does that mean the Fermat's last theorem can be proved in MacLane set theory (i.e. bounded Zermelo)? $\endgroup$
    – Zuhair Al-Johar
    Commented May 14, 2020 at 18:38
  • $\begingroup$ @Zuhair absolutely, and weaker foundations; this was the motivation for the paper. $\endgroup$
    – David Roberts ♦
    Commented May 14, 2020 at 20:45

You must log in to answer this question.