1.1 Grothendieck Universe
Definition 1.1.1 (Pure Set).label A set $x$ is pure if given any finite sequence $x_{n}\in x_{n-1}\in\cds\in x_{1}\in x_{0}=x$, all of $x_{i}$ are sets.
Definition 1.1.2 (Well-Founded).label A class $C$ of sets is $\in$-inductive if whenever all elements of some set $x$ are in $C$, then $x\in C$. A set $x$ is well-founded if it belongs to every $\in$-inductive class $C$.
Definition 1.1.3 (Grothendieck Universe).label A Grothendieck universe is a pure set $U$ such that:
- (GU1)
$\fall u\in U,t\in u,t\in U$
- (GU2)
$\fall u\in U,\cali{P}(u)\in U$
- (GU3)
$\emp\in U$
- (GU4)
$\fall I\in U$ and functions $u:I\to U,\cups{}{i\in I }u_{i}\in U$
An element of $U$ is called a $U$-small set, while a subset of $U$ is called $U$-moderate. Every $U$-small set is $U$-moderate by (GU1).
Lemma 1.1.4 (Closure Properties of Grothendieck Universe).label Let $U$ be a Grothendieck universe, $u,v\in U$ and $t\suf u$ is a subset then $t,u\cup v\in U$.
Proof. By (GU2) $\cali{P}(u)\in U$ so by (GU1) $t\in U$. By (GU3) $\emp\in U$ so by (GU2) $\cali{P}(\emp),\cali{P}(\cali{P}(\emp))\in U$. Then $2=\curl{\bot,\top}\suf \cali{P}(\cali{P}(\emp))$ so $2\in U$. Define a function $f:2\to U$ by $f(\bot)=u$ and $f(\top)=v$. By (GU4) $u\cup v\in U$.$\square$
Remark 1.1.5 ([Observation after Lemma 3.2., nLa26]).label Then using the usual encodings in set theory:
The nullary cartesian product $\star$ is $\cali{P}(\emp)$
The binary cartesian product $u\ti v$ is a subset of $\cali{P}(\cali{P}(u\cup v))$
The general cartesian product $\prods{}{i\in I}u_{i}$ is a subset of $\cali{P}\parens{I\ti \cups{}{i\in I }u_i}$
The nullary disjoint union is $\emp$
The binary disjoint union $u\sqcup v$ is a subset of $2\ti (u\cup v)$
The general disjoint union $\dcups{}{i\in I}u_{i}$ is a subset of $I\ti \cups{}{i\in I}u_{i}$
The set of functions $u\to v$ is a subset of $\cali{P}(u\ti v)$
Post a Comment