Differential Geometry of Synthetic Schemes

TL;DR

The paper develops a synthetic framework for algebraic geometry inside a higher topos by positing three axioms (Locality, Duality, and Zariski-local choice) and then defines formally étale, unramified, and smooth types via closed dense propositions. It then shows these fiberwise notions recover the classical notions through tangent-space criteria, notably proving that tangent spaces of smooth schemes are finite free over the base ring $R$. The work provides both internal characterizations (lift properties, Jacobian criteria) and external-like descriptions (standard étale/smooth presentations) that align with familiar local descriptions in algebraic geometry. By integrating duality between finitely presented and copresented modules and developing infinitesimal geometry inside type theory, the authors enable internal cohomological reasoning and concrete local descriptions of schemes and maps without leaving the synthetic setting.

Abstract

Synthetic algebraic geometry uses homotopy type theory extended with three axioms to develop algebraic geometry internal to a higher version of the Zariski topos. In this article we make no essential use of the higher structure and use homotopy type theory only for convenience. We define étale, smooth and unramified maps between schemes in synthetic algebraic geometry using a new synthetic definition. We give the usual characterizations of these classes of maps in terms of injectivity, surjectivity and bijectivity of differentials. We also show that the tangent spaces of smooth schemes are finite free modules. Finally, we show that unramified, étale and smooth schemes can be understood very concretely via the expected local algebraic description.

Theorems & Definitions (134)

• Definition 1.1.1
• Remark 1.1.2
• Definition 1.1.3
• Remark 1.1.4
• Definition 1.1.5
• Remark 1.1.6
• Lemma 1.1.7
• Proof 1
• Proposition 1.2.1
• Lemma 1.2.2