An equational way to prove associativity of least upper bounds

Traditionally, to prove the associativity of the least upper bounds, i.e. x \vee (y \vee z) = (x \vee y) \vee z 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




給定一個等價類 \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!

a x 1 \cong a

A quick note: A \times 1 \cong A where 1 is the terminal object.

Consider the following diagram,

we have id_a = \pi_1 \circ \langle id_a, ! \rangle already, and we attempt to find whether \langle id_a, ! \rangle \circ \pi_1 is equal to id_{a \times a}. However, \langle id_a, ! \rangle \circ \pi_1 = \langle id_a \circ \pi_1, ! \circ \pi_1 \rangle where


Since 1 is a terminal object, the morphism a \times a \rightarrow 1 is unique. So, ! \circ \pi_1 = \pi_2 and therefore \langle id_a \circ \pi_1, ! \circ \pi_1 \rangle = \langle \pi_1, \pi_2 \rangle which is the identity of a \times 1.

To see that \langle \pi_1, \pi_2 \rangle is the identity, we just draw the following diagram,

where id_{a \times b} also makes the diagram commute. Since \langle \pi_1, \pi_2 \rangle is unique, it must be as same as id_{a \times b}.

Also, to see \langle f, g \rangle \circ h = \langle f \circ h, g \circ h\rangle we just draw the following diagram,

where \langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle by the similar argument.

Exponential Notation

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 f:X \rightarrow Y. 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. 2^3?

Indeed, yes.

We can view the disjoint union and intersection as addition and multiplication respectively. For example, we have

\displaystyle{ (\mathbf{2} \rightarrow A) \cong A \times A}

where \mathbf{2} denotes the two-pointed set. In face, the isomorphism is given by f \mapsto (f(0), f(1)) and (x, y) \mapsto g where g(0) = x and g(1) = y. In general, it means that

\displaystyle{(B \rightarrow A) \cong \underbrace{A \times A \times \dots \times A}_{| B |}}.

Using exponential notation, it reads that A^{B} \cong \prod_{i = 1}^{|B|} A. It satisfies familiar equalities we learned, e.g.

  1. A^B \times A^C \cong A^{B + C}.
  2. (A^{B})^{C} \cong A^{B \times C}.
  3. A^{0} \cong 1 where 0 is the empty set and 1 is the one-pointed set.
  4. 0^{A} \cong 0 for any non-empty set A.

With this notation, we can drop the subset notation \subseteq since S \subseteq X is equivalent to S \in \mathbf{2}^{X} where S becomes the characteristic function on S. That is,

\chi_{S}(x) = 1 if x \in S or \chi_{S}(x) = 0 otherwise.

Moreover, the belonging relation \in can be viewed as a function from one-pointed set to X, e.g. (* \rightarrow A) \equiv A^{*}. Note that x \in X is a proposition in set theory but a function x : * \rightarrow A 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 …