restructure

3 files changed, 139 insertions, 123 deletions

diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean
new file mode 100644
index 0000000..793baa4
--- /dev/null
+++ b/Nominal/Instances.lean
@@ -0,0 +1,91 @@
+import Nominal.Permutations
+import Nominal.Support
+
+/-!
+# Instances
+
+This file contains common instances of (FPerm 饾敻)-sets and nominal sets.
+-/
+
+variable (饾敻 : Type)
+
+/-!
+## Atoms
+
+The set 饾敻 of atoms itself is a nominal set, where supp a = {a}.
+-/
+section Atoms
+
+private lemma NominalSet.supp_atoms' {a : 饾敻} : PermSet.HasSupport 饾敻 a {a} := by
+  simp [PermSet.HasSupport, PermSet.fix, PermSet.fix']
+
+instance : NominalSet 饾敻 饾敻 where
+  fin_supp := by
+    intro a
+    use {a}
+    constructor
+    路 exact NominalSet.supp_atoms' 饾敻
+    路 simp
+
+lemma NominalSet.supp_atoms [Infinite 饾敻] [DecidableEq 饾敻] {a : 饾敻} : supp 饾敻 a = {a} := by
+  ext b; constructor
+  路 apply support_subset_supp
+    路 apply NominalSet.supp_atoms'
+    路 simp
+  路 suffices : a 鈭� supp 饾敻 a
+    路 simp; intro h; rw [h]; assumption
+    路 intro S 鉄╤suppS, hfinS鉄�
+      by_contra ha
+      obtain 鉄╟, hc鉄� := Infinite.exists_notMem_finset ({a} 鈭� hfinS.toFinset)
+      simp at hc
+      have hfix : 飧╝, c飧� 鈭� PermSet.fix 饾敻 S := by
+        intro d hd
+        rw [show 飧╝,c飧� 鈥� d = (Equiv.swap a c) d from rfl]
+        apply Equiv.Perm.supp_notin
+        simp [Equiv.Perm.supp_swap, Ne.symm hc.left]
+        exact 鉄╪e_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right鉄�
+      have ha鈧� : 飧╝, c飧� 鈥� a = c := by
+        simp [show 飧╝,c飧� 鈥� a = (Equiv.swap a c) a from rfl]
+      have ha鈧� : 飧╝, c飧� 鈥� a = a := by
+        specialize hsuppS hfix
+        simpa [PermSet.fix']
+      rw [ha鈧乚 at ha鈧�
+      exact hc.left ha鈧�
+
+end Atoms
+
+/-!
+## Discrete Nominal Sets
+
+Every set can be made into a discrete nominal set, where supp x = 鈭�.
+-/
+section Discrete
+
+def NominalSet.discrete (X : Type) : DiscreteNominalSet 饾敻 X where
+  smul 蟺 x := x
+  one_smul := by intro; rfl
+  mul_smul := by intro _ _ _; rfl
+  is_discrete := by intro _ _; rfl
+  fin_supp := by
+    intro x
+    use {}
+    constructor
+    路 intro 蟺 h蟺; simp [PermSet.fix']; rfl
+    路 simp
+
+lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 饾敻 X] {x : X} : supp 饾敻 x = 鈭� := by
+  rw [鈫� Set.subset_empty_iff]
+  apply Set.sInter_subset_of_mem
+  constructor
+  路 intro 蟺 h蟺
+    simp [PermSet.fix']
+    exact DiscreteNominalSet.is_discrete x 蟺
+  路 exact Set.finite_empty
+
+/-- We consider Unit a discrete nominal set. -/
+instance : DiscreteNominalSet 饾敻 Unit := NominalSet.discrete 饾敻 Unit
+
+/-- We consider Bool a discrete nominal set. -/
+instance : DiscreteNominalSet 饾敻 Bool := NominalSet.discrete 饾敻 Bool
+
+end Discrete
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index 5f62ec0..6819c67 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -103,15 +103,14 @@ namespace Equiv.Perm
 
 /-- The support of a transposition (x y). -/
 lemma supp_swap {x y : X} : (Equiv.swap x y).supp = if x 鈮� y then {x, y} else 鈭� := by
-  if h : (x 鈮� y) then
-    ext z
+  by_cases h : x = y
+  路 simp [h, supp]
+  路 simp [h]; ext z
     by_cases hx : z = x
-    路 aesop
+    路 simp [hx, Ne.symm h]
     路 by_cases hy : z = y
-      路 simp [hy]
+      路 simp [hy, h]
       路 simp [Equiv.swap_apply_of_ne_of_ne, hx, hy]
-  else
-    aesop
 
 end Equiv.Perm
 
@@ -120,8 +119,7 @@ namespace FPerm
 def swap (x y : X) : FPerm X := 鉄‥quiv.swap x y, by
   apply Set.Finite.subset
   路 apply ({x, y} : Finset X).finite_toSet
-  路 simp [Equiv.Perm.supp_swap]
-    aesop鉄�
+  路 by_cases h : x = y <;> all_goals simp [Equiv.Perm.supp_swap, h]鉄�
 
 notation "飧�" a "," b "飧�" => FPerm.swap a b
 
@@ -130,3 +128,29 @@ end FPerm
 example : FPerm 鈩� := 飧�1, 2飧� * 飧�3, 4飧� * 飧�2, 3飧�
 
 end Transposition
+
+/-!
+## (FPerm 饾敻)-Sets
+
+Sets equipped with a permutation operation.
+-/
+section PermSet
+
+variable (饾敻 : Type) [Infinite 饾敻] [Countable 饾敻] [DecidableEq 饾敻]
+
+/-- A set X equipped with a group action 鈥�: (FPerm 饾敻) 脳 X 鈫� X. -/
+class PermSet (X : Type) extends MulAction (FPerm 饾敻) X
+
+/-- The set of atoms itself forms a (FPerm 饾敻)-Set. -/
+instance : PermSet 饾敻 饾敻 where
+  smul 蟺 a := 蟺 a
+  one_smul := by intro; rfl
+  mul_smul := by intro _ _ _; rfl
+
+/-- The set of finite permutations forms a (FPerm 饾敻)-Set. -/
+instance : PermSet 饾敻 (FPerm 饾敻) where
+  smul 蟺 蟿 := 蟺 * 蟿
+  one_smul := by intro; rfl
+  mul_smul := by intro _ _ _; rfl
+
+end PermSet
diff --git a/Nominal/Basic.lean b/Nominal/Support.lean
index 66f43b1..7875ad3 100644
--- a/Nominal/Basic.lean
+++ b/Nominal/Support.lean
@@ -1,53 +1,14 @@
 import Mathlib.Tactic
 import Nominal.Permutations
 import Nominal.Helpers.Finset
-/-!
-# Basic Definitions
-
-This file provides basic definitions for nominal sets.
--/
 
 /-!
-## (FPerm 饾敻)-Sets
+# Support
 
-Sets equipped with a permutation operation.
+This file provides basic definitions for support of (FPerm 饾敻)-sets and nominal sets.
 -/
-section PermSet
-
-variable (饾敻 : Type) [Infinite 饾敻] [Countable 饾敻] [DecidableEq 饾敻]
 
-/-- A set X equipped with a group action 鈥�: (FPerm 饾敻) 脳 X 鈫� X. -/
-class PermSet (X : Type) extends MulAction (FPerm 饾敻) X
-
-/-- The set of atoms itself forms a (FPerm 饾敻)-Set. -/
-instance : PermSet 饾敻 饾敻 where
-  smul 蟺 a := 蟺 a
-  one_smul := by intro; rfl
-  mul_smul := by intro _ _ _; rfl
-
-/-- The set of finite permutations forms a (FPerm 饾敻)-Set. -/
-instance : PermSet 饾敻 (FPerm 饾敻) where
-  smul 蟺 蟿 := 蟺 * 蟿
-  one_smul := by intro; rfl
-  mul_smul := by intro _ _ _; rfl
-
-class DiscretePermSet (X : Type) extends PermSet 饾敻 X where
-  is_discrete : 鈭� (x : X) (蟺 : FPerm 饾敻), 蟺 鈥� x = x
-
-/-- A discrete (FPerm 饾敻)-Set where permutations do not change anything. -/
-def PermSet.discrete (X : Type) : DiscretePermSet 饾敻 X where
-  smul 蟺 x := x
-  one_smul := by intro; rfl
-  mul_smul := by intro _ _ _; rfl
-  is_discrete := by intro _ _; rfl
-
-/-- We consider Unit a discrete (FPerm 饾敻)-Set. -/
-instance : DiscretePermSet 饾敻 Unit := PermSet.discrete 饾敻 Unit
-
-/-- We consider Bool a discrete (FPerm 饾敻)-Set. -/
-instance : DiscretePermSet 饾敻 Bool := PermSet.discrete 饾敻 Bool
-
-end PermSet
+variable (饾敻 : Type)
 
 /-!
 ## Support Definitions
@@ -56,7 +17,7 @@ We can define the notion of "supports" on elements of (FPerm 饾敻)-Sets as the a
 -/
 section Support
 
-variable (饾敻 : Type) {X : Type} [PermSet 饾敻 X]
+variable {X : Type} [PermSet 饾敻 X]
 
 namespace PermSet
 
@@ -72,7 +33,7 @@ def fix (A : Set X) : Set (FPerm 饾敻) :=
 def HasSupport (x : X) (S : Set 饾敻) : Prop :=
   fix 饾敻 S 鈯� fix' 饾敻 x
 
-@[simp]
+/-- Alternative definition with fix 饾敻 S unfolded. -/
 lemma support_iff {x : X} {S : Set 饾敻} : HasSupport 饾敻 x S 鈫� 鈭� (蟺 : FPerm 饾敻), (鈭� x 鈭� S, 蟺 x = x) 鈫� 蟺 鈭� fix' 饾敻 x := by
   constructor
   路 intro hsupp 蟺 h蟺
@@ -80,7 +41,8 @@ lemma support_iff {x : X} {S : Set 饾敻} : HasSupport 饾敻 x S 鈫� 鈭� (蟺 : FPe
   路 intro hsupp 蟺 h蟺
     exact hsupp 蟺 h蟺
 
-lemma support_subset {x : X} {S T : Set 饾敻} : HasSupport 饾敻 x S 鈫� S 鈯� T 鈫� HasSupport 饾敻 x T := by
+/-- If a support is a subset of another set, that set is also a support.  -/
+lemma support_superset {x : X} {S T : Set 饾敻} : HasSupport 饾敻 x S 鈫� S 鈯� T 鈫� HasSupport 饾敻 x T := by
   intro hS hsub 蟺 h蟺
   apply hS
   intro a ha
@@ -229,7 +191,7 @@ end PermSet
 end Support
 
 /-!
-## Basic Nominal Set Definition
+## Nominal Sets
 
 Nominal sets are then just (FPerm 饾敻)-Sets where all elements are finitely supported.
 -/
@@ -239,7 +201,11 @@ variable (饾敻 : Type)
 
 /-- An (FPerm 饾敻)-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
+  fin_supp : 鈭� (x : X), 鈭� (S : Set 饾敻), PermSet.HasSupport 饾敻 x S 鈭� S.Finite
+
+/-- A discrete nominal set where permutations do not change anything. -/
+class DiscreteNominalSet (X : Type) extends NominalSet 饾敻 X where
+  is_discrete : 鈭� (x : X) (蟺 : FPerm 饾敻), 蟺 鈥� x = x
 
 namespace NominalSet
 
@@ -252,14 +218,14 @@ def supp (x : X) : Set 饾敻 :=
 /-- The least finite support in a nominal set is always finite. -/
 lemma supp_finite {x : X} : (supp 饾敻 x).Finite := by
   unfold supp
-  obtain 鉄⊿, 鉄╤suppS, hfinS鉄┾煩 := nom.finsupp x
+  obtain 鉄⊿, 鉄╤suppS, hfinS鉄┾煩 := nom.fin_supp x
   apply Set.Finite.subset
   路 exact hfinS
   路 grind
 
 /-- The least finite support is itself a support. -/
 lemma supp_is_support [Infinite 饾敻] {x : X} : PermSet.HasSupport 饾敻 x (supp 饾敻 x) := by
-  obtain 鉄⊿, 鉄╤suppS, hfinS鉄┾煩 := nom.finsupp x
+  obtain 鉄⊿, 鉄╤suppS, hfinS鉄┾煩 := nom.fin_supp x
   have suppf : (supp 饾敻 x = 鈰傗個 { T : Set 饾敻 | T 鈯� S 鈭� PermSet.HasSupport 饾敻 x T 鈭� T.Finite }) := by
     unfold supp; ext a
     constructor
@@ -287,6 +253,7 @@ lemma supp_is_support [Infinite 饾敻] {x : X} : PermSet.HasSupport 饾敻 x (supp
   路 intro T hT
     exact hT.right
 
+/-- If S is a finite support for x, then supp x is a subset of it. -/
 lemma support_subset_supp {x : X} {S : Set 饾敻} : PermSet.HasSupport 饾敻 x S 鈫� S.Finite 鈫� supp 饾敻 x 鈯� S := by
   intro hsupp hfin
   apply Set.sInter_subset_of_mem
@@ -294,70 +261,4 @@ lemma support_subset_supp {x : X} {S : Set 饾敻} : PermSet.HasSupport 饾敻 x S �
 
 end NominalSet
 
-private lemma NominalSet.supp_atoms' {a : 饾敻} : PermSet.HasSupport 饾敻 a {a} := by
-  simp [PermSet.fix']
-
-/-- The set of atoms is a nominal set, where supp a = {a}. -/
-instance : NominalSet 饾敻 饾敻 where
-  finsupp := by
-    intro a
-    use {a}
-    constructor
-    路 exact NominalSet.supp_atoms' 饾敻
-    路 simp
-
-lemma NominalSet.supp_atoms [Infinite 饾敻] [DecidableEq 饾敻] {a : 饾敻} : supp 饾敻 a = {a} := by
-  ext b; constructor
-  路 apply support_subset_supp
-    路 apply NominalSet.supp_atoms'
-    路 simp
-  路 suffices : a 鈭� supp 饾敻 a
-    路 simp; intro h; rw [h]; assumption
-    路 intro S 鉄╤suppS, hfinS鉄�
-      by_contra ha
-      obtain 鉄╟, hc鉄� := Infinite.exists_notMem_finset ({a} 鈭� hfinS.toFinset)
-      simp at hc
-      have hfix : 飧╝, c飧� 鈭� PermSet.fix 饾敻 S := by
-        intro d hd
-        rw [show 飧╝,c飧� 鈥� d = (Equiv.swap a c) d from rfl]
-        apply Equiv.Perm.supp_notin
-        simp [Equiv.Perm.supp_swap, Ne.symm hc.left]
-        exact 鉄╪e_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right鉄�
-      have ha鈧� : 飧╝, c飧� 鈥� a = c := by
-        simp [show 飧╝,c飧� 鈥� a = (Equiv.swap a c) a from rfl]
-      have ha鈧� : 飧╝, c飧� 鈥� a = a := by
-        specialize hsuppS hfix
-        simpa [PermSet.fix']
-      rw [ha鈧乚 at ha鈧�
-      exact hc.left ha鈧�
-
-class DiscreteNominalSet (X : Type) extends NominalSet 饾敻 X, DiscretePermSet 饾敻 X
-
-private lemma NominalSet.supp_discrete' {X : Type} [disc : DiscretePermSet 饾敻 X] {x : X} : PermSet.HasSupport 饾敻 x 鈭� := by
-  intro 蟺 h蟺
-  simp [PermSet.fix']
-  exact DiscretePermSet.is_discrete x 蟺
-
-/-- Every set can be made into a discrete nominal set where every element has empty support. -/
-def NominalSet.discrete (X : Type) : DiscreteNominalSet 饾敻 X :=
-{ PermSet.discrete 饾敻 X with
-  finsupp := by
-    intro x
-    use {}
-    constructor
-    路 intro 蟺 h蟺; simp [PermSet.fix']; rfl
-    路 simp
-}
-
-lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 饾敻 X] {x : X} : supp 饾敻 x = 鈭� := by
-  rw [鈫� Set.subset_empty_iff]
-  apply Set.sInter_subset_of_mem
-  exact 鉄∟ominalSet.supp_discrete' 饾敻, Set.finite_empty鉄�
-
-/-- We consider Unit a discrete nominal set. -/
-instance : DiscreteNominalSet 饾敻 Unit := NominalSet.discrete 饾敻 Unit
-
-/-- We consider Bool a discrete nominal set. -/
-instance : DiscreteNominalSet 饾敻 Bool := NominalSet.discrete 饾敻 Bool
-
 end NominalSet