Finite support permutations (on Nat at least)

Stream: new members

[Philippe Duchon]

I understand that Equiv.Perm A is the set of all bijections from A to itself. When A is infinite (I would be happy with Nat), is there simple notation and API for the type (and group) of bijections with a finite support?

[Yaël Dillies]

No, I don't think we have this!

[Kevin Buzzard]

Interestingly, the phrase "finite support" is used to mean "all but finitely many things map to 0" in mathlib (eg docs#Finsupp is clearly named with this in mind) but you're using it to mean "all but finitely many things map to themselves", so only a finite distance from the identity map rather than from the zero map.

[Ruben Van de Velde]

Sounds like we need @[to_multiplicative]

[Kevin Buzzard]

But this would be "all but finitely many things map to 1"

[Philippe Duchon]

At least for finite A, Equiv.Perm.support is defined as the (fin)set of non-fixed points, so I felt justified in using the phrase "finite support" (in the generalized case of arbitrary A) to mean "with a support that happens to be finite", even though it does not agree with the other sense of "finite support".

[Kevin Buzzard]

docs#Equiv.Perm.support is only for permutations of a finite type. But I agree that the word is used in this way; I was just pointing out that mostly in mathlib it's used in a different way.

I feel like Equiv.Perm.support should be called something like Equiv.Perm.finsupport and that Equiv.Perm.support should just be the set, and the finite support elements should be defined as a subgroup using Set.Finite. It would make a nice exercise!