Equiv.Perm

Stream: mathlib4

[Yi.Yuan]

Excuse me, I want to construct an Equiv.Perm that rotates the elements in the range(i, j) while keeping the other positions unchanged. For example : (0, ..., i - 1, i, i + 1, ...., j , j + 1, ...., n ) → (0, ..., i - 1, i + 1, ...., j ,i, j + 1, ...., n )

How should I design this? I found finRotate n and Fin.cycleRange in mathlib for now. The former rotates everything, while the latter rotates the range Range(i). I tried to copy the proof of Fin.cycleRange, but it involves a lot of cumbersome steps like Fin (n) ≃ Fin (i + (n - i)).

[Antoine Chambert-Loir]

You can construct it this way, or provide a definition of the permutation you want (using if ... then ... else) and its inverse.

[Yi.Yuan]

Do you mean that I can use many by_cases? It is currently the most efficient approach, but they will probably not merge this into mathlib.

[Jz Pan]

by_cases is in tactic mode. In term mode you should use if ... then ... else if ... then ... else ... just like ordinary programming languages.

[Antoine Chambert-Loir]

Another, more general, option would be, given an embedding e of a type X into a type Y, to define (maybe it exists) the corresponding group morphism Equiv.Perm X ->* Equiv.Perm Y.

[Yaël Dillies]

Yes, this exists, although I can't remember where it is

[Aaron Liu]

#mathlib4 > Equiv.Perm from a list of mappings @ 💬

[Aaron Liu]

Oh, I found docs#Equiv.Perm.viaEmbeddingHom

[Kevin Buzzard]

There's also docs#Equiv.Perm.extendDomainHom