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.
@article{CML_2015__7_1_55_0,
author = {Rinaldi, Davide and Sambin, Giovanni and Schuster, Peter},
title = {The Basic Zariski Topology},
journal = {Confluentes Mathematici},
volume = {7},
year = {2015},
pages = {55-81},
doi = {10.5802/cml.18},
language = {en},
url = {http://dml.mathdoc.fr/item/CML_2015__7_1_55_0}
}
Rinaldi, Davide; Sambin, Giovanni; Schuster, Peter. The Basic Zariski Topology. Confluentes Mathematici, Tome 7 (2015) pp. 55-81. doi : 10.5802/cml.18. http://gdmltest.u-ga.fr/item/CML_2015__7_1_55_0/
[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, Tome 27 (1983), pp. 193-202 | MR 692524 | Zbl 0523.03037
[3] 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] 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] Reducibility, a constructive dual of spatiality, Preprint, Università di Padova (2015)
[6] Space of valuations, Annals of Pure and Applied Logic, Tome 157 (2009), pp. 97-109 | MR 2499701 | Zbl 1222.03072
[7] A logical approach to abstract algebra., Mathematical Structures in Computer Science, Tome 16 (2006), pp. 885-900 | MR 2268347 | Zbl 1118.03059
[8] 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] Valuations and Dedekind’s Prague theorem, Journal of Pure and Applied Algebra, Tome 155 (2001), pp. 121-129 | MR 1801410 | Zbl 0983.11061
[10] Inductively generated formal topologies, Annals of Pure and Applied Logic, Tome 124 (2003), pp. 71-106 | MR 2013394 | Zbl 1070.03041
[11] Axiom of choice and complementation, Proceedings of the American Mathematical Society, Tome 51 (1975), pp. 176-178 | MR 373893 | Zbl 0317.02077
[12] Spatiality for formal topologies., Mathematical Structures in Computer Science, Tome 17 (2007) no. 1, pp. 65-80 | MR 2311086 | Zbl 1139.03045
[13] Choice implies excluded middle, Mathematical Logic Quarterly, Tome 24 (1978) no. 25-30, p. 461-461 | Article | MR 509798 | Zbl 0387.03017
[14] Stone Spaces., Cambridge etc.: Cambridge University Press, Cambridge Studies in Advanced Mathematics (1982) no. 3 | MR 698074 | Zbl 0499.54001
[15] 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] Spectral spaces and distributive lattices, Notices of the American Mathematical Society, Tome 18 (1971), pp. 393
[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, Tome 16 (1976), pp. 256-258 | Zbl 0354.02038
[18] 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] 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) | MR 769301
[21] 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] Continuous domains as formal spaces, Mathematical Structures in Computer Science, Tome 12 (2002), pp. 19-52 | MR 1887335 | Zbl 0994.06005
[23] 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] 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] Intuitionistic formal spaces - a first communication, Mathematical Logic and its Applications, Plenum (1987), pp. 187-204 | MR 945195 | Zbl 0703.03040
[26] Some points in formal topology, Theoretical Computer Science, Tome 305 (2003) no. 1-3, pp. 347-408 | MR 2013578 | Zbl 1044.54001
[27] The Basic Picture and Positive Topology. New structures for constructive mathematics, Clarendon Press, Oxford, Oxford Logic Guides (forthcoming) | MR 1686856
[28] 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] 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] 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] The Zariski spectrum as a formal geometry, Theoretical Computer Science, Tome 405 (2008), pp. 101-115 | MR 2454496 | Zbl 1154.03038
[32] 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] Formal spaces and their effective presentations, Archive for Mathematical Logic, Tome 34 (1995) no. 4, pp. 211-246 | MR 1356538 | Zbl 0829.03026
[34] 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] Topology via logic, Cambridge University Press, Cambridge, Cambridge Tracts in Theoretical Computer Science, Tome 5 (1989) | MR 1002193 | Zbl 0668.54001