1 files changed, 80 insertions, 6 deletions
diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean
index dca31e2..534759d 100644
--- a/Nominal/Basic.lean
+++ b/Nominal/Basic.lean
@@ -65,17 +65,91 @@ lemma supp_inv_finite {π : Equiv.Perm X} (hπ : π ∈ FPerm X) : π⁻¹ ∈ F
 instance (X : Type) : Group (FPerm X) :=
   Subgroup.toGroup (FPerm X)
 
+-- Since FPerm is a subset of Perm, we can coerce it into a function.
+instance (X : Type) : CoeFun (FPerm X) (fun _ => X → X) where
+  coe π := (↑π : Equiv.Perm X)
+
 example : FPerm ℕ := ⟨⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩, by simp [supp_swap_finite, supp_mul_finite]⟩
 
 end Permutations
 
-section BasicDefinitions
+section GSets
+
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+
+-- A G-set is a set X equipped with a group action •: (FPerm 𝔸) × X → X.
+class GSet (X : Type) extends MulAction (FPerm 𝔸) X
+
+instance : GSet 𝔸 𝔸 where
+  smul π a := π a
+  one_smul := by aesop
+  mul_smul := by aesop
+
+instance discreteGSet (X : Type) : GSet 𝔸 X where
+  smul π x := x
+  one_smul := by aesop
+  mul_smul := by aesop
+
+instance : GSet 𝔸 Unit := discreteGSet 𝔸 Unit
+instance : GSet 𝔸 Bool := discreteGSet 𝔸 Bool
+
+variable {X : Type} [GSet 𝔸 X]
+
+-- The permutations that leave an element x unchanged.
+def fix' (x : X) : Set (FPerm 𝔸) :=
+  { π : FPerm 𝔸 | π • x = x }
+
+-- The permutations that leave all elements in A unchanged.
+def fix (A : Set X) : Set (FPerm 𝔸) :=
+  { π : FPerm 𝔸 | ∀ x ∈ A, π • x = x }
+
+-- A set S ⊆ 𝔸 is a support for x if every permutation that fixes S also leaves x unchanged.
+def HasSupport (x : X) (S : Set 𝔸) : Prop :=
+  fix 𝔸 S ⊆ fix' 𝔸 x
+
+end GSets
+
+section NominalSets
+
+variable (𝔸 : Type)
+
+-- A G-Set X is nominal if every x ∈ X is finitely supported.
+class Nominal (X : Type) extends GSet 𝔸 X where
+  finsupp : ∀ (x : X), ∃ (S : Set 𝔸), HasSupport 𝔸 x S ∧ S.Finite
+
+instance : Nominal 𝔸 𝔸 where
+  finsupp := by
+    intro a
+    use {a}
+    constructor
+    · intro π hπ
+      aesop
+    · simp
+
+instance discreteNominal (X : Type) : Nominal 𝔸 X where
+  finsupp := by
+    intro x
+    use {}
+    constructor
+    · intro π hπ
+      aesop
+    · simp
+
+instance : Nominal 𝔸 Unit := discreteNominal 𝔸 Unit
+instance : Nominal 𝔸 Bool := discreteNominal 𝔸 Bool
 
-variable (𝔸: Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+variable {X : Type} [nom : Nominal 𝔸 X]
 
-class GSet (X : Type u) : Type (u + 1) where
-  action : MulAction (FPerm 𝔸) X
+-- For every element x of a nominal set, there exists a least finite support, denoted "supp x".
+noncomputable def supp (x : X) : Set 𝔸 :=
+  ⋂₀ { S : Set 𝔸 | HasSupport 𝔸 x S }
 
-class Nominal (X : Type u) : Type (u + 1) extends (GSet 𝔸 X) where
+-- The least finite support in a nominal set is always finite.
+theorem supp_finite (x : X) : (supp 𝔸 x).Finite := by
+  unfold supp
+  obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.finsupp x
+  apply Set.Finite.subset
+  · exact hfinS
+  · grind
 
-end BasicDefinitions
+end NominalSets