Mac Lane本のユニバースの定義には、「いくらか冗長な」という表記がある。
例えば、性質(v)は冗長... というか少なくとも、より小さな仮定から導くことができる。これを見てみよう。
その前に、Grothendieck universe - Wikipedia, the free encyclopediaを見る。
性質として、以下が挙げられている。
(vi)$\{x_\alpha\}_{\alpha \in I}$ を $U$ の元の族とする時、 $I \in U$ であれば $\bigcup_{\alpha \in I} x_\alpha \in U$ である。
また、同ページ内のPropositionを見る。
Proposition
$x \in U$ かつ $y \subset x$ であれば、 $y \in U$ である。
Proof.
$y \subset x$ より、$y \in \mathcal{P}(x)$ である。*1
$x \in U$ であったので、性質(iii)の前半より $\mathcal{P}(x) \in U$ である。
よって、 $y \in \mathcal{P}(x) \in U$ であるので、性質(i)より $y \in U$ である。${}_\blacksquare$
この命題の系として性質(v)が得られることを見る。
まず、性質(ii)において $u = v$ とおくことで、 $u \in U \Rightarrow \{u\} \in U$ となることに注意する。
Cor1
性質(i)(ii)(iii)の前半(iv)(vi)のもと、 $f: a \to b$ が全射的関数で $a \in U$ かつ $b \subset U$ ならば $b \in U$ である。
Proof.
$\tilde{a} = f(a)$ とおくと仮定より $b = \tilde{a}$ である。特に、 $b \subset \tilde{a}$ である。よって、 $\tilde{a} \in U$ を示せば前述のPropositionより $b \in U$ が従う。
また、仮定より $b \subset U$ なので、 $\tilde{a} \subset U$ となる。従って、任意の $x \in a$ に対して、$f(x) \in U$ となるので、 $\{f(x)\} \in U$ を得る。 $\tilde{a} = f(a) = \bigcup_{x \in a} \{ f(x) \}$ と書けるが、仮定より $a \in U$ であったので、(vi)より $\tilde{a} \in U$ を得る。${}_\blacksquare$
更に、性質(iii)の前半、即ち
(iii')$x \in U$ ならば $\mathcal{P}(x) \in U$
を考えると、
Cor2
性質(i)(ii)(iii')(iv)(vi)のもと、 $x \in U$ ならば $\bigcup x \in U$ である。
を得る。よって、性質(iii)も小さな仮定に置き換えられる。要するに、(iii)+(v)は(iii')+(vi)から導くことができる。
Proof of Cor2.
(i)と(iii')より、$x$ の任意の部分集合 $y$ は $y \in \mathcal{P}(x) \in U$ であるので、 $y \in U$ である。
$\mathcal{P}(x) =: I = \{ y \}_{y \in \mathcal{P}(x)}$ と書き直す。*2
$\{ y \}_{y \in \mathcal{P}(x)}$ は $U$ の元の族である。
この時 $\bigcup x = \bigcup_{y \in I} y$ と書けるが、 $I = \mathcal{P}(x) \in U$ であることから、性質(vi)により $\bigcup x \in U$ が従う。${}_\blacksquare$
ということで、Mac Lane本の性質(i)(ii)(iii)(iv)(v)は性質(i)(ii)(iii')(iv)(vi)で置き換えても良いことが分かった。(ii)ももっと絞れるようだが面倒なので今はやめておこう。
