Traditionally, to prove the associativity of the least upper bounds, i.e. we need few lines to prove the inequality from the left hand side and conversely. However, by turning the definition of finit join to the adjunction form, we have a more compact and algebraic-like way to do it. Continue reading
給定一個等價類 ，事實上這個 relation 的性質跟等式一樣，因此作 quotient set 的意義實際上是替代原本的等式，換成這個 relation，所以就有 若且唯若 這件事情。實際上構造也很簡單，就是定義 .
接下來的問題是，我們要怎麼在 quotient set 上定義函數呢？事實上就跟一般函數的定義方式一樣，取 指定對應的對象就好了。但是既然 quotient set 可以寫成 ，我們是不是能根據 來定義呢？可以的，但是數學教科書都會寫，必須是良好定義的，也就是若 ，那麼 ，白話來講，原本被看作一樣的東西，對應過去也是要一樣的。
那為甚麼在一般的集合上定義不需要呢？若是根據 的 表示來定義，事實上我們定義的是一個從原本集合 為定義域的函數，而不是 這個新的集合，而為了要說這個函數可以沿用到 上，我們自然必須檢查是否還是個集合。
若是用範疇論的語言來解釋的話，考慮 其中箭頭代表兩個投影函數 分別對應成 和 的投影而已，那麼 quotient set 事實上是該 diagram 的 coequalizer ，那麼定義 用表示來定義的函數，若是對所有 都滿足 的話，那麼自然從 coequalizer 會有一個唯一的映射到 ，而那就是 quotient set 上的函數。
用箭頭語言講的好處是，我們清楚知道是哪些物件在作用，每個步驟都是 diagram 裡的一部分，但是我們又不限定多餘的東西：誰說 quotient set 一定要是 呢？因為與 quotient set 相等的集合有很多，只要有一對一且映成的函數連結起來就夠了。
A simple application of Yoneda argument is to prove that in Cartesian closed category.
Lemma. In Cartesian closed category, where is terminal.
Proof. for all objects . Hene .
It’s also quite easy to see that since . Hence . It’s just like that we prvoe the equality in the Heyting algebra!
I don’t want to repeat the Yoneda lemma, but one of the important corollary should be emphasized. Roughly speaking, given any object in the category , is determined by its morphisms up to isomorphism. That is, the natural isomorphism between hom-sets corresponds to the isomorphism between objects, i.e. . How do we prove it? Well, let’s see a simpler analogy in partial orders.
Lemma. if and only if .
Proof. If , then and which imply and . Hence . The converse is quite trivial.
First, we can prove it by brute force method.
Lemma. if and only if .
Proof. Consider the following diagrams,
by replacing with , we will see that and we will have the other isomorphism by replacing with and reversing the arrows.
However, the diagram above is exactly used in Yoneda lemma, and of course we can use Yoneda lemma to prove it.
First recall that Yoneda lemma states that where is a Set-valued functor and is an object in a locally small category . Let be the hom-set functor . It gives the isomorphism between . Hence, it indeed tells you that is fully faithful. Therefore, we have the second proof.
Proof2. Given that is fully faithful, thus the natural isomorphisms actually correspond to the isomorphism and vice verse. That’s it!
A quick note: where is the terminal object.
Consider the following diagram,
we have already, and we attempt to find whether is equal to . However, where
Since is a terminal object, the morphism is unique. So, and therefore which is the identity of .
To see that is the identity, we just draw the following diagram,
where also makes the diagram commute. Since is unique, it must be as same as .
Also, to see we just draw the following diagram,
where by the similar argument.
Let’s enjoy some familiar concepts in sets and be happy with the exponential notation of function space.
Normally, a function from set X to set Y is represented as . Sometimes, people say that it is the exponential object in the category of Set, but what does it mean? Is it similar to the exponentiation of numbers, e.g. ?
We can view the disjoint union and intersection as addition and multiplication respectively. For example, we have
where denotes the two-pointed set. In face, the isomorphism is given by and where and . In general, it means that
Using exponential notation, it reads that . It satisfies familiar equalities we learned, e.g.
- where is the empty set and is the one-pointed set.
- for any non-empty set .
With this notation, we can drop the subset notation since is equivalent to where becomes the characteristic function on . That is,
if or otherwise.
Moreover, the belonging relation can be viewed as a function from one-pointed set to , e.g. . Note that is a proposition in set theory but a function is a proposition in the meta-language.
Looking at the above discussion more carefully, we may suspect whether we can talk about set theory purely in terms of objects, morphisms, hom-set and so on. Well, indeed! Basically it is called topos theory and maybe I can say something about topos theory after I fully understand it …
這有個很漂亮的證法, 運用質數的性質就不需要再實際造出函數了。 Continue reading