restructure

1 files changed, 32 insertions, 8 deletions

diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index 5f62ec0..6819c67 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -103,15 +103,14 @@ namespace Equiv.Perm
 
 /-- The support of a transposition (x y). -/
 lemma supp_swap {x y : X} : (Equiv.swap x y).supp = if x ≠ y then {x, y} else ∅ := by
-  if h : (x ≠ y) then
-    ext z
+  by_cases h : x = y
+  · simp [h, supp]
+  · simp [h]; ext z
     by_cases hx : z = x
-    · aesop
+    · simp [hx, Ne.symm h]
     · by_cases hy : z = y
-      · simp [hy]
+      · simp [hy, h]
       · simp [Equiv.swap_apply_of_ne_of_ne, hx, hy]
-  else
-    aesop
 
 end Equiv.Perm
 
@@ -120,8 +119,7 @@ namespace FPerm
 def swap (x y : X) : FPerm X := ⟨Equiv.swap x y, by
   apply Set.Finite.subset
   · apply ({x, y} : Finset X).finite_toSet
-  · simp [Equiv.Perm.supp_swap]
-    aesop⟩
+  · by_cases h : x = y <;> all_goals simp [Equiv.Perm.supp_swap, h]⟩
 
 notation "⸨" a "," b "⸩" => FPerm.swap a b
 
@@ -130,3 +128,29 @@ end FPerm
 example : FPerm ℕ := ⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩
 
 end Transposition
+
+/-!
+## (FPerm 𝔸)-Sets
+
+Sets equipped with a permutation operation.
+-/
+section PermSet
+
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+
+/-- A set X equipped with a group action •: (FPerm 𝔸) × X → X. -/
+class PermSet (X : Type) extends MulAction (FPerm 𝔸) X
+
+/-- The set of atoms itself forms a (FPerm 𝔸)-Set. -/
+instance : PermSet 𝔸 𝔸 where
+  smul π a := π a
+  one_smul := by intro; rfl
+  mul_smul := by intro _ _ _; rfl
+
+/-- The set of finite permutations forms a (FPerm 𝔸)-Set. -/
+instance : PermSet 𝔸 (FPerm 𝔸) where
+  smul π τ := π * τ
+  one_smul := by intro; rfl
+  mul_smul := by intro _ _ _; rfl
+
+end PermSet