fs constructions

1 files changed, 12 insertions, 0 deletions

diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index f1115d3..6119df3 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -259,4 +259,16 @@ lemma PermSet.atom_set_swap_left {a b : 𝔸} {S : Set 𝔸} : a ∈ S ↔ b ∈
 lemma PermSet.atom_set_swap_right {a b : 𝔸} {S : Set 𝔸} : b ∈ S ↔ a ∈ ⸨a, b⸩ • S := by
   rw [FPerm.swap_comm, atom_set_swap_left]
 
+instance {X Y : Type} [SMul (FPerm 𝔸) X] [SMul (FPerm 𝔸) Y] : SMul (FPerm 𝔸) (X → Y) where
+  smul π f := fun x ↦ π • f (π⁻¹ • x)
+
+@[simp] lemma PermSet.smul_function {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] (π : FPerm 𝔸)
+    (f : X → Y) (x : X) : (π • f) x = π • f (π⁻¹ • x) :=
+  rfl
+
+/-- Functions between (FPerm 𝔸)-sets form (FPerm 𝔸)-sets with (π • f) x = π • f (π⁻¹ • x). -/
+instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X → Y) where
+  one_smul f := by ext x; simp
+  mul_smul π τ f := by ext x; simp [mul_smul]
+
 end PermSet