Avec cedram.org
Confluentes Mathematici
Rechercher un article
Recherche sur le site
Table des matières de ce fascicule | Article précédent | Article suivant
Davide Rinaldi; Giovanni Sambin; Peter Schuster
The Basic Zariski Topology
Confluentes Mathematici, 7 no. 1 (2015), p. 55-81, doi: 10.5802/cml.18
Article PDF
Class. Math.: 03E25, 03F65, 13A99, 54B35

Résumé - Abstract

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.

Bibliographie

[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 27 (1983), p. 193-202  MR 692524 |  Zbl 0523.03037
[3] Francesco Ciraulo, Maria Emilia Maietti & Giovanni Sambin, “Convergence in formal topology: a unifying notion”, Journal of Logic and Analysis 5 (2013) no. 2, p. 1-45  MR 3033505 |  Zbl 1280.54003
[4] Francesco Ciraulo & Giovanni Sambin, “Finitary formal topologies and Stone’s representation theorem”, Theoretical Computer Science 405 (2008) no. 1-2, p. 11-23 Article |  MR 2454487 |  Zbl 1187.54010
[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 157 (2009), p. 97-109  MR 2499701 |  Zbl 1222.03072
[7] Thierry Coquand & Henri Lombardi, “A logical approach to abstract algebra.”, Mathematical Structures in Computer Science 16 (2006), p. 885-900  MR 2268347 |  Zbl 1118.03059
[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 48 (2007), p. 220-228 Numdam |  MR 2351269 |  Zbl 1131.03035
[9] Thierry Coquand & Henrik Persson, “Valuations and Dedekind’s Prague theorem”, Journal of Pure and Applied Algebra 155 (2001), p. 121-129  MR 1801410 |  Zbl 0983.11061
[10] Thierry Coquand, Giovanni Sambin, J. Smith & Silvio Valentini, “Inductively generated formal topologies”, Annals of Pure and Applied Logic 124 (2003), p. 71-106  MR 2013394 |  Zbl 1070.03041
[11] Radu Diaconescu, “Axiom of choice and complementation”, Proceedings of the American Mathematical Society 51 (1975), p. 176-178  MR 373893 |  Zbl 0317.02077
[12] Nicola Gambino & Peter Schuster, “Spatiality for formal topologies.”, Mathematical Structures in Computer Science 17 (2007) no. 1, p. 65-80  MR 2311086 |  Zbl 1139.03045
[13] N. Goodman & J. Myhill, “Choice implies excluded middle”, Mathematical Logic Quarterly 24 (1978) no. 25-30, p. 461-461 Article |  MR 509798 |  Zbl 0387.03017
[14] Peter T. Johnstone, Stone Spaces., Cambridge Studies in Advanced Mathematics, Cambridge etc.: Cambridge University Press, 1982  MR 698074 |  Zbl 0499.54001
[15] Peter T. Johnstone, Sketches of an Elephant: A Topos Theory Compendium, Oxford Logic Guides, Oxford University Press, 2002  Zbl 1071.18001
[16] André Joyal, “Spectral spaces and distributive lattices”, Notices of the American Mathematical Society 18 (1971)
[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 16 (1976), p. 256-258  Zbl 0354.02038
[18] Henri Lombardi, “Algèbre dynamique, espaces topologiques sans points et programme de Hilbert.”, Annals of Pure and Applied Logic 137 (2006), p. 256-290  MR 2182105 |  Zbl 1077.03039
[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  MR 769301
[21] Per Martin-Löf & Giovanni Sambin, Generating positivity by coinduction, in The Basic Picture and Positive Topology. New structures for constructive mathematics, Oxford Logic Guides, Clarendon Press, forthcoming  MR 1686856
[22] Sara Negri, “Continuous domains as formal spaces”, Mathematical Structures in Computer Science 12 (2002), p. 19-52  MR 1887335 |  Zbl 0994.06005
[23] Davide Rinaldi, “A constructive notion of codimension”, Journal of Algebra 383 (2013), p. 178-196 Article |  MR 3037974 |  Zbl 1291.13015
[24] Kimmo I. Rosenthal, 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  MR 1088258 |  Zbl 0703.06007
[25] G. Sambin, Intuitionistic formal spaces - a first communication, in D. Skordev, éd., Mathematical Logic and its Applications, Plenum, 1987, p. 187-204  MR 945195 |  Zbl 0703.03040
[26] Giovanni Sambin, “Some points in formal topology”, Theoretical Computer Science 305 (2003) no. 1-3, p. 347-408  MR 2013578 |  Zbl 1044.54001
[27] Giovanni Sambin, The Basic Picture and Positive Topology. New structures for constructive mathematics, Oxford Logic Guides, Clarendon Press, Oxford, forthcoming  MR 1686856
[28] Giovanni Sambin & Giulia Battilotti, “Pretopologies and a uniform presentation of sup-lattices, quantales and frames”, Annals of Pure and Applied Logic 137 (2006) no. 1-3, p. 30-61  MR 2182097 |  Zbl 1077.03036
[29] Giovanni Sambin & Silvia Gebellato, A preview of the basic picture: a new perspective on formal topology, in Selected papers from the International Workshop on Types for Proofs and Programs, TYPES ’98, Springer-Verlag, 1999, p. 194-207  MR 1853605 |  Zbl 0953.03069
[30] Peter Schuster, “Formal Zariski topology: positivity and points”, Annals of Pure and Applied Logic 137 (2006) no. 1-3, p. 317-359  MR 2182108 |  Zbl 1088.03050
[31] Peter Schuster, “The Zariski spectrum as a formal geometry”, Theoretical Computer Science 405 (2008), p. 101-115  MR 2454496 |  Zbl 1154.03038
[32] Peter Schuster, “Induction in algebra: a first case study”, Logical Methods in Computer Science 9 (2013) no. 3  MR 3109604 |  Zbl 1277.03065
[33] Inger Sigstam, “Formal spaces and their effective presentations”, Archive for Mathematical Logic 34 (1995) no. 4, p. 211-246  MR 1356538 |  Zbl 0829.03026
[34] Marshall Harvey Stone, “Topological representations of distributive lattices and Brouwerian logics”, Časopis pro pěstování matematiky a fysiky 67 (1938) no. 1, p. 1-25  Zbl 0018.00303 |  JFM 63.0830.01
[35] Steven Vickers, Topology via logic, Cambridge Tracts in Theoretical Computer Science 5, Cambridge University Press, Cambridge, 1989  MR 1002193 |  Zbl 0668.54001
eISSN : 1793-7434

haut