The Basic Zariski Topology
Confluentes Mathematici, Volume 7 (2015) no. 1, p. 55-81

We present the Zariski spectrum as an inductively generated basic topology à la Martin-Löf and Sambin. Since we can thus get by without considering powers and radicals, this simplifies the presentation as a formal topology initiated by Sigstam. Our treatment includes closed subspaces and basic opens: that is, arbitrary quotients and singleton localisations. All the effective objects under consideration are introduced by means of inductive definitions. The notions of spatiality and reducibility are characterized for the class of Zariski formal topologies, and their nonconstructive content is pointed out: while spatiality implies classical logic, reducibility corresponds to a fragment of the Axiom of Choice in the form of Russell’s Multiplicative Axiom.

DOI : https://doi.org/10.5802/cml.18
Classification:  03E25,  03F65,  13A99,  54B35
@article{CML_2015__7_1_55_0,
     author = {Rinaldi, Davide and Sambin, Giovanni and Schuster, Peter},
     title = {The Basic Zariski Topology},
     journal = {Confluentes Mathematici},
     publisher = {Institut Camille Jordan},
     volume = {7},
     number = {1},
     year = {2015},
     pages = {55-81},
     doi = {10.5802/cml.18},
     language = {en},
     url = {http://www.numdam.org/item/CML_2015__7_1_55_0}
}
Rinaldi, Davide; Sambin, Giovanni; Schuster, Peter. The Basic Zariski Topology. Confluentes Mathematici, Volume 7 (2015) no. 1, pp. 55-81. doi : 10.5802/cml.18. http://www.numdam.org/item/CML_2015__7_1_55_0/

[1] Aczel, Peter; Rathjen, Michael Notes on Constructive Set Theory, Available from Aczel’s webpage (2008)

[2] Banaschewski, Bernhard The power of the ultrafilter theorem, Journal of the London Mathematical Society, Tome 27 (1983), pp. 193-202 | MR 692524 | Zbl 0523.03037

[3] Ciraulo, Francesco; Maietti, Maria Emilia; Sambin, Giovanni Convergence in formal topology: a unifying notion, Journal of Logic and Analysis, Tome 5 (2013) no. 2, pp. 1-45 | MR 3033505 | Zbl 1280.54003

[4] Ciraulo, Francesco; Sambin, Giovanni Finitary formal topologies and Stone’s representation theorem, Theoretical Computer Science, Tome 405 (2008) no. 1-2, pp. 11-23 | Article | MR 2454487 | Zbl 1187.54010

[5] Ciraulo, Francesco; Sambin, Giovanni Reducibility, a constructive dual of spatiality, Preprint, Università di Padova (2015)

[6] Coquand, Thierry Space of valuations, Annals of Pure and Applied Logic, Tome 157 (2009), pp. 97-109 | MR 2499701 | Zbl 1222.03072

[7] Coquand, Thierry; Lombardi, Henri A logical approach to abstract algebra., Mathematical Structures in Computer Science, Tome 16 (2006), pp. 885-900 | MR 2268347 | Zbl 1118.03059

[8] Coquand, Thierry; Lombardi, Henri; Schuster, Peter The projective spectrum as a distributive lattice, Cahiers de Topologie et Géométrie Différentielle Catégoriques, Tome 48 (2007), pp. 220-228 | Numdam | MR 2351269 | Zbl 1131.03035

[9] Coquand, Thierry; Persson, Henrik Valuations and Dedekind’s Prague theorem, Journal of Pure and Applied Algebra, Tome 155 (2001), pp. 121-129 | MR 1801410 | Zbl 0983.11061

[10] Coquand, Thierry; Sambin, Giovanni; Smith, J.; Valentini, Silvio Inductively generated formal topologies, Annals of Pure and Applied Logic, Tome 124 (2003), pp. 71-106 | MR 2013394 | Zbl 1070.03041

[11] Diaconescu, Radu Axiom of choice and complementation, Proceedings of the American Mathematical Society, Tome 51 (1975), pp. 176-178 | MR 373893 | Zbl 0317.02077

[12] Gambino, Nicola; Schuster, Peter Spatiality for formal topologies., Mathematical Structures in Computer Science, Tome 17 (2007) no. 1, pp. 65-80 | MR 2311086 | Zbl 1139.03045

[13] Goodman, N.; Myhill, J. Choice implies excluded middle, Mathematical Logic Quarterly, Tome 24 (1978) no. 25-30, p. 461-461 | Article | MR 509798 | Zbl 0387.03017

[14] Johnstone, Peter T. Stone Spaces., Cambridge etc.: Cambridge University Press, Cambridge Studies in Advanced Mathematics (1982) no. 3 | MR 698074 | Zbl 0499.54001

[15] Johnstone, Peter T. Sketches of an Elephant: A Topos Theory Compendium, Oxford University Press, Oxford Logic Guides (2002) no. 43-44 http://books.google.de/books?id=9oIZwBQbjiwC | Zbl 1071.18001

[16] Joyal, André Spectral spaces and distributive lattices, Notices of the American Mathematical Society, Tome 18 (1971), pp. 393

[17] Joyal, André Les théoremes de Chevalley-Tarski et remarques sur l’algèbre constructive, Cahiers de Topologie et Géométrie Différentielle Catégoriques, Tome 16 (1976), pp. 256-258 | Zbl 0354.02038

[18] Lombardi, Henri Algèbre dynamique, espaces topologiques sans points et programme de Hilbert., Annals of Pure and Applied Logic, Tome 137 (2006), pp. 256-290 | MR 2182105 | Zbl 1077.03039

[19] Lombardi, Henri; Quitté, Claude Algèbre Commutative, Méthodes constructives, Modules projectifs de type fini., Calvage & Mounet, Paris (2012)

[20] Martin-Löf, Per Intuitionistic Type Theory, Notes by Giovanni Sambin of a series of lectures given in Padua, Bibliopolis, Napoli (1984) | MR 769301

[21] Martin-Löf, Per; Sambin, Giovanni Generating positivity by coinduction, The Basic Picture and Positive Topology. New structures for constructive mathematics, Clarendon Press, Oxford (Oxford Logic Guides) (forthcoming) | MR 1686856

[22] Negri, Sara Continuous domains as formal spaces, Mathematical Structures in Computer Science, Tome 12 (2002), pp. 19-52 | MR 1887335 | Zbl 0994.06005

[23] Rinaldi, Davide A constructive notion of codimension, Journal of Algebra, Tome 383 (2013), pp. 178-196 http://www.sciencedirect.com/science/article/pii/S0021869313001257 | Article | MR 3037974 | Zbl 1291.13015

[24] Rosenthal, Kimmo I. Quantales and their applications, Longman Scientific & Technical, Harlow; copublished in the United States with John Wiley & Sons, Inc., New York, Pitman Research Notes in Mathematics Series, Tome 234 (1990) | MR 1088258 | Zbl 0703.06007

[25] Sambin, G.; Skordev, D. Intuitionistic formal spaces - a first communication, Mathematical Logic and its Applications, Plenum (1987), pp. 187-204 | MR 945195 | Zbl 0703.03040

[26] Sambin, Giovanni Some points in formal topology, Theoretical Computer Science, Tome 305 (2003) no. 1-3, pp. 347-408 | MR 2013578 | Zbl 1044.54001

[27] Sambin, Giovanni The Basic Picture and Positive Topology. New structures for constructive mathematics, Clarendon Press, Oxford, Oxford Logic Guides (forthcoming) | MR 1686856

[28] Sambin, Giovanni; Battilotti, Giulia Pretopologies and a uniform presentation of sup-lattices, quantales and frames, Annals of Pure and Applied Logic, Tome 137 (2006) no. 1-3, pp. 30-61 | MR 2182097 | Zbl 1077.03036

[29] Sambin, Giovanni; Gebellato, Silvia A preview of the basic picture: a new perspective on formal topology, Selected papers from the International Workshop on Types for Proofs and Programs, Springer-Verlag, London, UK (TYPES ’98) (1999), pp. 194-207 http://dl.acm.org/citation.cfm?id=646538.696020 | MR 1853605 | Zbl 0953.03069

[30] Schuster, Peter Formal Zariski topology: positivity and points, Annals of Pure and Applied Logic, Tome 137 (2006) no. 1-3, pp. 317-359 | MR 2182108 | Zbl 1088.03050

[31] Schuster, Peter The Zariski spectrum as a formal geometry, Theoretical Computer Science, Tome 405 (2008), pp. 101-115 | MR 2454496 | Zbl 1154.03038

[32] Schuster, Peter Induction in algebra: a first case study, Logical Methods in Computer Science, Tome 9 (2013) no. 3, pp. 20 | MR 3109604 | Zbl 1277.03065

[33] Sigstam, Inger Formal spaces and their effective presentations, Archive for Mathematical Logic, Tome 34 (1995) no. 4, pp. 211-246 | MR 1356538 | Zbl 0829.03026

[34] Stone, Marshall Harvey Topological representations of distributive lattices and Brouwerian logics, Časopis pro pěstování matematiky a fysiky, Tome 67 (1938) no. 1, pp. 1-25 | Zbl 0018.00303

[35] Vickers, Steven Topology via logic, Cambridge University Press, Cambridge, Cambridge Tracts in Theoretical Computer Science, Tome 5 (1989) | MR 1002193 | Zbl 0668.54001