The Basic Zariski Topology
Confluentes Mathematici, Tome 7 (2015) no. 1, pp. 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.

Reçu le : 2014-05-11
Révisé le : 2015-07-15
Accepté le : 2015-07-15
Publié le : 2016-02-03
DOI : https://doi.org/10.5802/cml.18
Classification : 03E25,  03F65,  13A99,  54B35
@article{CML_2015__7_1_55_0,
     author = {Davide Rinaldi and Giovanni Sambin and Peter Schuster},
     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 = {cml.centre-mersenne.org/item/CML_2015__7_1_55_0/}
}
Davide Rinaldi; Giovanni Sambin; Peter Schuster. The Basic Zariski Topology. Confluentes Mathematici, Tome 7 (2015) no. 1, pp. 55-81. doi : 10.5802/cml.18. https://cml.centre-mersenne.org/item/CML_2015__7_1_55_0/

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

[2] Bernhard Banaschewski The power of the ultrafilter theorem, Journal of the London Mathematical Society, Volume 27 (1983), pp. 193-202

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

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

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

[6] Thierry Coquand Space of valuations, Annals of Pure and Applied Logic, Volume 157 (2009), pp. 97-109

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

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

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

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

[11] Radu Diaconescu Axiom of choice and complementation, Proceedings of the American Mathematical Society, Volume 51 (1975), pp. 176-178

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

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

[14] Peter T. Johnstone Stone Spaces., Cambridge Studies in Advanced Mathematics, Cambridge etc.: Cambridge University Press, 1982 no. 3

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

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

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

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

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

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

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

[22] Sara Negri Continuous domains as formal spaces, Mathematical Structures in Computer Science, Volume 12 (2002), pp. 19-52

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

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

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

[26] Giovanni Sambin Some points in formal topology, Theoretical Computer Science, Volume 305 (2003) no. 1-3, pp. 347-408

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

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

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

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

[31] Peter Schuster The Zariski spectrum as a formal geometry, Theoretical Computer Science, Volume 405 (2008), pp. 101-115

[32] Peter Schuster Induction in algebra: a first case study, Logical Methods in Computer Science, Volume 9 (2013) no. 3, 20 pages

[33] Inger Sigstam Formal spaces and their effective presentations, Archive for Mathematical Logic, Volume 34 (1995) no. 4, pp. 211-246

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

[35] Steven Vickers Topology via logic, Cambridge Tracts in Theoretical Computer Science, Volume 5, Cambridge University Press, Cambridge, 1989