1 files changed, 81 insertions, 1 deletions
diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean
index 99415d9..dca31e2 100644
--- a/Nominal/Basic.lean
+++ b/Nominal/Basic.lean
@@ -1 +1,81 @@
-def hello := "world"
+import Mathlib.Tactic
+
+section Permutations
+
+variable {X : Type}
+
+notation "⸨" a "," b "⸩" => Equiv.swap a b
+
+-- The support of a permutation; i.e., the set of elements where the permutation actually maps the element to a different one.
+def Equiv.Perm.supp (π : Equiv.Perm X) : Set X :=
+  {x | π x ≠ x}
+
+@[simp]
+theorem mem_support (π : Equiv.Perm X) (x : X) : x ∈ π.supp ↔ π x ≠ x := by
+  simp [Equiv.Perm.supp]
+
+-- 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 [Equiv.Perm.supp, Equiv.Perm.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 [Equiv.Perm.supp]
+  apply Equiv.Perm.set_support_mul_subset
+
+lemma supp_swap [DecidableEq X] {x y : X} (h : x ≠ y) : ⸨x, y⸩.supp = {x, y} := by
+  ext z
+  by_cases hx : z = x
+  · simpa [hx] using h.symm
+  · by_cases hy : z = y
+    · simpa [Equiv.swap_apply_of_ne_of_ne, hx, hy] using h
+    · simp [Equiv.swap_apply_of_ne_of_ne, hx, hy]
+
+-- 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 supp_mul_subset π τ
+  one_mem' := by
+    simp [supp_one]
+  inv_mem' {x} hx := by
+    simp [supp_inv]
+    exact hx
+
+lemma supp_swap_finite [DecidableEq X] (x y : X) : ⸨x, y⸩ ∈ FPerm X := by
+  by_cases hx : x = y
+  · rw [<-Equiv.swap_eq_one_iff] at hx
+    simp [hx]
+  · simp [FPerm, supp_swap hx]
+
+lemma supp_mul_finite {π τ : Equiv.Perm X} (hπ : π ∈ FPerm X) (hτ : τ ∈ FPerm X) : (π * τ) ∈ FPerm X :=
+  (FPerm X).mul_mem hπ hτ
+
+lemma supp_inv_finite {π : Equiv.Perm X} (hπ : π ∈ FPerm X) : π⁻¹ ∈ FPerm X :=
+  (FPerm X).inv_mem hπ
+
+-- Since FPerm is a subgroup of Perm, it is also a group.
+instance (X : Type) : Group (FPerm X) :=
+  Subgroup.toGroup (FPerm X)
+
+example : FPerm ℕ := ⟨⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩, by simp [supp_swap_finite, supp_mul_finite]⟩
+
+end Permutations
+
+section BasicDefinitions
+
+variable (𝔸: Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+
+class GSet (X : Type u) : Type (u + 1) where
+  action : MulAction (FPerm 𝔸) X
+
+class Nominal (X : Type u) : Type (u + 1) extends (GSet 𝔸 X) where
+
+end BasicDefinitions