more wip

1 files changed, 35 insertions, 0 deletions

diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index 0d6b81c..bc775b9 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -202,4 +202,39 @@ instance {X : Type} [PermSet 𝔸 X] : PermSet 𝔸 (Set X) where
 /-- Simplification for swaps applied to an atom. -/
 @[simp] lemma PermSet.atom_swap {a b c : 𝔸} : ⸨a, b⸩ • c = (Equiv.swap a b) c := by rfl
 
+/-- Given x = (a b) y, we also know y = (a b) x. -/
+lemma PermSet.swap_switch {X : Type} [PermSet 𝔸 X] {a b : 𝔸} {x y : X} : x = ⸨a, b⸩ • y → y = ⸨a, b⸩ • x := by
+  intro h
+  have h' : ⸨a, b⸩ • x = ⸨a, b⸩ • ⸨a, b⸩ • y := by congr
+  rw [← mul_smul, FPerm.swap_mul_self, one_smul] at h'
+  exact h'.symm
+
+/-- If the element is not affected by the swap, membership of it is the same as before the swap. -/
+lemma PermSet.atom_set_swap_ne_ne {a b c : 𝔸} {S : Set 𝔸} : c ≠ a → c ≠ b → (c ∈ S ↔ c ∈ ⸨a, b⸩ • S) := by
+  intro ha hb
+  constructor
+  · intro h
+    rw [← FPerm.swap_apply_of_ne_of_ne ha hb]
+    exact Set.smul_mem_smul_set h
+  · intro h
+    have h' : ⸨a, b⸩ c ∈ ⸨a, b⸩ • ⸨a, b⸩ • S := Set.smul_mem_smul_set h
+    rw [FPerm.swap_apply_of_ne_of_ne ha hb, ← mul_smul, FPerm.swap_mul_self, one_smul] at h'
+    exact h'
+
+/-- If an element is swapped, its membership is exactly that of the other element in the swapped set. -/
+lemma PermSet.atom_set_swap_left {a b : 𝔸} {S : Set 𝔸} : a ∈ S ↔ b ∈ ⸨a, b⸩ • S := by
+  constructor
+  · intro h
+    have h' : ⸨a, b⸩ a ∈ ⸨a, b⸩ • S := Set.smul_mem_smul_set h
+    rw [FPerm.swap_apply_left] at h'
+    exact h'
+  · intro h
+    have h' : ⸨a, b⸩ b ∈ ⸨a, b⸩ • ⸨a, b⸩ • S := Set.smul_mem_smul_set h
+    rw [FPerm.swap_apply_right, ← mul_smul, FPerm.swap_mul_self, one_smul] at h'
+    exact h'
+
+/-- If an element is swapped, its membership is exactly that of the other element in the swapped set. -/
+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]
+
 end PermSet