Maximum linearizations of lower sets in ℕ𝕞 with application to monomial ideals

We compute the type (maximum linearization) of the well partial order of bounded lower sets in N m N^m , ordered under inclusion, and find it is ω ω m − 1 ω ^{ω ᵐ⁻¹} . Moreover we compute the type of the set of all lower sets in N m N^m , a topic studied by Aschenbrenner and Pong [Fund. Math. 181 (2004), pp. 27–74], and find that it is equal to \[ ω ∑ k = 1 m ω m − k ( m k − 1 ) + 1. ω ^{∑ ₖ₌₁ᵐ ω ᵐ⁻ᵏ {m}{k-1} }+ 1. \] As a consequence we deduce corresponding lower bounds on effectively given sequences of lower sets and effectively given sequences of monomial ideals in F [ X , Y ] F[X,Y] where F F is a field.