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.
Révisé le :
Accepté le :
Publié le :
@article{CML_2015__7_1_55_0, author = {Rinaldi, Davide and Sambin, Giovanni and Schuster, Peter}, title = {The {Basic} {Zariski} {Topology}}, journal = {Confluentes Mathematici}, pages = {55--81}, publisher = {Institut Camille Jordan}, volume = {7}, number = {1}, year = {2015}, doi = {10.5802/cml.18}, language = {en}, url = {http://www.numdam.org/articles/10.5802/cml.18/} }
TY - JOUR AU - Rinaldi, Davide AU - Sambin, Giovanni AU - Schuster, Peter TI - The Basic Zariski Topology JO - Confluentes Mathematici PY - 2015 SP - 55 EP - 81 VL - 7 IS - 1 PB - Institut Camille Jordan UR - http://www.numdam.org/articles/10.5802/cml.18/ DO - 10.5802/cml.18 LA - en ID - CML_2015__7_1_55_0 ER -
Rinaldi, Davide; Sambin, Giovanni; Schuster, Peter. The Basic Zariski Topology. Confluentes Mathematici, Tome 7 (2015) no. 1, pp. 55-81. doi : 10.5802/cml.18. http://www.numdam.org/articles/10.5802/cml.18/
[1] Notes on Constructive Set Theory, Available from Aczel’s webpage, 2008
[2] The power of the ultrafilter theorem, Journal of the London Mathematical Society, Volume 27 (1983), pp. 193-202
[3] Convergence in formal topology: a unifying notion, Journal of Logic and Analysis, Volume 5 (2013) no. 2, pp. 1-45
[4] Finitary formal topologies and Stone’s representation theorem, Theoretical Computer Science, Volume 405 (2008) no. 1-2, pp. 11-23 | DOI
[5] Reducibility, a constructive dual of spatiality, Preprint, Università di Padova (2015)
[6] Space of valuations, Annals of Pure and Applied Logic, Volume 157 (2009), pp. 97-109
[7] A logical approach to abstract algebra., Mathematical Structures in Computer Science, Volume 16 (2006), pp. 885-900
[8] 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] Valuations and Dedekind’s Prague theorem, Journal of Pure and Applied Algebra, Volume 155 (2001), pp. 121-129
[10] Inductively generated formal topologies, Annals of Pure and Applied Logic, Volume 124 (2003), pp. 71-106
[11] Axiom of choice and complementation, Proceedings of the American Mathematical Society, Volume 51 (1975), pp. 176-178
[12] Spatiality for formal topologies., Mathematical Structures in Computer Science, Volume 17 (2007) no. 1, pp. 65-80
[13] Choice implies excluded middle, Mathematical Logic Quarterly, Volume 24 (1978) no. 25-30, p. 461-461 | DOI
[14] Stone Spaces., Cambridge Studies in Advanced Mathematics, Cambridge etc.: Cambridge University Press, 1982 no. 3
[15] 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] Spectral spaces and distributive lattices, Notices of the American Mathematical Society, Volume 18 (1971), 393 pages
[17] 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] Algèbre dynamique, espaces topologiques sans points et programme de Hilbert., Annals of Pure and Applied Logic, Volume 137 (2006), pp. 256-290
[19] Algèbre Commutative, Méthodes constructives, Modules projectifs de type fini., Calvage & Mounet, Paris, 2012
[20] Intuitionistic Type Theory, Notes by Giovanni Sambin of a series of lectures given in Padua, Bibliopolis, Napoli, 1984
[21] Generating positivity by coinduction, The Basic Picture and Positive Topology. New structures for constructive mathematics (Oxford Logic Guides), Clarendon Press, Oxford (forthcoming)
[22] Continuous domains as formal spaces, Mathematical Structures in Computer Science, Volume 12 (2002), pp. 19-52
[23] A constructive notion of codimension, Journal of Algebra, Volume 383 (2013), pp. 178-196 http://www.sciencedirect.com/science/article/pii/S0021869313001257 | DOI
[24] Quantales and their applications, Pitman Research Notes in Mathematics Series, 234, Longman Scientific & Technical, Harlow; copublished in the United States with John Wiley & Sons, Inc., New York, 1990
[25] Intuitionistic formal spaces - a first communication, Mathematical Logic and its Applications (Skordev, D., ed.), Plenum, 1987, pp. 187-204
[26] Some points in formal topology, Theoretical Computer Science, Volume 305 (2003) no. 1-3, pp. 347-408
[27] The Basic Picture and Positive Topology. New structures for constructive mathematics, Oxford Logic Guides, Clarendon Press, Oxford, forthcoming
[28] 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] 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), Springer-Verlag, London, UK (1999), pp. 194-207 http://dl.acm.org/citation.cfm?id=646538.696020
[30] Formal Zariski topology: positivity and points, Annals of Pure and Applied Logic, Volume 137 (2006) no. 1-3, pp. 317-359
[31] The Zariski spectrum as a formal geometry, Theoretical Computer Science, Volume 405 (2008), pp. 101-115
[32] Induction in algebra: a first case study, Logical Methods in Computer Science, Volume 9 (2013) no. 3, 20 pages
[33] Formal spaces and their effective presentations, Archive for Mathematical Logic, Volume 34 (1995) no. 4, pp. 211-246
[34] 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] Topology via logic, Cambridge Tracts in Theoretical Computer Science, 5, Cambridge University Press, Cambridge, 1989
Cité par Sources :