The large structures of Grothendieck founded on finite order arithmetic

TL;DR

This paper establishes that advanced cohomological structures like toposes and derived categories can be founded on finite order arithmetic, aligning their formal foundations with practical mathematical usage.

Contribution

It formalizes the foundations of key cohomological tools at the level of finite order arithmetic, the weakest possible foundation consistent with their practical use.

Findings

Formalization of EGA and SGA theorems within finite order arithmetic

Derived categories founded on finite order arithmetic

Shows these structures are compatible with minimal set-theoretic assumptions

Abstract

Such large-structure tools of cohomology as toposes and derived categories stay close to arithmetic in practice, yet existing foundations for them go beyond the strong set theory ZFC. We formalize the practical insight by founding the theorems of EGA and SGA, plus derived categories, at the level of finite order arithmetic. This is the weakest possible foundation for these tools since one elementary topos of sets with infinity is already this strong.