Some elementary facts

Archived page

This page is kept for reference and its original URL still works, but it is not part of the current site and is no longer maintained. Dates and links reflect when it was written.

\(\def\inj{\mathrm{in}}\) \(\def\inji{\mathrm{in}_i}\)

Notation

The symbols \(\mathbb{N}\), \(\omega\), and nat are used interchangeably; they all denote the set of natural numbers.

If \(m\) is a natural number, we write \(m \colon \mathbb N\) and say "\(m\) has type \(\mathbb N\)." (For the reader unfamiliar with type theory, it's safe in the beginning to think of this as meaning \(m\in \mathbb N\).)

For \(m \colon \mathbb N\), we denote and define \(\underline{m} = \{0, 1, \dots, m-1\}\). Let \(a = (a_0, a_1, \dots, a_{m-1})\) be an mtuple of elements from \(A\).

(As explained in the post on composition of operations, the tuple \(a\) may be identified with a function of type \(\underline{m} \to A\), where \(a(i) = a_i\), for each \(i<m\).)

If \(h \colon A \to A\), then \(h\circ a : \underline{m} \to A\) is the function whose \(i\)-th coordinate is \((h\circ a)(i) = h(a(i)) = h(a_i)\), and we may formally identify the function \(h \circ a : \underline{m} \to A\) with its "image tuple" \((h(a_0), h(a_1), \dots, h(a_{m-1}))\).

A signature \(S = (F, \rho)\) consists of a set \(F\) of operation symbols and a function \(\rho \colon F \to \mathbb{N}\). We call \(\rho f\) the arity of the symbol \(f\).

If \(A\) is a set and \(f\) is a \(\rho f\)-ary operation on \(A\), then we may write \(f \colon A^{\rho f} \to A\). On the other hand, as the natural number \(\rho f\) denotes the set \(\{0, 1, \dots, \rho f -1\}\), a function \(a \colon \rho f \to A\) can be identified with its graph, which is simply a \(\rho f\)-tuple of elements from \(A\); that is, \(a i : A\), for each \(i: \rho f\). Then, by identifying the \(\rho f\)-th power \(A^{\rho f}\) with the type \(\rho f \to A\) of functions from \(\{0, 1, \dots, \rho f -1\}\) to \(A\), we thus identify the function type \(A^{\rho f} \to A\) with the type \((\rho f \to A) \to A\).

Examples.\ a. If \(g \colon (\underline{m} \to A) \to A\) is an \(\underline{m}\)-ary operation on \(A\) and if \(a : \underline{m} \to A\), then \(g a = g(a_0, a_1, \dots, a_{m-1})\) has type \(A\).\ b. If \(f \colon (\rho f \to B) \to B\) is a \(\rho f\)-ary operation on \(B\), if \(a \colon \rho f \to A\) is a \(\rho f\)-tuple on \(A\), and if \(h \colon A \to B\), then \(h \circ a \colon \rho f \to B\), so \(f (h \circ a)\) has type \(B\).

Elementary facts

Let \(F\) be an endofunctor on Set and let \((A, f^A)\) and \((B, f^B)\) be \(F\)-algebras each with \(m\) operation symbols. Let \(k_i\) be the arity of the \(i\)-th operation symbol. Then \(F A : \coprod_{i=0}^{m-1}(\underline{k_i} \to A)\). (See the F-algebras post.)

Let \(g\) and \(h\) be homomorphisms from \((A, f^A)\) to \((B, f^B)\). That is, \(g \circ f^A = f^B \circ F g\) (similarly with \(h\) in place of \(g\)).

Define the equalizer of \(g\) and \(h\) as follows: \(E(g,h) = \{ a : A \mid g(a) = h(a) \}\).

Fact 1. \(E(g,h)\) is a subuniverse of \((A, f^A)\).

Proof. Fix arbitrary \(0\leq i< m\) and \(a : \underline{k_i} \to E(g,h)\). We wish to show that \(g (f^A (\inji a)) = h (f^A (\inji a))\), as this will show that \(E(g,h)\) is closed under the \(i\)-th operation of \((A, f^A)\). But this is trivial since, by definition of an \(F\)-algebra homomorphism, we have \(\((g \circ f^A)(\inji a) = (f^B \circ F g)(\inji a) = (f^B \circ F h)(\inji a) = (h \circ f^A)(\inji a).\)\)

Fact 2. If \(X \subseteq A\) and \(X\) generates \((A, f^A)\) and \(g|_X= h|_X\), then \(g = h\).

Proof. Suppose the subset \(X \subseteq A\) generates \((A, f^A)\) and suppose \(g|_X = h|_X\). Fix an arbitrary \(a : A\). We show \(g(a) = h(a)\).

Since \(X\) generates \((A, f^A)\), there exists a term \(t\) and a tuple \(x : \rho t \to X\) of generators such that \(a = t^A x\). Therefore, since \(F g = F h\) on \(X\), we have \(\(g(a) = g(t^A x) = (t^B \circ F g)(x) = (t^B \circ F h)(x) = h(t^A x) = h(a).\)\)

Fact 3. If \(A\) and \(B\) are finite sets and \(X\) generates \((A, f^A)\), then \(|\mathrm{Hom}((A, f^A),(B, f^B))| \leq |B|^{|X|}\).

Proof. By Fact 2, a homomorphism is uniquely determined by its restriction to a generating set. If \(X\) generates \((A, f^A)\), then since there are exactly \(|B|^{|X|}\) functions from \(X\) to \(B\) we have \(|\mathrm{Hom}((A, f^A),(B, f^B))| \leq |B|^{|X|}\).

Fact 4. Suppose \(g\) and \(h\) are homomorphisms from \((A, f^A)\) to \((B, f^B)\) and from \((A, f^A)\) to \((C,f^C)\), respectively. Assume \(g\) is surjective, and \(\ker g \subseteq \ker h\). Then there exists a homomorphism \(k : (B, f^B)\to (C, f^C)\) such that \(h = k \circ g\).

Proof. We define \(k : (B, f^B)\to (C, f^C)\) constructively, as follows:

Fix \(b\colon B\). Since \(g\) is surjective, the set \(g^{-1}\{b\} \subseteq A\) is nonempty, and since \(\ker g \subseteq \ker h\), we see that every element of \(g^{-1}\{b\}\) is mapped by \(h\) to a single element of \(C\). Label this element \(c_b\). That is, \(h(a) = c_b\), for all \(a : g^{-1}\{b\}\). We define \(k(b) = c_b\). Since \(b\) was arbitrary, \(k\) is defined on all of \(B\) in this way.

Now it's easy to see that \(k g = h\) by construction. Indeed, for each \(a \in A\), we have \(a \in g^{-1}\{g(a)\}\), so \(k(g(a)) = h(a)\) by definition.

To see that \(k\) is a homomorphism, let there be \(m\) operation symbols and let \(0\leq i< m\) be arbitrary. Fix \(b \colon \underline{k_i} \to B\). Since \(g\) is surjective, for each \(i \colon \underline{k_i}\), the subset \(g^{-1}\{b(i)\}\subseteq A\) is nonempty and is mapped by \(h\) to a single point of \(C\) (since \(\ker g \subseteq \ker h\)). Label this point \(c_i\) and define \(c \colon \underline{k_i} \to C\) by \(c(i) = c_i\).

We want to show \((f^C \circ F k) (b) = (k \circ f^B)(b).\) The left hand side is \(f^C c\), which is equal to \((h \circ f^A)(a)\) for some \(a\colon \underline{k_i} \to A\), since \(h\) is a homomorphism. Therefore, \(\((f^C \circ F k) (b) = (h \circ f^A) (a) = (k \circ g \circ f^A)(a) = (k \circ f^B \circ F g)(a) = (k \circ f^B)(b).\)\)