1 files changed, 99 insertions, 103 deletions

diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean
index 534759d..eb10b44 100644
--- a/Nominal/Basic.lean
+++ b/Nominal/Basic.lean
@@ -1,123 +1,125 @@
 import Mathlib.Tactic
+import Nominal.Permutations
+/-!
+# Basic Definitions
 
-section Permutations
+This file provides basic definitions for nominal sets.
+-/
 
-variable {X : Type}
+/-!
+## (FPerm 𝔸)-Sets
 
-notation "⸨" a "," b "⸩" => Equiv.swap a b
+Sets equipped with a permutation operation.
+-/
+section PermSet
 
--- 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}
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
-@[simp]
-theorem mem_support (π : Equiv.Perm X) (x : X) : x ∈ π.supp ↔ π x ≠ x := by
-  simp [Equiv.Perm.supp]
+/-- A set X equipped with a group action •: (FPerm 𝔸) × X → X. -/
+class PermSet (X : Type) extends MulAction (FPerm 𝔸) X
 
--- 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 set of atoms itself forms a G-Set. -/
+instance : PermSet 𝔸 𝔸 where
+  smul π a := π a
+  one_smul := by aesop
+  mul_smul := by aesop
 
--- 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 set of finite permutations forms a G-Set. -/
+instance : PermSet 𝔸 (FPerm 𝔸) where
+  smul π τ := π * τ
+  one_smul := by aesop
+  mul_smul := by aesop
 
--- 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
+/-- A discrete (FPerm 𝔸)-Set where permutations do not change anything. -/
+instance PermSet.discrete (X : Type) : PermSet 𝔸 X where
+  smul π x := x
+  one_smul := by aesop
+  mul_smul := by aesop
 
-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]
+/-- We consider Unit a discrete (FPerm 𝔸)-Set. -/
+instance : PermSet 𝔸 Unit := PermSet.discrete 𝔸 Unit
 
--- 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
+/-- We consider Bool a discrete (FPerm 𝔸)-Set. -/
+instance : PermSet 𝔸 Bool := PermSet.discrete 𝔸 Bool
 
-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]
+end PermSet
 
-lemma supp_mul_finite {π τ : Equiv.Perm X} (hπ : π ∈ FPerm X) (hτ : τ ∈ FPerm X) : (π * τ) ∈ FPerm X :=
-  (FPerm X).mul_mem hπ hτ
+/-!
+## Support Definitions
 
-lemma supp_inv_finite {π : Equiv.Perm X} (hπ : π ∈ FPerm X) : π⁻¹ ∈ FPerm X :=
-  (FPerm X).inv_mem hπ
+We can define the notion of "supports" on elements of (FPerm 𝔸)-Sets as the atoms which need to be left unchanged to also fix the element.
+-/
+section Support
 
--- Since FPerm is a subgroup of Perm, it is also a group.
-instance (X : Type) : Group (FPerm X) :=
-  Subgroup.toGroup (FPerm X)
+variable (𝔸 : Type) {X : Type} [PermSet 𝔸 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)
+namespace PermSet
 
-example : FPerm ℕ := ⟨⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩, by simp [supp_swap_finite, supp_mul_finite]⟩
+/-- The permutations that leave an element x unchanged. -/
+def fix' (x : X) : Set (FPerm 𝔸) :=
+  { π : FPerm 𝔸 | π • x = x }
 
-end Permutations
+/-- The permutations that leave all elements in A unchanged. -/
+def fix (A : Set X) : Set (FPerm 𝔸) :=
+  { π : FPerm 𝔸 | ∀ x ∈ A, π • x = x }
 
-section GSets
+/-- 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
 
-variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+@[simp]
+lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ fix 𝔸 S ⊆ fix' 𝔸 x := by
+  rfl
 
--- A G-set is a set X equipped with a group action •: (FPerm 𝔸) × X → X.
-class GSet (X : Type) extends MulAction (FPerm 𝔸) X
+lemma support_subset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ T → HasSupport 𝔸 x T := by
+  intro hS hsub π hπ
+  apply hS
+  intro a
+  aesop
 
-instance : GSet 𝔸 𝔸 where
-  smul π a := π a
-  one_smul := by aesop
-  mul_smul := by aesop
+lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by
+  sorry
 
-instance discreteGSet (X : Type) : GSet 𝔸 X where
-  smul π x := x
-  one_smul := by aesop
-  mul_smul := by aesop
+end PermSet
 
-instance : GSet 𝔸 Unit := discreteGSet 𝔸 Unit
-instance : GSet 𝔸 Bool := discreteGSet 𝔸 Bool
+end Support
 
-variable {X : Type} [GSet 𝔸 X]
+/-!
+## Basic Nominal Set Definition
 
--- The permutations that leave an element x unchanged.
-def fix' (x : X) : Set (FPerm 𝔸) :=
-  { π : FPerm 𝔸 | π • x = x }
+Nominal sets are then just G-Sets where all elements are finitely supported.
+-/
+section NominalSet
 
--- The permutations that leave all elements in A unchanged.
-def fix (A : Set X) : Set (FPerm 𝔸) :=
-  { π : FPerm 𝔸 | ∀ x ∈ A, π • x = x }
+variable (𝔸 : Type)
 
--- 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
+/-- A G-Set X is nominal if every x ∈ X is finitely supported. -/
+class NominalSet (X : Type) extends PermSet 𝔸 X where
+  finsupp : ∀ (x : X), ∃ (S : Set 𝔸), PermSet.HasSupport 𝔸 x S ∧ S.Finite
 
-end GSets
+namespace NominalSet
 
-section NominalSets
+variable {X : Type} [nom : NominalSet 𝔸 X]
 
-variable (𝔸 : Type)
+/-- 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 𝔸 | PermSet.HasSupport 𝔸 x S }
+
+/-- The least finite support in a nominal set is always finite. -/
+lemma supp_finite {x : X} : (supp 𝔸 x).Finite := by
+  unfold supp
+  obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.finsupp x
+  apply Set.Finite.subset
+  · exact hfinS
+  · grind
 
--- 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
+/-- The least finite support is itself a support. -/
+lemma supp_is_support {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := sorry
 
-instance : Nominal 𝔸 𝔸 where
+end NominalSet
+
+/-- The set of atoms is a nominal set, where supp a = {a}. -/
+instance : NominalSet 𝔸 𝔸 where
   finsupp := by
     intro a
     use {a}
@@ -126,7 +128,10 @@ instance : Nominal 𝔸 𝔸 where
       aesop
     · simp
 
-instance discreteNominal (X : Type) : Nominal 𝔸 X where
+-- TODO: Prove supp a = {a}
+
+/-- Every set can be made into a discrete nominal set where every element has empty support. -/
+instance NominalSet.discrete (X : Type) : NominalSet 𝔸 X where
   finsupp := by
     intro x
     use {}
@@ -135,21 +140,12 @@ instance discreteNominal (X : Type) : Nominal 𝔸 X where
       aesop
     · simp
 
-instance : Nominal 𝔸 Unit := discreteNominal 𝔸 Unit
-instance : Nominal 𝔸 Bool := discreteNominal 𝔸 Bool
-
-variable {X : Type} [nom : Nominal 𝔸 X]
+-- TODO: Prove supp 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 }
+/-- We consider Unit a discrete nominal set. -/
+instance : NominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit
 
--- 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
+/-- We consider Bool a discrete nominal set. -/
+instance : NominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool
 
-end NominalSets
+end NominalSet