Concrete permutation

Stream: Is there code for X?

[Oliver Nash]

Do we have a standard way to represent a concrete permutation?

For example, suppose I wanted to talk about the permutation 3, 0, 4, 1, 2 of Fin 5, how should I represent it?

[Oliver Nash]

Here's one way which I don't particularly like:

[EDIT: removed to prevent confusing future people as it was nonsense]

[Oliver Nash]

What better means exist?

[Oliver Nash]

Oh wait, I'm missing the obvious:

#check (Equiv.ofBijective [3, 0, 4, 1, 2].get (by decide) : Equiv.Perm (Fin 5))

[Yaël Dillies]

Look at file#Mathlib/GroupTheory/Perm/Cycle/Concrete and around

[Oliver Nash]

Thanks! How did I miss this? I think this is a sign I need to go to bed!

[Oliver Nash]

OK that is a useful file but it doesn't quite seem to have what I want. Possibly just notation for the construction I outlined above might suffice.

[Oliver Nash]

Anyway, I have to stop for now.

[Eric Wieser]

#24960 has some links between Fin and Vector, but it evolved into permutations of natural numbers instead

[Yakov Pechersky]

Why doesn't c[3,0,4,1,2] work for your use case?

[Kevin Buzzard]

There are two standard ways to represent permutations of {0,1,2,...,n}. One is the "product of disjoint cycles" notation, the other is the "write down a list, the j'th element of which is where j goes" and I think Oliver is talking about the latter whereas I think you're talking about the former (but I might be wrong, I don't know this part of the library at all, I just know there are two standard ways to represent permutations)

[Eric Wieser]

Oliver, surely you're in trouble there because Fintype.equivFin is an arbitrary bijection, and so toPerm [0, 1, 2, 3, 4] is not the identity permutation

[Matt Diamond]

yeah I think the object Oliver is talking about would be c[3, 0, 1] * c[2, 4] in cycle format, considered as a permutation of 0, 1, 2, 3, 4 (we move 3 to where 0 is, move 0 to where 1 is, etc.)

[Eric Wieser]

Here's a computable implementation with some annoying proofs absent:

import Mathlib

@[simp]
theorem Vector.finIdxOf?_eq_some_iff {α n} [BEq α] [LawfulBEq α] {v : Vector α n} {a : α} {i : Fin n} :
    v.finIdxOf? a = some i ↔ v[i] = a ∧ ∀ j < i, ¬v[j] = a := by
  obtain ⟨xs, rfl⟩ := v
  simp

-- Like `List.get_eq_getElem`
theorem Vector.get_eq_getElem (v : Vector α n) (i : Fin n) : v.get i = v[(i : ℕ)] := rfl

open Function

def Vector.toPerm (v : Vector (Fin n) n) (h : Injective v.get) :
    Equiv.Perm (Fin n) where
  toFun := v.get
  invFun x := (v.finIdxOf? x).get <| by
    let ⟨i, hi⟩ := Finite.surjective_of_injective h x
    cases v
    aesop
  left_inv x := by
    dsimp
    apply Option.get_of_eq_some
    simpa [← Vector.get_eq_getElem, h.eq_iff] using (fun _ => ne_of_lt)
  right_inv x := by
    rw [Vector.get_eq_getElem]
    refine (Vector.finIdxOf?_eq_some_iff.1 ?_).1
    simp

#eval! #v[0, 1, 2, 3, 4].toPerm (by decide)
#eval! #v[3, 0, 4, 1, 2].toPerm (by decide)
#eval c[3,0,4,1,(2 : Fin 5)] -- not the same thing

[Eric Wieser]

The two sorrys look like missing theorems that core or batteries wants, so the fact they're annoying doesn't make this a bad idea

[Eric Wieser]

Maybe @Wrenna Robson already has a proof of them?

[Yakov Pechersky]

I would expect to see a List.ofFn somewhere here, to me, Vector is a red herring.

[Eric Wieser]

That goes in the wrong direction, it's the opposite to get

[Yakov Pechersky]

I thought it would be something like Perm.ofFn ![3,0,4,1,2]

[Wrenna Robson]

My work definitely covers this stuff.

[Wrenna Robson]

Eric Wieser said:

#24960 has some links between Fin and Vector, but it evolved into permutations of natural numbers instead

