Rewriting vs. lifting

Stream: maths

[Mitchell Lee]

Hi, I was talking to some undergraduate students at the National University of Singapore about how to formalize the theory of Coxeter groups today. We happened upon an idea that I think has the potential to be quite useful, not just for the formalization of Coxeter groups, but for formalization in general. I'm sure this idea is not new, but I have not seen it written down anywhere.

This is best illustrated with an example. Let $W$ be a Coxeter system with simple generators $(s_i)_{i \in B}$ and Coxeter matrix $(m(i, i'))_{i, i' \in B}$. Then we have the following key theorem.

Matsumoto's theorem.

Let $s_{i_1} \cdots s_{i_{\ell}} = s_{i'_1} \cdots s_{i'_\ell}$ be two reduced expressions for the same element of $W$. Then the sequence $(i_1, \ldots, i_\ell)$ can be transformed into $(i'_1, \ldots, i'_\ell)$ via a sequence of braid moves. (A braid move on the letters $i, i' \in B$, where $i \neq i'$, changes a contiguous subsequence of length $m(i, i')$ of the form $(i, i', i, i', \ldots)$ to a sequence of length $m(i, i')$ of the form $(i', i, i', i, \ldots)$.)

This is a theorem about "rewriting"; that is, changing one string into another by applying a sequence of local moves.

[Mitchell Lee]

As useful as this theorem is, it's very difficult to use in a formal setting. For example, suppose that you want to prove that if $s_{i_1} \cdots s_{i_{\ell}} = s_{i'_1} \cdots s_{i'_\ell}$ are two reduced expressions for the same element of $W$, then we have the equality of sets $\{i_1, \ldots, i_\ell\} = \{i'_1, \ldots, i'_\ell\}$. (This is one of the key ingredients in the proof that a parabolic subgroup of a Coxeter group is again a Coxeter group.)

Informally, you would just say "this is a trivial consequence of Matsumoto's theorem". Formally, though, you have to use induction on the number of braid moves used to transform $(i_1, \ldots, i_\ell)$ to $(i'_1, \ldots, i'_\ell)$. Then, you need to show that each braid move doesn't change the set of indices, which is really annoying, because you have to split the word into three pieces (the second of which gets affected by the braid move), turn each one into a set, and take the union. Honestly, it seems like a nightmare.

[Mitchell Lee]

The solution to this issue is to instead write Matsumoto's theorem in the following equivalent form.

Matsumoto's theorem, equivalent form.

Let $M$ be a monoid and let $f \colon B \to M$ be a function (where $B$ is the set that indexes the simple reflections of $W$). Suppose that for all $i, i' \in B$ with $i \neq i'$, we have $f(i) f(i') f(i) f(i') \cdots = f(i') f(i) f(i') f(i) \cdots$, where there are $m(i, i')$ terms being multiplied on each side of the equation. Then there is a unique function $\tilde f \colon W \to M$ such that for every reduced word $s_{i_1} \cdots s_{i_\ell}$, we have $\tilde f(s_{i_1} \cdots s_{i_\ell}) = f(i_1) \cdots f(i_\ell)$.

Now, this is a theorem about "lifting"; that is, factoring a function that satisfies a particular property.

[Mitchell Lee]

This form is much easier to state and use. (I'm not sure it's easier to prove, but at least you only have to do that once.) To illustrate, let's use it to prove the lemma we had trouble with earlier: if $s_{i_1} \cdots s_{i_{\ell}} = s_{i'_1} \cdots s_{i'_\ell}$ are two reduced expressions for the same element of $W$, then we have the equality of sets $\{i_1, \ldots, i_\ell\} = \{i'_1, \ldots, i'_\ell\}$.

The proof goes as follows. Let $M$ be the set of all subsets of $B$, where the monoid operation is union. For all $i \in B$, let $f(i) = \{i\} \in M$. Then for all $i, i' \in B$ with $i \neq i'$, we have $f(i) \cup f(i') \cup f(i) \cup f(i') \cup \cdots = f(i') \cup f(i) \cup f(i') \cup f(i) \cup \cdots$, because both sides are equal to $\{i, i'\}$. Hence, the theorem guarantees the existence of a lift $\tilde f$. Finally, we calculate

$$\{i_1, \ldots, i_\ell\} = \tilde f(s_{i_1} \cdots s_{i_\ell}) = \tilde f(s_{i'_1} \cdots s_{i'_\ell}) = \{i'_1, \ldots, i'_\ell\}.$$

This proof method is quite friendly to formalization. Much friendlier than what we were trying to do earlier.

[Mitchell Lee]

You can use the same "lifting" form of Matsumoto's theorem to do anything that you could use the "rewriting" form for:

Bruhat order.

Let $M$ be the set of all subsets of $W$, where the monoid operation is pointwise product (i.e. $AB = \{ab \mid a \in A, b \in B\}$). Let $f(i) = \{1, s_i\}$. It is not too difficult to check that this satisfies the hypothesis of Matsumoto's theorem. For all $w \in W$, we have that $\tilde f(w)$ is the interval $[1, w]$ of the (strong) Bruhat order on $W$. In fact, this is a reasonable way to define the Bruhat order.

Iwahori-Hecke algebras

Define the Iwahori-Hecke algebra $H_R$ by generators, the braid relations, and the quadratic relation. Then, Matsumoto's theorem gives you the elements $T_w \in H_R$, and you can show that they form a basis of $H_R$ through other means.

Divided difference operators.

Since the divided difference operators $\partial_i$ satisfy the braid relations of the symmetric group, one can use Matsumoto's theorem to define $\partial_w$ for all $w \in W$. This is one way to define Schubert polynomials.

[Mitchell Lee]

But that's not all. One can show that for any function $f$ that satisfies the hypotheses of Matsumoto's theorem, the lift $\tilde f$ is "almost a monoid homomorphism": that is, $\tilde f(1) = 1$ and $\tilde f(u v) = \tilde f(u) \tilde f(v)$ for all $u, v \in W$ such that $\ell(uv) = \ell(u) + \ell(v)$. In fact, this is the defining property of functions obtained through this lifting process. So, by writing Matsumoto's theorem in the lifting form, we now also have a class of functions, the "almost monoid homomorphisms", that we can prove general lemmas about, and we get those lemmas for free in every one of the above examples.

Does anyone have any other examples of theorems that are traditionally stated in a "rewriting" form, but can be instead stated in a "lifting" form? Is there any general design principle to be gleaned here?

[Yaël Dillies]

Something like the proof of the ping pong lemma maybe? Not sure I remember correctly

[Edward van de Meent]

To me, this problem has a similar "taste" to the work @Floris van Doorn has mentioned in a talk, about notation/api for working with iterated/indexed integrals? the similarities could be very minor though, the talk was a few months ago so i don't remember the details...

[Antoine Chambert-Loir]

Mathlib is full of lifting lemmas of this kind. docs#TensorProduct.lift, docs#FreeGroup.lift, docs#SeparationQuotient.lift, etc.

[Antoine Chambert-Loir]

IIUC, Matsumoto's theorem goes further: it's not so much about the relations satisfied by the elements of a Coxeter group that about the generators of the canonical morphism from the free group on the simple reflexions to the Coxeter group.

[Mitchell Lee]

Yes, there are lifting lemmas in mathlib. But the examples you gave are all explicitly used in the informal literature.

I was asking if there are other theorems that are traditionally stated in the form "A can be rewritten to B using a series of moves" (i.e. in a "syntactic" formulation), but can also be understood as a lifting lemma (i.e. in a "semantic" formulation).