Adjacent Transpositions

Stream: maths

[Thomas Browning]

Transpositions are easy: is_swap

What's the best way to talk about adjacent transpositions? (context: we want to prove that S_n is generated by adjacent transpositions, which I don't think is in mathlib yet).

One consideration is that you might want to talk about adjacent transpositions in S_N or S_Z (or maybe not?)

If you do, then one option would be to define an instance extending linear_order stating that every element has a unique element directly below it and a unique element directly above it. Is this notion in mathlib anywere?

[Thomas Browning]

Or maybe in general an adjacent transposition is a swap between two elements with no element between them?

[Kevin Buzzard]

It's not true that every element has a unique element directly below it of course, I guess the theorem is that you have a unique element directly below you iff you're not bot, and you have a subsingleton of things directly below you in general

[Eric Wieser]

Adjacent swaps on fin n are in #3770

[Eric Wieser]

And on nat in #4739

[Eric Wieser]

But your point about wanting a typeclass is salient