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 rachman.jm@gmail.com.
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
PoM
PrO and
PoM
Mon 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
PrO
PoM 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.
Like this:
Like Loading...