A Foundation for Synthetic Algebraic Geometry
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909500286435328 |
|---|---|
| author | Cherubini, Felix Coquand, Thierry Hutzler, Matthias |
| author_facet | Cherubini, Felix Coquand, Thierry Hutzler, Matthias |
| contents | This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt. The Zariski topos consists of sheaves on the site opposite to the category of finitely presented algebras over a fixed ring, with the Zariski topology, i.e. generating covers are given by localization maps $A\to A_{f_1}$ for finitely many elements $f_1,\dots,f_n$ that generate the ideal $(1)=A\subseteq A$. We use homotopy type theory together with three axioms as the internal language of a (higher) Zariski topos. One of our main contributions is the use of higher types -- in the homotopical sense -- to define and reason about cohomology. Actually computing cohomology groups, seems to need a principle along the lines of our ``Zariski local choice'' axiom, which we justify as well as the other axioms using a cubical model of homotopy type theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2307_00073 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | A Foundation for Synthetic Algebraic Geometry Cherubini, Felix Coquand, Thierry Hutzler, Matthias Algebraic Geometry Logic 14A99 (Primary), 03B38, 18N99 (Secondary) This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt. The Zariski topos consists of sheaves on the site opposite to the category of finitely presented algebras over a fixed ring, with the Zariski topology, i.e. generating covers are given by localization maps $A\to A_{f_1}$ for finitely many elements $f_1,\dots,f_n$ that generate the ideal $(1)=A\subseteq A$. We use homotopy type theory together with three axioms as the internal language of a (higher) Zariski topos. One of our main contributions is the use of higher types -- in the homotopical sense -- to define and reason about cohomology. Actually computing cohomology groups, seems to need a principle along the lines of our ``Zariski local choice'' axiom, which we justify as well as the other axioms using a cubical model of homotopy type theory. |
| title | A Foundation for Synthetic Algebraic Geometry |
| topic | Algebraic Geometry Logic 14A99 (Primary), 03B38, 18N99 (Secondary) |
| url | https://arxiv.org/abs/2307.00073 |