I don't think this is quite fair as a description. It could easily be "about" Fin as well.

Essentially I have done a lot of work on thinking about concrete permutations in a nice way.

[Wrenna Robson]

I use Vectors though because I wanted fairly nice performance for some specific uses.

[Eric Wieser]

Edited above to be sorry free, PR'd as batteries#1262

[Wrenna Robson]

I have in a repository a nice type which essentially captures "all finite permutations" using "one line notation" rather than cycle notation.

[Wrenna Robson]

It depends in some ways if you want it for logical and mathematical reasoning or for calculation and computation. I needed the latter. I feel like the existing theories probably cover the former?

[Wrenna Robson]

My argument is that permutations of Fin n are most naturally thought of as permutations of the naturals with finite support because it becomes much more obvious how you should combine them.

[Wrenna Robson]

Cycle notation is obviously also useful for this but sometimes it's useful to just be able to write down a permutation with decomposing it.

[Thomas Browning]

There's also this method from docs#Equiv.Perm.fin_5_not_solvable

theorem Equiv.Perm.fin_5_not_solvable : ¬IsSolvable (Equiv.Perm (Fin 5)) := by
  let x : Equiv.Perm (Fin 5) := ⟨![1, 2, 0, 3, 4], ![2, 0, 1, 3, 4], by decide, by decide⟩
  let y : Equiv.Perm (Fin 5) := ⟨![3, 4, 2, 0, 1], ![3, 4, 2, 0, 1], by decide, by decide⟩
  let z : Equiv.Perm (Fin 5) := ⟨![0, 3, 2, 1, 4], ![0, 3, 2, 1, 4], by decide, by decide⟩
  have key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹ := by unfold x y z; decide
  refine not_solvable_of_mem_derivedSeries (show x ≠ 1 by decide) fun n => ?_
  induction n with
  | zero => exact mem_top x
  | succ n ih =>
    rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]
    exact commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)

[Wrenna Robson]

Yes I think that kind of construction basically works. As I say on balance I favour, through experience, not having the carrying entries be Fin n but instead Nat - essentially my argument is that the fact that all the entries are less than n should be a global property and not a local one.

[Wrenna Robson]

Sorry if I seem terse about this - it's past midnight here and also my discussion with Eric about it the other day seemed to just go round and round. But I spent months of my time thinking about different ways of doing this and the above is the conclusion I came to. I know that's not a fully-reasoned argument but I haven't written the paper yet.

[Wrenna Robson]

There's an interesting and subtle argument that arises from the fact that you can use injectivity implying surjectivity - in the way that Eric does above - to construct the permutation without knowing all the information you think you'd need to know.

[Wrenna Robson]

But mostly it's just neater and I hate dependent type casting if I can help it (and not making the individual entries Fin n avoids a lot of that).

[Wrenna Robson]

def ofVector (a : Vector ℕ n) (hx : ∀ x (hx : x < n), a[x] < n := by decide)
  (ha : a.toList.Nodup := by decide) : PermOf n where
  toVector := a
  invVector := (Vector.range n).map a.toList.idxOf
  getElem_toVector_lt := hx
  getElem_invVector_getElem_toVector := fun {i} hi => by
    simp_rw [Vector.getElem_map, Vector.getElem_range]
    exact a.toList.idxOf_getElem ha _ _

I do the above construction from a Vector like this.

[Wrenna Robson]

(Note that again here the use of List.idxOfis convenient because we are working with ℕ. As I say I really am quite convinced this is the way to go.)

[Oliver Nash]

Wow, what a great set of responses :)

@Kevin Buzzard and @Matt Diamond are right of course: I was not using cycle notation, which also answers @Yakov Pechersky 's very sensible question about why I didn't want c[3, 0, 4, 1, 2]. Also @Eric Wieser is right that using Fintype.equivFin was insanity.

[Wrenna Robson]

What was the context ooi?

[Oliver Nash]

Just for for some fun, I was toying with the idea if introducing a concrete model for the g2 root system. There are lots of ways to do this (especially as the Weyl group is a dihedral group) but my preferred approach requires me to supply data of some explicit permutations.

[Wrenna Robson]

Permutations on what?

[Wrenna Robson]

Sounds fun, by the way.

[Oliver Nash]

I now wonder if we should introduce:

