further work

1 files changed, 127 insertions, 0 deletions

diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
new file mode 100644
index 0000000..40f0f13
--- /dev/null
+++ b/Nominal/Permutations.lean
@@ -0,0 +1,127 @@
+import Mathlib.Tactic
+
+/-!
+# Finitely supported permutations
+
+This file defines `FPerm`, the subgroup of permutations with finite support.
+It also provides basic lemmas about permutation supports and transpositions.
+-/
+
+/-!
+## Support Definition
+
+Support is defined on Equiv.Perm which also includes infinitely supported permutations.
+-/
+section Support
+
+variable {X : Type}
+
+namespace Equiv.Perm
+
+/--
+The support of a permutation; i.e., the set of elements the permutation actually changes.
+
+Note that, while there is an Equiv.Perm.support, it only works for finite types and thus finite supports.
+-/
+def supp (π : Equiv.Perm X) : Set X :=
+  {x | π x ≠ x}
+
+@[simp]
+theorem mem_supp (π : Equiv.Perm X) (x : X) : x ∈ π.supp ↔ π x ≠ x := by rfl
+
+/-- The support of the identity function is the empty set. -/
+lemma supp_one : (1 : Equiv.Perm X).supp = ∅ := by
+  rw [Set.eq_empty_iff_forall_notMem]
+  intro x hx
+  contradiction
+
+/-- The support of the inverse function is the same as the function's support. -/
+lemma supp_inv (π : Equiv.Perm X) : π⁻¹.supp = π.supp := by
+  simp [supp, set_support_inv_eq]
+
+/-- The support of two concatenated permutations is a subset of the individual supports as a union. -/
+lemma supp_mul_subset (π τ : Equiv.Perm X) : (π * τ).supp ⊆ π.supp ∪ τ.supp := by
+  simp [supp]
+  apply set_support_mul_subset
+
+end Equiv.Perm
+
+end Support
+
+/-!
+## FPerm Group
+
+The FPerm group is the subgroup of finitely supported permutations.
+-/
+section Subgroup
+
+/-- The group of (finitely supported) permutations. -/
+def FPerm (X : Type) : Subgroup (Equiv.Perm X) where
+  carrier := {π | π.supp.Finite}
+  mul_mem' {π τ} hπ hτ := by
+    apply (hπ.union hτ).subset
+    exact Equiv.Perm.supp_mul_subset π τ
+  one_mem' := by
+    simp [Equiv.Perm.supp_one]
+  inv_mem' {x} hx := by
+    simp [Equiv.Perm.supp_inv]
+    exact hx
+
+variable {X : Type}
+
+namespace FPerm
+
+lemma mem_mul {π τ : Equiv.Perm X} (hπ : π ∈ FPerm X) (hτ : τ ∈ FPerm X) : (π * τ) ∈ FPerm X :=
+  (FPerm X).mul_mem hπ hτ
+
+lemma mem_inv {π : Equiv.Perm X} (hπ : π ∈ FPerm X) : π⁻¹ ∈ FPerm X :=
+  (FPerm X).inv_mem hπ
+
+end FPerm
+
+/-- Since FPerm is a subset of Equiv.Perm, we can coerce it into a function. -/
+instance (X : Type) : CoeFun (FPerm X) (fun _ => X → X) where
+  coe π := (↑π : Equiv.Perm X)
+
+end Subgroup
+
+/-!
+## Transpositions
+
+Transpositions are a special case of finite permutations, where only (at most) two elements are swapped.
+-/
+section Transposition
+
+notation "⸨" a "," b "⸩" => Equiv.swap a b
+
+variable {X : Type} [DecidableEq X]
+
+namespace Equiv.Perm
+
+/-- The support of a transposition (x y). -/
+lemma supp_swap{x y : X} : ⸨x, y⸩.supp = if x ≠ y then {x, y} else ∅ := by
+  if h : (x ≠ y) then
+    ext z
+    by_cases hx : z = x
+    · aesop
+    · by_cases hy : z = y
+      · simp [hy]
+      · simp [Equiv.swap_apply_of_ne_of_ne, hx, hy]
+  else
+    aesop
+
+end Equiv.Perm
+
+namespace FPerm
+
+lemma mem_swap {x y : X} : ⸨x, y⸩ ∈ FPerm X := by
+  apply Set.Finite.subset
+  · apply ({x, y} : Finset X).finite_toSet
+  · simp [Equiv.Perm.supp_swap]
+    aesop
+
+end FPerm
+
+example : FPerm ℕ := ⟨⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩, by simp [FPerm.mem_swap, FPerm.mem_mul]⟩
+
+end Transposition