<abstract xmlns="http://www.w3.org/1999/xhtml">

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 (<italic>Chapitre 0 Univers et Appendice “Univers” (par N. Bourbaki) de l’Exposé I. “PREFAISCE-AUX”</italic>) [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 <italic>ω</italic> (NAT), following the notion of Robert M. Solovay2. The following result links the universes <bold>U</bold>0 (FinSETS) and <bold>U</bold>1 (SETS):
<disp-formula>
<alternatives>
<graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0005_eq_001.png"></graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mrow><mtext>Grothendieck</mtext><mi> </mi><mtext>Universe</mtext><mi> </mi><mi>ω</mi><mo>=</mo><mtext>Grothendieck</mtext><mi> </mi><mtext>Universe</mtext><mi> </mi><msub><mrow><mstyle fontweight="bold" fontstyle="normal"><mi>U</mi></mstyle></mrow><mn>0</mn></msub><mo>=</mo><msub><mrow><mstyle fontweight="bold" fontstyle="normal"><mi>U</mi></mstyle></mrow><mn>1</mn></msub></mrow></math>
<tex-math>{\rm{Grothendieck}}\,{\rm{Universe}}\,\omega = {\rm{Grothendieck}}\,{\rm{Universe}}\,{{\bf{U}}_0} = {{\bf{U}}_1}</tex-math>
</alternatives>
</disp-formula>
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 theory in Context” [29], and more specifically “Strict Universes for Grothendieck Topoi” [14].
</abstract>

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. “PREFAISCE-AUX”) [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. Solovay2. The following result links the universes U0 (FinSETS) and U1 (SETS):



Grothendieck Universe ω=Grothendieck Universe U0=U1
{\rm{Grothendieck}}\,{\rm{Universe}}\,\omega = {\rm{Grothendieck}}\,{\rm{Universe}}\,{{\bf{U}}_0} = {{\bf{U}}_1}


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 theory in Context” [29], and more specifically “Strict Universes for Grothendieck Topoi” [14].

Non-Trivial Universes and Sequences of Universes

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"Non-Trivial Universes and Sequences of Universes"}

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,...

Non-Trivial Universes and Sequences of Universes

Online veröffentlicht: 21. Dez. 2022

Seitenbereich: 53 - 66

Akzeptiert: 30. Apr. 2022

DOI: https://doi.org/10.2478/forma-2022-0005

Schlüsselwörter
Tarski-Grothendieck set theory, Grothendieck universe, universe hierarchy

© 2022 Roland Coghetto, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Non-Trivial Universes and Sequences of Universes

Online veröffentlicht: 21. Dez. 2022

Seitenbereich: 53 - 66

Akzeptiert: 30. Apr. 2022

DOI: https://doi.org/10.2478/forma-2022-0005

SchlüsselwörterTarski-Grothendieck set theory, Grothendieck universe, universe hierarchy

© 2022 Roland Coghetto, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Schlüsselwörter
Tarski-Grothendieck set theory, Grothendieck universe, universe hierarchy