set_option linter.unusedTactic false in
notation3 (prettyPrint := false) "p["(l", "* => foldr (h t => List.cons h t) List.nil)"]" =>
  Equiv.ofBijective (List.get l) (by decide)

#check (p[3, 0, 4, 1, 2] : Equiv.Perm (Fin 5)) -- works!

[Oliver Nash]

Wrenna Robson said:

Permutations on what?

This is a choice but pobably Fin 12 is the most convenient thing.

[Wrenna Robson]

So I do like this, but (see above etc.) I think there is value in being able to do, say, p[3, 0, 4, 1, 2] * p[1, 0] = p [0, 3, 4, 1, 2], say.

[Wrenna Robson]

If you make this Equiv.Perm (Fin n)) you can't really do that.

[Oliver Nash]

You mean it should be computable?

For once I agree: I would prefer a computable thing here.

[Wrenna Robson]

Aye. Apologies for linking a random file, but see FinitePerm in this file:
https://github.com/linesthatinterlace/controlbits/blob/master/CBConcrete/CBConcrete/PermOf/MonoidHom.lean

[Wrenna Robson]

structure FinitePerm where
  len : ℕ
  toPermOf : PermOf len
  toPermOf_minLen : toPermOf.minLen = len
  deriving DecidableEq

[Oliver Nash]

Oh I definitely do want a term of type Equiv.Perm α (for some α). The reason my definition above is not computable is that the inverse is not explicit.

[Wrenna Robson]

Oh that's easy enough to convert to :)

[Eric Wieser]

Oliver Nash said:

You mean it should be computable?

For once I agree: I would prefer a computable thing here.

Your strategy is to post deliberately non-computable code to increase engagement and snipe someone into writing the computable version for you, right?

[Oliver Nash]

Exactly :)

[Wrenna Robson]

Wrenna Robson said:

structure FinitePerm where
  len : ℕ
  toPermOf : PermOf len
  toPermOf_minLen : toPermOf.minLen = len
  deriving DecidableEq

Essentially this is a type that captures "a finite permutation, written in minimal one-line form".

[Wrenna Robson]

And it's computable I believe :)

[Wrenna Robson]

Then I have def natPerm : FinitePerm →* Perm ℕ which is basically the conversion to a "proper" Equiv.

[Wrenna Robson]

So I think I have already written something that ought to be suitable but I need some help person-handling it into mathlib in the right form.

[Eric Wieser]

Does Oliver need these extra abstractions, or would Vector.toPerm above suffice, which is computable but not efficient.

[Wrenna Robson]

I think that's nice, but it doesn't solve the issue that being able to do p[3, 0, 4, 1, 2] * p[1, 0] = p [0, 3, 4, 1, 2] etc. is desirable.

[Oliver Nash]

Yeah I mean Equiv.ofBijective (List.get l) (by decide) is sufficient for me, but I think if we are going to introduce a notation to own p[...] then it probably should be computable, and should describe a term of type Equiv.Perm α.

[Wrenna Robson]

Basically you kind of want to compute permutations together that aren't the same length. This gives a way of doing that and hides the abstractions.

[Eric Wieser]

I don't think Oliver's application cares about mixing lengths

[Wrenna Robson]

Right :)

[Eric Wieser]

Oliver Nash said:

and should describe a term of type Equiv.Perm α.

This could only work with FinEnum

[Wrenna Robson]

Then yeah I think Vector.toPerm or ofVector work fine.

[Wrenna Robson]

Eric Wieser said:

Oliver Nash said:

and should describe a term of type Equiv.Perm α.

This could only work with FinEnum

Not quite true - it only needs to embed, after all.

[Wrenna Robson]

Basically, if FixGENat n is the subgroup of Perm ℕ which fixes all inputs >= n, what you need is an embedding of Equiv.Perm α into ⨆ (n : ℕ), FixGENat n.

[Wrenna Robson]

Well, hmm, I guess α is ℕ. The point is that ⨆ (n : ℕ), FixGENat n is much smaller and more controlled than Perm ℕ.

[Wrenna Robson]

(Well, "smaller".)

[Wrenna Robson]

I do think having a convenient short notation for Equiv.Perm (Fin n) is an unambiguous good though, it is clearly going to make sense for some applications.

[Eric Wieser]

