Conjugate of swap is swap

Stream: Is there code for X?

[Violeta Hernández]

Do we have the result that conjugating docs#Equiv.swap yields another swap operation? And more generally, do we have this for cycle permutations? (I'm not even sure if we have cycle permutations)

[Daniel Weber]

docs#Equiv.Perm.IsCycle.conj

[Violeta Hernández]

Hm, I want to explicitly have the elements that are swapped. I think you should have for instance e * (swap x y) * e⁻¹ = swap (e x) (e y).

[Daniel Weber]

I don't think it's in Mathlib, but

import Mathlib

example {α : Type*} [DecidableEq α] (e : Equiv.Perm α) (x y : α) :
    e * (Equiv.swap x y) * e⁻¹ = Equiv.swap (e x) (e y) := by
  aesop (add norm Equiv.swap_apply_def)

[Violeta Hernández]

Awesome! How does this proof work? I haven't really used aesop in the past

[Daniel Weber]

You can use aesop? (add norm Equiv.swap_apply_def) to see the proof, but it's just using extensionality and splitting to a bunch of cases