Categorical Restatement of Higman’s Lemma (“Unpolished”)

This is the first section of my current research paper which restates Higman’s Lemma,

If \preceq is a wqo on A, then \ll is a wqo on A^*.

, categorically which will be followed by the proof in the next section. However before I move forward, I want to personally thank Brian O’Neill for helping me specifically in this section. He is a former MIT graduate student and I am forever in debt to him.

If anyone has any suggestions or corrections that you think will be beneficial to this section in my paper, please comment the specifics down below or send it to my email at

Let \cdot_X denote the monoid operation on X and e_X be the identity element on X. Mon and PrO denote the categories of monoids and preorders respectively.

Definition. A preordered monoid, or promonoid, is a quadruple \mathcal{X}=(X,\preceq_X,\cdot_X,e_X) such that

  1. \preceq_X preorders X,
  2. (X,\cdot_X,e_X) is a monoid,
  3. for all x\in X, \ e_X\preceq_xx, and
  4. (for all w,x,y,z\in X) if w\preceq_Xx and y\preceq_Xz, then w\cdot_Xy\preceq_Xx\cdot_Xz.

We may drop the subscripts on \preceq_X and \cdot_X as ambiguity is unlikely.

Let \mathcal{X}=(X,\preceq_X,\cdot_X,e_X) and \mathcal{Y}=(Y,\preceq_Y,\cdot_Y,e_Y) be promonoids. Then the promonoid morphism f:\mathcal{X}\to\mathcal{Y} is a function f:X\to Y where it respects both the order and monoid structures:

  1. f:(X,\cdot_X,e_X)\to(Y,\cdot_Y,e_X) is a monoid morphism such that f(e_X)=e_Y and f(x_1\cdot_Xx_2)=f(x_1)\cdot_Yf(x_2) for all x_1,x_2\in X, and
  2. f:(X,\preceq_X)\to(Y,\preceq_Y) is a preorder morphism such that for all pairs of elements x_1,x_2\in X, if x_1\preceq_Xx_2 then f(x_1)\preceq_Yf(x_2).

By this, promonoids and their morphisms form a category, PoM, whose objects are promonoids and the morphisms are morphisms of underlying objects that respect the order and monoid structures. The category of promonoids comes with two forgetful functors G_\text{pre}:PoM\toPrO and G_\text{mon}:PoM\toMon where a span between categories may be formed:


Definition. Let A be a set. The Kleene closure A^* is the set of all finite sequences of elements of A. It forms a monoid with the identity element \epsilon being the empty sequence and concatenation || being the monoid operation.

Remark. Given a set A, (A^*,||,\epsilon) is the free monoid on A such that for any monoid (B,\cdot,e) if f:A\to B is any function, then there exists a unique monoid morphism f^*:(A^*,||,\epsilon)\to(B,\cdot,e) such that f=f^*\circ\text{inc}_{A\to A^*} where \text{inc}_{A\to A^*}:a\mapsto a:A\to A^* is the inclusion map (equivalently, f^*|_A=f).

We generally use juxtaposition to indicate concatenation: st:=s||t for all s,t\in A^*.

Given a preorder \mathcal{A}=(A,\preceq_A), the string-embedding order \ll_\mathcal{A} on the Kleene closure A^* of A is defined such that for u_1,\cdots,u_m,v_1,\cdots,v_n\in A, u_1,\cdots,u_m\ll_\mathcal{A}v_1,\cdots,v_n iff there exists m indexes of j_i where 1\leq j_1<\cdots<j_m\leq n such that for all i, u_i\leq v_{j_i}. Note that if s\ll t then |s|\leq|t| where |w| denotes the length of w.

As we will only consider the string-embedding order arising from a single preorder \mathcal{A}, it would not be necessary to explicitly indicate the dependence of the string-embedding order on \mathcal{A}, therefore we may simply write \ll.

Remark. For a preorder (A,\preceq), \ll preorders A^*, and the inclusion \text{inc}_{A\to A^*} is a preorder morphism (A,\preceq)\to(A^*,\ll) such that A\subseteq A^*.

Proposition. The forgetful functor G_\text{pre} has a left adjoint F:PrO\toPoM where given any preorder (A,\preceq_A), if (B,\preceq,\cdot_B,e_B) is a promonoid and f:(A,\preceq_A)\to(B,\preceq_B) a preorder morphism, there is a unique promonoid morphism f^*:(A^*,\ll,||,\epsilon)\to(B,\preceq_B,\cdot_B,e_B) such that f=f^*\circ\text{inc}_{A\to A^*}.

Proof. Suppose \mathcal{B}=(B,\preceq_B,\cdot_B,e_B) is a promonoid and f:(A,\preceq_A)\to(B,\preceq_B) a preorder morphism. We know that f lifts to a unique monoid morphism f^*:(A^*,||,\epsilon)\to(B,\cdot_B,e_B). It suffices to show that f^* is order-preserving. Suppose then that s\ll t, where s=u_1,\cdots,u_m and t=v_1,\cdots,v_n. Then for some increasing sequence of indexes j_i with 1\leq j_1<\cdots<j_m\leq n, we have u_i\preceq_Av_{j_i} for i=1,\cdots,m. Expand the finite sequence (u_i)_{1\leq i\leq m} to an n-tuple sequence (u'_j)_{1\leq j\leq n}:


Then s=u_1,\cdots,u_m=u'_1,\cdots,u'_n, and u'_j\preceq_Av_j for j=1,\cdots,n. Since f preserves order, f(u'_j)\preceq_Bf(v_j), j=1,\cdots,n. Because f^* is a monoid morphism which agrees with f on A, we have:




So f^*:(A^*\ll)\to(B,\preceq_B) is also a preorder morphism, as proposed. \blacksquare

In other words, if \mathcal{A}=(A,\preceq_A) is a preorder, then then promonoid (A^*,\ll_\mathcal{A},||,\epsilon) is the free promonoid on \mathcal{A}. Therefore Higman’s Lemma can be restated as follows:

If \mathcal{A} is wqo, then the free promonoid on \mathcal{A} is wqo.






Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s