I think for other types it doesn't make so much sense, p[A, a, æ] relies on the reader knowing what the canonical order of the type is (the contents of the docs#FinEnum instance)

[Wrenna Robson]

I am inclined to agree.

[Eric Wieser]

You could imagine p[a=>A, A=>a] or something though

[Wrenna Robson]

Oh, that would be quite nice I think.

[Eric Wieser]

If we want that notation for perms we should have it for regular functions too I think; right now that's only possible for constants on the LHS of the =>

[Wrenna Robson]

In effect what you're talking about there is the two line notation, right?

[Wrenna Robson]

In the sense of
image.png

[Wrenna Robson]

But for a general type.

[Wrenna Robson]

Eric Wieser said:

If we want that notation for perms we should have it for regular functions too I think; right now that's only possible for constants on the LHS of the =>

Of course such functions are precisely those with finite support I think?

[Wrenna Robson]

I am inclined to agree that that would be nice.

[Wrenna Robson]

I'm not sure what the efficient way to calculate that such an (asserted) permutation is actually a permutation is.

[Eric Wieser]

I don't think we care about efficient, decide is enough

[Wrenna Robson]

Well, true - I guess I meant I wasn't sure what procedure decide would use, if the underlying type is not finite.

[Wrenna Robson]

Wrenna Robson said:

Eric Wieser said:

If we want that notation for perms we should have it for regular functions too I think; right now that's only possible for constants on the LHS of the =>

Of course such functions are precisely those with finite support I think?

(I take it from the react that this is not correct - what am I missing?)

[Eric Wieser]

You only need to decide anything when building the permutation, there's nothing to decide for a raw function (eg the function that swaps π and e and is the identity elsewhere)

[Wrenna Robson]

Sure, agreed on that.

[Wrenna Robson]

But suppose you have p[π=>e, e=>π]. What does decide do to construct the permutation?

[Eric Wieser]

Well, the comment I :-1: d was about functions not perms...

[Wrenna Robson]

No I know, I just would have thought that, in theory, every function with finite support could be written in this notation.

[Eric Wieser]

Indeed, and such notation already exists (with "support" meaning "not zero")

[Eric Wieser]

Wrenna Robson said:

But suppose you have p[π=>e, e=>π]. What does decide do to construct the permutation?

Bijectivity on the finite support

[Wrenna Robson]

Eric Wieser said:

If we want that notation for perms we should have it for regular functions too I think; right now that's only possible for constants on the LHS of the =>

Oh, maybe I misunderstood this comment, then.

[Wrenna Robson]

I took that to mean we either didn't have it for regular functions or in a limited case (though I suppose I am not certain what you meant by constants on the LHS of the =>).

[Wrenna Robson]

Eric Wieser said:

Wrenna Robson said:

But suppose you have p[π=>e, e=>π]. What does decide do to construct the permutation?

Bijectivity on the finite support

Right, so ultimately Fintype.decidableBijectiveFintype?

[Kevin Buzzard]

Wrenna Robson said:

So I do like this, but (see above etc.) I think there is value in being able to do, say, p[3, 0, 4, 1, 2] * p[1, 0] = p [0, 3, 4, 1, 2], say.

p[1, 0] makes no sense, right? Or should it expand to p[1, 0, 2, 3, 4]?

[Wrenna Robson]

Yes, that.

[Wrenna Robson]

But the nice thing about my FinitePerm type is that it doesn't matter for this kind of thing.

[Wrenna Robson]

i.e. you can just mash together permutations of different lengths, computably, and not worry about expanding them to the same length.

[Wrenna Robson]

So in fact it is true that p[1, 0] = p[1, 0, 2] = p[1, 0, 2, 3], etc.

[Eric Wieser]

I would guess that in 90% of cases this would just be a trap for users

[Wrenna Robson]

Fair!

[Wrenna Robson]

Ultimately I didn't use that part, that was just for fun, so I haven't "field tested" it.

[Wrenna Robson]

I think this => notation would be useful though, quite agree there.

[Wrenna Robson]

Notably though, like, p[0=>1, 1=>0] in that notation is very similar. So I am not sure why you feel that's less of a trap.

[Oliver Nash]

FWIW here are the concrete permutations in action #25480 (this is a bit of an experimental PR --- I'm not sure about the design just yet)