Topic: Adjacent Transpositions
Thomas Browning (Dec 25 2020 at 02:11):
Transpositions are easy:
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 (Dec 25 2020 at 02:13):
Or maybe in general an adjacent transposition is a swap between two elements with no element between them?
Kevin Buzzard (Dec 25 2020 at 02:35):
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 (Dec 25 2020 at 08:25):
Adjacent swaps on
fin n are in #3770
Eric Wieser (Dec 25 2020 at 08:26):
nat in #4739
Eric Wieser (Dec 25 2020 at 08:27):
But your point about wanting a typeclass is salient
Last updated: May 09 2021 at 09:11 UTC