restructure

1 files changed, 91 insertions, 0 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 ⟨hsuppS, hfinS⟩
+      by_contra ha
+      obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset ({a} ∪ hfinS.toFinset)
+      simp at hc
+      have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by
+        intro d hd
+        rw [show ⸨a,c⸩ • d = (Equiv.swap a c) d from rfl]
+        apply Equiv.Perm.supp_notin
+        simp [Equiv.Perm.supp_swap, Ne.symm hc.left]
+        exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩
+      have ha₁ : ⸨a, c⸩ • a = c := by
+        simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl]
+      have ha₂ : ⸨a, 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