feat: tautological action of RelIso on the ground type (#21024)

This will be useful to make order isomorphisms act on flags.

Also add the monoid structure on `r →r r` and `r ↪r r` and the corresponding tautological actions.

From MiscYD

Author: YaelDillies

Mathlib.lean

@@ -749,6 +749,7 @@ import Mathlib.Algebra.Order.Floor.Div
 import Mathlib.Algebra.Order.Floor.Prime
 import Mathlib.Algebra.Order.Group.Abs
 import Mathlib.Algebra.Order.Group.Action
+import Mathlib.Algebra.Order.Group.Action.End
 import Mathlib.Algebra.Order.Group.Action.Synonym
 import Mathlib.Algebra.Order.Group.Basic
 import Mathlib.Algebra.Order.Group.Bounds

Mathlib/Algebra/Group/Action/End.lean

@@ -45,6 +45,9 @@ This is generalized to bundled endomorphisms by:
 * `RingHom.applyMulSemiringAction`
 * `RingAut.applyMulSemiringAction`
 * `AlgEquiv.applyMulSemiringAction`
+* `RelHom.applyMulAction`
+* `RelEmbedding.applyMulAction`
+* `RelIso.applyMulAction`
 -/
 instance applyMulAction : MulAction (Function.End α) α where
   smul := (· <| ·)

Mathlib/Algebra/Order/Group/Action/End.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Algebra.Group.Action.Faithful
+import Mathlib.Algebra.Order.Group.End
+import Mathlib.Order.RelIso.Basic
+
+/-!
+# Tautological action by relation automorphisms
+-/
+
+assert_not_exists MonoidWithZero
+
+namespace RelHom
+variable {α : Type*} {r : α → α → Prop}
+
+/-- The tautological action by `r →r r` on `α`. -/
+instance applyMulAction : MulAction (r →r r) α where
+  smul := (⇑)
+  one_smul _ := rfl
+  mul_smul _ _ _ := rfl
+
+@[simp] lemma smul_def (f : r →r r) (a : α) : f • a = f a := rfl
+
+instance apply_faithfulSMul : FaithfulSMul (r →r r) α where eq_of_smul_eq_smul h := RelHom.ext h
+
+end RelHom
+
+namespace RelEmbedding
+variable {α : Type*} {r : α → α → Prop}
+
+/-- The tautological action by `r ↪r r` on `α`. -/
+instance applyMulAction : MulAction (r ↪r r) α where
+  smul := (⇑)
+  one_smul _ := rfl
+  mul_smul _ _ _ := rfl
+
+@[simp] lemma smul_def (f : r ↪r r) (a : α) : f • a = f a := rfl
+
+instance apply_faithfulSMul : FaithfulSMul (r ↪r r) α where eq_of_smul_eq_smul h := ext h
+
+end RelEmbedding
+
+namespace RelIso
+variable {α : Type*} {r : α → α → Prop}
+
+/-- The tautological action by `r ≃r r` on `α`. -/
+instance applyMulAction : MulAction (r ≃r r) α where
+  smul := (⇑)
+  one_smul _ := rfl
+  mul_smul _ _ _ := rfl
+
+@[simp] lemma smul_def (f : r ≃r r) (a : α) : f • a = f a := rfl
+
+instance apply_faithfulSMul : FaithfulSMul (r ≃r r) α where eq_of_smul_eq_smul h := RelIso.ext h
+
+end RelIso

Mathlib/Algebra/Order/Group/End.lean

@@ -14,27 +14,65 @@ assert_not_exists MulAction MonoidWithZero
 
 variable {α : Type*} {r : α → α → Prop}
 
+namespace RelHom
+
+instance : Monoid (r →r r) where
+  one := .id r
+  mul := .comp
+  mul_assoc _ _ _ := rfl
+  one_mul _ := rfl
+  mul_one _ := rfl
+
+lemma one_def : (1 : r →r r) = .id r := rfl
+lemma mul_def (f g : r →r r) : (f * g) = f.comp g := rfl
+
+@[simp] lemma coe_one : ⇑(1 : r →r r) = id := rfl
+@[simp] lemma coe_mul (f g : r →r r) : ⇑(f * g) = f ∘ g := rfl
+
+lemma one_apply (a : α) : (1 : r →r r) a = a := rfl
+lemma mul_apply (e₁ e₂ : r →r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x) := rfl
+
+end RelHom
+
+namespace RelEmbedding
+
+instance : Monoid (r ↪r r) where
+  one := .refl r
+  mul f g := g.trans f
+  mul_assoc _ _ _ := rfl
+  one_mul _ := rfl
+  mul_one _ := rfl
+
+lemma one_def : (1 : r ↪r r) = .refl r := rfl
+lemma mul_def (f g : r ↪r r) : (f * g) = g.trans f := rfl
+
+@[simp] lemma coe_one : ⇑(1 : r ↪r r) = id := rfl
+@[simp] lemma coe_mul (f g : r ↪r r) : ⇑(f * g) = f ∘ g := rfl
+
+lemma one_apply (a : α) : (1 : r ↪r r) a = a := rfl
+lemma mul_apply (e₁ e₂ : r ↪r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x) := rfl
+
+end RelEmbedding
+
 namespace RelIso
 
 instance : Group (r ≃r r) where
-  one := RelIso.refl r
+  one := .refl r
   mul f₁ f₂ := f₂.trans f₁
-  inv := RelIso.symm
+  inv := .symm
   mul_assoc _ _ _ := rfl
   one_mul _ := ext fun _ => rfl
   mul_one _ := ext fun _ => rfl
   inv_mul_cancel f := ext f.symm_apply_apply
 
-@[simp]
-theorem coe_one : ((1 : r ≃r r) : α → α) = id :=
-  rfl
+lemma one_def : (1 : r ≃r r) = .refl r := rfl
+lemma mul_def (f g : r ≃r r) : (f * g) = g.trans f := rfl
 
-@[simp]
-theorem coe_mul (e₁ e₂ : r ≃r r) : ((e₁ * e₂) : α → α) = e₁ ∘ e₂ :=
-  rfl
+@[simp] lemma coe_one : ((1 : r ≃r r) : α → α) = id := rfl
+@[simp] lemma coe_mul (e₁ e₂ : r ≃r r) : ((e₁ * e₂) : α → α) = e₁ ∘ e₂ := rfl
 
-theorem mul_apply (e₁ e₂ : r ≃r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x) :=
-  rfl
+lemma one_apply (x : α) : (1 : r ≃r r) x = x := rfl
+lemma mul_apply (e₁ e₂ : r ≃r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x) := rfl
 
 @[simp]
 theorem inv_apply_self (e : r ≃r r) (x) : e⁻¹ (e x) = x :=