Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/14247
Tytuł: | Non-Trivial Universes and Sequences of Universes |
Autorzy: | Coghetto, Roland |
Słowa kluczowe: | Tarski-Grothendieck set theory Grothendieck universe universe hierarchy |
Data wydania: | 2022 |
Data dodania: | 29-gru-2022 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 30, Issue 1, Pages 53-66 |
Abstrakt: | Universe is a concept which is present from the beginning of the creation of the Mizar Mathematical Library (MML) in several forms (Universe, Universe_closure, UNIVERSE) [25], then later as the_universe_of, [33], and recently with the definition GrothendieckUniverse [26], [11], [11]. These definitions are useful in many articles [28, 33, 8, 35], [19, 32, 31, 15, 6], but also [34, 12, 20, 22, 21], [27, 2, 3, 23, 16, 7, 4, 5]. In this paper, using the Mizar system [9] [10], we trivially show that Grothendieck’s definition of Universe as defined in [26], coincides with the original definition of Universe defined by Artin, Grothendieck, and Verdier (Chapitre 0 Univers et Appendice “Univers” (par N. Bourbaki) de l’Exposé I. “PREFAISCEAUX”) [1], and how the different definitions of MML concerning universes are related. We also show that the definition of Universe introduced by Mac Lane ([18]) is compatible with the MML’s definition. Although a universe may be empty, we consider the properties of non-empty universes, completing the properties proved in [25]. We introduce the notion of “trivial” and “non-trivial” Universes, depending on whether or not they contain the set ω (NAT), following the notion of Robert M. Solovay. The following result links the universes U₀ (FinSETS) and U₁ (SETS): GrothendieckUniverse ω = GrothendieckUniverse U₀ = U₁ . Before turning to the last section, we establish some trivial propositions allowing the construction of sets outside the considered universe. The last section is devoted to the construction, in Tarski-Grothendieck, of a tower of universes indexed by the ordinal numbers (See 8. Examples, Grothendieck universe, ncatlab.org [24]). Grothendieck’s universe is referenced in current works: “Assuming the existence of a sufficient supply of (Grothendieck) univers”, Jacob Lurie in “Higher Topos Theory” [17], “Annexe B – Some results on Grothendieck universes”, Olivia Caramello and Riccardo Zanfa in “Relative topos theory via stacks” [13], “Remark 1.1.5 (quoting Michael Shulman [30])”, Emily Riehl in “Category the ory in Context” [29], and more specifically “Strict Universes for Grothendieck Topoi” [14]. |
Afiliacja: | Roland Coghetto - cafr-MSA2P asbl, Rue de la Brasserie 5, 7100 La Louvi`ere, Belgium |
URI: | http://hdl.handle.net/11320/14247 |
DOI: | 10.2478/forma-2022-0005 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | 0000-0002-4901-0766 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | https://creativecommons.org/licenses/by-sa/3.0/ |
Właściciel praw: | © 2022 The Author(s) CC BY-SA 3.0 license |
Występuje w kolekcji(ach): | Formalized Mathematics, 2022, Volume 30, Issue 1 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
10.2478_forma-2022-0005.pdf | 306,04 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL