{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:23:35Z","timestamp":1760081015940,"version":"3.37.3"},"reference-count":24,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2024,12,4]],"date-time":"2024-12-04T00:00:00Z","timestamp":1733270400000},"content-version":"unspecified","delay-in-days":64,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2024,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt (Kock (2006) [I.12], Blechschmidt (2017)). 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, that is, generating covers are given by localization maps for finitely many elements <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000239_inline1.png\"\/><jats:tex-math>\n$f_1,\\dots, f_n$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> that generate the ideal <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000239_inline2.png\"\/><jats:tex-math>\n$(1)=A\\subseteq A$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. 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 \u2013 in the homotopical sense \u2013 to define and reason about cohomology. Actually computing cohomology groups seems to need a principle along the lines of our \u201cZariski local choice\u201d axiom, which we justify as well as the other axioms using a cubical model of homotopy-type theory.<\/jats:p>","DOI":"10.1017\/s0960129524000239","type":"journal-article","created":{"date-parts":[[2024,12,4]],"date-time":"2024-12-04T07:42:26Z","timestamp":1733298146000},"page":"1008-1053","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":2,"title":["A foundation for synthetic algebraic geometry"],"prefix":"10.1017","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6589-1874","authenticated-orcid":false,"given":"Felix","family":"Cherubini","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5429-5153","authenticated-orcid":false,"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]},{"given":"Matthias","family":"Hutzler","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2024,12,4]]},"reference":[{"key":"S0960129524000239_ref8","first-page":"18","volume-title":"21st International Conference On Types for Proofs and Programs","author":"Cohen","year":"2015"},{"key":"S0960129524000239_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8640-5"},{"volume-title":"Cubical Interpretations of Type Theory","year":"2016","author":"Huber","key":"S0960129524000239_ref12"},{"key":"S0960129524000239_ref19","unstructured":"Myers, D. J. (2019a). Degrees, dimensions, and crispness (unpublished data). URL: https:\/\/www.felix-cherubini.de\/abstracts.html#myers (cit. on p.\u00a03)."},{"key":"S0960129524000239_ref23","unstructured":"The Univalent Foundations Program (2013). Homotopy type theory: Univalent foundations of mathematics. URL: https:\/\/homotopytypetheory.org\/book (cit. on p. 4)."},{"key":"S0960129524000239_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71104-2"},{"key":"S0960129524000239_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603153"},{"key":"S0960129524000239_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/BF02699258"},{"volume-title":"Semantics and logics of computation. Summer school at the Isaac Newton Institute for Mathematical Sciences","year":"1997","author":"Hofmann","key":"S0960129524000239_ref11"},{"key":"S0960129524000239_ref20","unstructured":"Myers, D. J. (2019b). Logical topology and axiomatic cohesion (unpublished data). URL: https:\/\/www.felix-cherubini.de\/abstracts.html#myers (cit. on p.\u00a03)."},{"volume-title":"Using the Internal Language of Toposes in Algebraic Geometry","year":"2017","author":"Blechschmidt","key":"S0960129524000239_ref1"},{"key":"S0960129524000239_ref3","unstructured":"Capriotti, P. , Kraus, N. and Vezzosi, A. (2015). Functions out of higher truncations. In: Kreutzer, S. (eds.) 24th EACSL Annual Conference on Computer Science Logic (CSL) 2015, Dagstuhl, Germany: Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 41, 359\u2013373, ISBN: 978-3- 939897-90-3. http:\/\/dx.doi.org\/10.4230\/LIPIcs.CSL.2015.359. URL: http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2015\/5425 (cit. on p. 5)."},{"key":"S0960129524000239_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"S0960129524000239_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-9944-7"},{"volume-title":"Lawvere-Tierney sheafification in Homotopy Type Theory. (Faisceautisation de Lawvere-Tierney en th\u00e9orie des types homotopiques)","year":"2016","author":"Quirin","key":"S0960129524000239_ref21"},{"key":"S0960129524000239_ref24","unstructured":"van den Berg, B. and Moerdijk, I. (2013). The Axiom of Multiple Choice and Models for Constructive Set Theory\u201d. Journal of Mathematical Logic. World Scientific. arXiv: 1204.4045 [math.LO] (cit. on p. 3)."},{"key":"S0960129524000239_ref4","unstructured":"Cherubini, F. and Hutzler, M. Synthetic geometry. URL: https:\/\/github.com\/felixwellen\/synthetic-geometry (cit. on p. 3)."},{"key":"S0960129524000239_ref13","unstructured":"Ingo, Blechschmidt , et al. (2023). Topology of synthetic schemes (preprint). URL: https:\/\/www.felix-cherubini.de\/topology.pdf (cit. on p. 27)."},{"key":"S0960129524000239_ref14","unstructured":"Kock, A. (2006). Synthetic differential geometry. London Mathematical Society Lecture Note Series, Cambridge University Press. URL: https:\/\/users-math.au.dk\/kock\/sdg99.pdf (cit. on pp. 1, 2, 6)."},{"key":"S0960129524000239_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3849-0"},{"key":"S0960129524000239_ref2","unstructured":"Blechschmidt, I. , Cherubini, F. and W\u00e4rn, D. (2023). \u010cech cohomology in homotopy type theory (unpublished preprint). URL: https:\/\/www.felix-cherubini.de\/cech.pdf (cit. on pp. 28, 31)."},{"key":"S0960129524000239_ref7","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000359"},{"key":"S0960129524000239_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3242953.3242962"},{"volume-title":"Continuity and effectiveness in topoi","year":"1986","author":"Rosolini","key":"S0960129524000239_ref22"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129524000239","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T11:35:11Z","timestamp":1739273711000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129524000239\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10]]},"references-count":24,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["S0960129524000239"],"URL":"https:\/\/doi.org\/10.1017\/s0960129524000239","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2024,10]]},"assertion":[{"value":"\u00a9 The Author(s), 2024. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}