The four lifting squares in S4

The displayed products are computed by [F2]: $1342\cdot s_1=3142$, $1342\cdot s_2=1432$, $1342\cdot s_3=1324$, $1423\cdot s_2=1243$, $4132\cdot s_1=1432$, $4132\cdot s_2=4312$, $1432\cdot s_3=1423$ and $4123\cdot s_2=4213$. Their inversion numbers, computed with [F3] and equal to the lengths by [F1], are: $\mathrm{\ell }(1342)=2$, $\mathrm{\ell }(1423)=2$, $\mathrm{\ell }(4132)=4$, $\mathrm{\ell }(1432)=3$, $\mathrm{\ell }(4123)=3$, $\mathrm{\ell }(3142)=3$, $\mathrm{\ell }(1324)=1$, $\mathrm{\ell }(1243)=1$, $\mathrm{\ell }(4312)=5$ and $\mathrm{\ell }(4213)=4$.

First certify $u\le v$ in each case: in (a) and (b), $1342=s_2{s}_3$ occurs at positions $1,2$ of $4132=s_2{s}_3{s}_2{s}_1$; in (c), it occurs at positions $1,2$ of $1432=s_2{s}_3{s}_2$; and in (d), $1423=s_3{s}_2$ occurs at positions $1,2$ of $4123=s_3{s}_2{s}_1$. Each ambient word has length equal to the inversion number of its value, so [F1] and [F5] prove these initial comparisons. The comparisons required by the four cases — $us\le v$ and $u\le vs$ in (a), $us\le vs$ and $u\le vs$ in (b), $us\le vs$ and $us\le v$ in (c), and $us\le v$ and $u\le vs$ in (d) — are certified by subword witnesses in the displayed reduced words, each verified by multiplying out the indicated letters: $3142=s_2{s}_3{s}_1$ is the subword at positions $1,2,4$ of $4132=s_2{s}_3{s}_2{s}_1$; $1342=s_2{s}_3$ is the subword at positions $1,2$ of $1432=s_2{s}_3{s}_2$ and at positions $1,3$ of $4312=s_2{s}_1{s}_3{s}_2{s}_1$; $1432=s_2{s}_3{s}_2$ is the subword at positions $1,3,4$ of $4312=s_2{s}_1{s}_3{s}_2{s}_1$; $1324=s_2$ is the subword at position $1$ of $1432=s_2{s}_3{s}_2$ and at position $2$ of $1423=s_3{s}_2$; $1243=s_3$ is the subword at position $1$ of $4123=s_3{s}_2{s}_1$; and $1423=s_3{s}_2$ is the subword at positions $2,3$ of $4213=s_1{s}_3{s}_2{s}_1$. Each listed ambient word is reduced, since its value has inversion number equal to its length by [F1]; hence the subword criterion [F5] applies and gives the stated comparisons.

The two negative comparisons follow from length alone: in case (a) the elements $us=3142$ and $vs=1432$ both have length $3$ and are distinct, so they are incomparable by [F6], and in particular $us\le vs$ fails; in case (c) the elements $u=1342$ and $vs=1423$ both have length $2$ and are distinct, so they are incomparable by [F6], and in particular $u\le vs$ fails. The equalities of the displayed lengths with the inversion numbers were computed in step 1.1.

The descent and ascent patterns are read off the lengths computed in step 1.1: in (a) $\mathrm{\ell }(vs)=3<4=\mathrm{\ell }(v)$ and $\mathrm{\ell }(us)=3>2=\mathrm{\ell }(u)$; in (b) $\mathrm{\ell }(vs)=5>4$ and $\mathrm{\ell }(us)=3>2$; in (c) $\mathrm{\ell }(vs)=2<3$ and $\mathrm{\ell }(us)=1<2$; and in (d) $\mathrm{\ell }(vs)=4>3$ and $\mathrm{\ell }(us)=1<2$.

Each of the four cases of [F4] is therefore instantiated: case (a) by the pair $u=1342\le v=4132$ with $s=s_1$, where step 1.2 gives $us\le v$ and $u\le vs$ and step 2.1 shows the companion comparison $us\le vs$ fails; case (b) by the same pair with $s=s_2$, where $s$ is an ascent of both and step 1.2 gives $us\le vs$ and $u\le vs$; case (c) by $u=1342\le v=1432$ with $s=s_3$, where $s$ is a descent of both, step 1.2 gives $us\le vs$, $us\le v$ and step 2.1 shows $u\le vs$ fails; and case (d) by $u=1423\le v=4123$ with $s=s_2$, where step 1.2 gives $us\le v$ and $u\le vs$. In each case the four elements $u,v,us,vs$ form the lifting square of the theorem with the sides listed in the statement, and cases (a) and (c) show that the two extra comparisons cannot be asserted uniformly. All computations are finite enumerations in $S_4$ and use no choice principle.