用 Facebook 幾年了,漸漸不大會組織文字,也忘記寫文章不是為了給別人看,更多的時候,只是為了想要寫,然後記錄而已。雖然 blog 還是開放的空間,比起 FB 強迫式的閱讀,應該溫和了些,不用強迫任何人。有時候會有些衝動,把每個人的訊息一一隱藏,每次連上 FB 充滿各種訊息,相當暴力地佈滿。礙於人際社交,有些是以前同學,即使現在沒有關係了,但解除名單或是將 FB 整個刪掉,說不上來似乎不好(其實沒人在乎)。

總之,再度試著用 blog ,原本想寫些專業文章,只是有點疲倦。

「文學是苦悶的象徵」每隔一陣子讀了幾頁書,總是會想起廚川白村這句話。文字之間的情緒滲透進來的,很少是喜悅大多是難以言喻說不出口的哀戚。那些太過歡樂的,情緒往往都很膚淺很少留住。

Well-definedness

脫稿好久,而且還不是本來預定要寫的東西,只是最近即便是這簡單的例子,也發現把事情講清楚的重要性。

給定一個等價類 \equiv,事實上這個 relation 的性質跟等式一樣,因此作 quotient set 的意義實際上是替代原本的等式,換成這個 relation,所以就有 [a] = [b] 若且唯若 a \equiv b 這件事情。實際上構造也很簡單,就是定義 [a] = \{ x \in X : a \equiv x \}.

接下來的問題是,我們要怎麼在 quotient set 上定義函數呢?事實上就跟一般函數的定義方式一樣,取 C \in X/\equiv 指定對應的對象就好了。但是既然 quotient set 可以寫成 \{ [a] \subseteq X : a \in X \},我們是不是能根據 a 來定義呢?可以的,但是數學教科書都會寫,必須是良好定義的,也就是若 [a] = [b],那麼 f([a]) = f([b]),白話來講,原本被看作一樣的東西,對應過去也是要一樣的。

那為甚麼在一般的集合上定義不需要呢?若是根據 [a]a 表示來定義,事實上我們定義的是一個從原本集合 X 為定義域的函數,而不是 X/\equiv 這個新的集合,而為了要說這個函數可以沿用到 X/\equiv 上,我們自然必須檢查是否還是個集合。

若是用範疇論的語言來解釋的話,考慮 \equiv \overset{\pi_1, \pi_2}{\longrightarrow} X 其中箭頭代表兩個投影函數 (x, y) 分別對應成 xy 的投影而已,那麼 quotient set 事實上是該 diagram 的 coequalizer ,那麼定義 f : X \rightarrow Y  用表示來定義的函數,若是對所有 (x, y) \in R 都滿足 f(x) = f(y) 的話,那麼自然從 coequalizer 會有一個唯一的映射到 Y,而那就是 quotient set 上的函數。

用箭頭語言講的好處是,我們清楚知道是哪些物件在作用,每個步驟都是 diagram 裡的一部分,但是我們又不限定多餘的東西:誰說 quotient set 一定要是 \{[a] \subseteq X : a \in X\}呢?因為與 quotient set 相等的集合有很多,只要有一對一且映成的函數連結起來就夠了。

Yoneda argument – Application

A simple application of Yoneda argument is to prove that a^1 \cong a in Cartesian closed category.

Lemma. In Cartesian closed category, a^1 \cong a where 1 is terminal.

Proof. hom(b, a) \cong hom(b \times 1, a) \cong hom(b, a^1) for all objects b. Hene a \cong a^1.

It’s also quite easy to see that a^{b \times c} \cong (a^b)^c since hom(d, a^{b \times c}) \cong hom(d \times b \times c, a) \cong hom(d \times c, a^b) \cong hom(d, (a^b)^c).  Hence a^{b \times c} \cong (a^b)^c. It’s just like that we prvoe the equality c \wedge b \rightarrow a = c \rightarrow (b \rightarrow a) in the Heyting algebra!

Yoneda argument

I don’t want to repeat the Yoneda lemma, but one of the important corollary should be emphasized. Roughly speaking, given any object c in the category \mathcal{C}, c is determined by its morphisms up to isomorphism. That is, the natural isomorphism between hom-sets corresponds to the isomorphism between objects, i.e. hom(-, c) \cong hom(-, d) \Leftrightarrow c \cong d. How do we prove it? Well, let’s see a simpler analogy in partial orders.

Lemma. \uparrow x = \uparrow y if and only if x = y.
Proof. If \uparrow x = \uparrow y , then a \in \uparrow b and b \in \uparrow a which imply a \leq b and b \leq a. Hence a = b. The converse is quite trivial.

First, we can prove it by brute force method.

Lemma. hom( - , c ) \cong hom( - , d ) if and only if c \cong d.
Proof. Consider the following diagrams,

by replacing f with \phi^{-1}_{d}(id_{d}), we will see that id_{d} = \phi_{c}(id_c) \circ \phi^{-1}_{d}(id_{d}) and we will have the other isomorphism by replacing f with \phi_{c}(id_c) 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 Nat ( hom ( - , r ), K ) \cong Kr where K is a Set-valued functor and r is an object in a locally small category \mathcal{C}. Let K be the hom-set functor hom(-, s). It gives the isomorphism between Nat(hom(-, r), hom(-, s)) \cong hom(r, s). Hence, it indeed tells you that Y(d) = hom(-, d) is fully faithful. Therefore, we have the second proof.

Proof2. Given that Y is fully faithful, thus the natural isomorphisms Y ( d ) \cong Y ( c ) actually correspond to the isomorphism d \cong c and vice verse. That’s it!

為甚麼是 Functional Programming?

正在 Midlands Graduate School 2010 上課,想到一些東西寫點輕鬆的。

我第一個學的語言,嚴格講起來應該是小學二年級的 GW-Basic,姊姊正在念高職時,借她的課本來看,稍微玩一下。不過並沒有認真學,到最後電腦只是拿來玩電動而已。在那之後過很久,高中電子辭典有些內建 gw-basic,那時候還稍微記得上課會寫些東西打發時間,但就只是玩玩而已。 Continue reading

恭喜 Josh ~

恭喜 Josh 獲得 Clarendon Scholarship – University College MPLS Scholarship!(當然同時也獲得入學許可了),原文在此

這代表我以後去 Oxford 可以住 University College 了嗎?XD