This is the first section of my current research paper which restates Higman’s Lemma,
If is a wqo on , then is a wqo on .
, 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 firstname.lastname@example.org.
Let denote the monoid operation on and be the identity element on . Mon and PrO denote the categories of monoids and preorders respectively.
Definition. A preordered monoid, or promonoid, is a quadruple such that
- preorders ,
- is a monoid,
- for all , and
- (for all ) if and , then .
We may drop the subscripts on and as ambiguity is unlikely.
Let and be promonoids. Then the promonoid morphism is a function where it respects both the order and monoid structures:
- is a monoid morphism such that and for all , and
- is a preorder morphism such that for all pairs of elements , if then .
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 PoMPrO and PoMMon where a span between categories may be formed:
Definition. Let be a set. The Kleene closure is the set of all finite sequences of elements of . It forms a monoid with the identity element being the empty sequence and concatenation being the monoid operation.
Remark. Given a set , is the free monoid on such that for any monoid if is any function, then there exists a unique monoid morphism such that where is the inclusion map (equivalently, ).
We generally use juxtaposition to indicate concatenation: for all .
Given a preorder , the string-embedding order on the Kleene closure of is defined such that for , iff there exists indexes of where such that for all , . Note that if then where denotes the length of .
As we will only consider the string-embedding order arising from a single preorder , it would not be necessary to explicitly indicate the dependence of the string-embedding order on , therefore we may simply write .
Remark. For a preorder , preorders , and the inclusion is a preorder morphism such that .
Proposition. The forgetful functor has a left adjoint PrOPoM where given any preorder , if is a promonoid and a preorder morphism, there is a unique promonoid morphism such that .
Proof. Suppose is a promonoid and a preorder morphism. We know that lifts to a unique monoid morphism . It suffices to show that is order-preserving. Suppose then that , where and . Then for some increasing sequence of indexes with , we have for . Expand the finite sequence to an -tuple sequence :
Then , and for . Since preserves order, , . Because is a monoid morphism which agrees with on , we have:
So is also a preorder morphism, as proposed.
In other words, if is a preorder, then then promonoid is the free promonoid on . Therefore Higman’s Lemma can be restated as follows:
If is wqo, then the free promonoid on is wqo.