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 :
Révisé le :
Accepté le :
Publié le :
DOI : 10.5802/cml.18
Classification : 03E25, 03F65, 13A99, 54B35
Rinaldi, Davide 1 ; Sambin, Giovanni 2 ; Schuster, Peter 3

1 Department of Pure Mathematics, University of Leeds, Leeds LS2 9JT, England
2 Dipartimento di Matematica, Università di Padova, Via Trieste 63, 35121 Padova, Italy
3 Dipartimento di Informatica, Università di Verona, Strada le Grazie 15, 37134 Verona, Italy
@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  - 
%0 Journal Article
%A Rinaldi, Davide
%A Sambin, Giovanni
%A Schuster, Peter
%T The Basic Zariski Topology
%J Confluentes Mathematici
%D 2015
%P 55-81
%V 7
%N 1
%I Institut Camille Jordan
%U http://www.numdam.org/articles/10.5802/cml.18/
%R 10.5802/cml.18
%G en
%F CML_2015__7_1_55_0
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] 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, Volume 27 (1983), pp. 193-202

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

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

[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, Volume 157 (2009), pp. 97-109

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

[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, Volume 48 (2007), pp. 220-228

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

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

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

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

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

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

[15] Johnstone, Peter T. 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] Joyal, André Spectral spaces and distributive lattices, Notices of the American Mathematical Society, Volume 18 (1971), 393 pages

[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, Volume 16 (1976), pp. 256-258

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

[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

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

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

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

[24] Rosenthal, Kimmo I. 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] Sambin, G. Intuitionistic formal spaces - a first communication, Mathematical Logic and its Applications (Skordev, D., ed.), Plenum, 1987, pp. 187-204

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

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

[28] Sambin, Giovanni; Battilotti, Giulia 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] 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 (TYPES ’98), Springer-Verlag, London, UK (1999), pp. 194-207 http://dl.acm.org/citation.cfm?id=646538.696020

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

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

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

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

[34] Stone, Marshall Harvey 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] Vickers, Steven Topology via logic, Cambridge Tracts in Theoretical Computer Science, 5, Cambridge University Press, Cambridge, 1989

Cité par Sources :