MulAction for OrderIso

Stream: mathlib4

[Eric Paul]

Is this an instance that should be added?

import Mathlib

variable {α : Type*} [LinearOrder α]

instance : MulAction (α ≃o α) α where
  smul f := f
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

I wanted to use this to talk about the orbit of an element in a linear order under order automorphisms.

[Aaron Liu]

You can use docs#Equiv.Perm

[Eric Paul]

As far as I can tell, those are not order preserving maps

[Aaron Liu]

I mean, to get the MulAction instance

[Aaron Liu]

(I realize this might not be as good of an idea as I had thought)

[Eric Wieser]

I think the instance above should be an instance, we have this pattern in general

[Eric Wieser]

@loogle "applyMulAction"

[loogle]

:search: Function.End.applyMulAction, Equiv.Perm.applyMulAction, and 2 more

[Eric Wieser]

I don't think you need to assume a linear order though

[Aaron Liu]

You don't need any order at all, just LE, since this is an instance about RelIso

[Eric Paul]

So it seems like this is the instance we want:

import Mathlib

variable {α : Type*} [LE α]

instance RelIso.applyMulAction : MulAction ((· ≤ (· : α)) ≃r (· ≤ (· : α))) α where
  smul f := f
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

I'd be happy to make a PR for it if that seems reasonable

[Daniel Weber]

Perhaps more generally

import Mathlib

variable {α : Type*} {s : α → α → Prop}

instance RelIso.applyMulAction : MulAction (s ≃r s) α where
  smul f := f
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

[Yaël Dillies]

This is in a PR of mine

[Yaël Dillies]

#21024

[Yaël Dillies]

cc @Eric Paul to avoid you duplicating work :smile:

[Eric Paul]

Awesome, that looks like just what I need!