Grothendieck universe

In mathematics, a Grothendieck universe is a set U with the following properties:

A Grothendieck universe is meant to provide a set in which all of mathematics can be performed. (In fact, uncountable Grothendieck universes provide models of set theory with the natural ∈-relation, natural powerset operation etc.). Elements of a Grothendieck universe are sometimes called small sets. The idea of universes is due to Alexander Grothendieck, who used them as a way of avoiding proper classes in algebraic geometry.

The existence of a nontrivial Grothendieck universe goes beyond the usual axioms of Zermelo–Fraenkel set theory; in particular it would imply the existence of strongly inaccessible cardinals. Tarski–Grothendieck set theory is an axiomatic treatment of set theory, used in some automatic proof systems, in which every set belongs to a Grothendieck universe. The concept of a Grothendieck universe can also be defined in a topos.[1]

It is similarly easy to prove that any Grothendieck universe U contains:

In particular, it follows from the last axiom that if U is non-empty, it must contain all of its finite subsets and a subset of each finite cardinality. One can also prove immediately from the definitions that the intersection of any class of universes is a universe.

Other examples are more difficult to construct. Loosely speaking, this is because Grothendieck universes are equivalent to strongly inaccessible cardinals. More formally, the following two axioms are equivalent:

(C) For each cardinal κ, there is a strongly inaccessible cardinal λ that is strictly larger than κ.

Let κ be a strongly inaccessible cardinal. Say that a set S is strictly of type κ if for any sequence sn ∈ ... ∈ s0S, |sn| < κ. (S itself corresponds to the empty sequence.) Then the set u(κ) of all sets strictly of type κ is a Grothendieck universe of cardinality κ. The proof of this fact is long, so for details, we again refer to Bourbaki's article, listed in the references.

In fact, any Grothendieck universe is of the form u(κ) for some κ. This gives another form of the equivalence between Grothendieck universes and strongly inaccessible cardinals: