Zulip Chat Archive

Stream: maths

Topic: Adjacent Transpositions


view this post on Zulip Thomas Browning (Dec 25 2020 at 02:11):

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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 25 2020 at 08:25):

Adjacent swaps on fin n are in #3770

view this post on Zulip Eric Wieser (Dec 25 2020 at 08:26):

And on nat in #4739

view this post on Zulip 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