1 files changed, 206 insertions, 0 deletions
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
new file mode 100644
index 0000000..19b8566
--- /dev/null
+++ b/Nominal/Instances/Basic.lean
@@ -0,0 +1,206 @@
+import Mathlib
+import Nominal.Support
+import Nominal.Equivariance
+
+/-!
+# Basic Nominal Sets
+
+This file contains common instances of nominal sets and their smallest supports.
+-/
+
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+
+/-!
+## Atoms
+
+The set 𝔸 of atoms itself is a nominal set, where supp a = {a}.
+-/
+section Atoms
+
+private lemma NominalSet.supp_atom' {a : 𝔸} : PermSet.HasSupport 𝔸 a {a} := by
+  simp [PermSet.HasSupport, PermSet.fix, PermSet.fix']
+
+instance : NominalSet 𝔸 𝔸 where
+  fin_supp := by
+    intro a; use {a}
+    exact ⟨NominalSet.supp_atom' 𝔸, Set.finite_singleton a⟩
+
+@[simp] lemma NominalSet.supp_atom {a : 𝔸} : supp 𝔸 a = {a} := by
+  ext b; constructor
+  · apply support_subset_supp 𝔸
+    · exact NominalSet.supp_atom' 𝔸
+    · exact Set.finite_singleton a
+  · suffices a ∈ supp 𝔸 a by simp; intro h; rwa [h]
+    intro S ⟨hsuppS, hfinS⟩
+    by_contra ha
+    -- Show that we can find a fresh c with (a c) ∈ fix S
+    obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset ({a} ∪ hfinS.toFinset)
+    simp at hc
+    have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by
+      intro d hd
+      apply Equiv.Perm.supp_notin
+      simp [FPerm.swap, 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 h₁ : ⸨a, c⸩ • a = c := by simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl]
+    have h₂ : ⸨a, c⸩ • a = a := by apply hsuppS; assumption
+    rw [h₁] at h₂
+    exact hc.left h₂
+
+@[simp] lemma NominalSet.fresh_atom {a b : 𝔸} : a # b ↔ a ≠ b := by
+  simp [IsFresh]
+
+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
+    · exact Set.finite_empty
+
+@[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', DiscreteNominalSet.is_discrete]
+  · exact Set.finite_empty
+
+@[simp] lemma NominalSet.fresh_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {a : 𝔸} {x : X} : a # x := by
+  simp [IsFresh]
+
+/-- 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
+
+/-!
+## Products
+
+Pairs of two nominal sets also form a nominal set, where supp (x, y) = supp x ∪ supp y.
+-/
+section Products
+
+instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X × Y) where
+
+variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
+
+private lemma NominalSet.supp_product' {x : X} {y : Y} : PermSet.HasSupport 𝔸 (x, y) (supp 𝔸 x ∪ supp 𝔸 y) := by
+  intro π hπ
+  obtain ⟨hπ₁, hπ₂⟩ := PermSet.fix_union 𝔸 hπ
+  exact Prod.mk_inj.mpr ⟨supp_is_support 𝔸 hπ₁, supp_is_support 𝔸 hπ₂⟩
+
+instance : NominalSet 𝔸 (X × Y) where
+  fin_supp := by
+    intro ⟨x, y⟩; use NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 y
+    exact ⟨NominalSet.supp_product' 𝔸, Set.Finite.union (NominalSet.supp_finite 𝔸) (NominalSet.supp_finite 𝔸)⟩
+
+@[simp] lemma NominalSet.supp_product {x : X} {y : Y} : supp 𝔸 (x, y) = supp 𝔸 x ∪ supp 𝔸 y := by
+  ext b; constructor
+  · apply support_subset_supp
+    · exact supp_product' 𝔸
+    · exact Set.Finite.union (supp_finite 𝔸) (supp_finite 𝔸)
+  · intro hb; cases hb with
+    | inl hx =>
+        intro S hS
+        suffices PermSet.HasSupport 𝔸 x S by apply hx; exact ⟨this, hS.out.right⟩
+        intro π hπ
+        suffices π ∈ PermSet.fix' 𝔸 (x, y) by simp [PermSet.fix'] at this; exact this.left
+        exact (hS.out.left hπ).out
+    | inr hy =>
+        intro S hS
+        suffices PermSet.HasSupport 𝔸 y S by apply hy; exact ⟨this, hS.out.right⟩
+        intro π hπ
+        suffices π ∈ PermSet.fix' 𝔸 (x, y) by simp [PermSet.fix'] at this; exact this.right
+        exact (hS.out.left hπ).out
+
+@[simp] lemma NominalSet.fresh_product {a : 𝔸} {x : X} {y : Y} : a # (x, y) ↔ a # x ∧ a # y := by
+  simp [IsFresh]
+
+lemma NominalSet.supp_product_comm {x : X} {y : Y} : supp 𝔸 (x, y) = supp 𝔸 (y, x) := by
+  simp; apply Set.union_comm
+
+lemma Prod.fst_equivariant : Equivariant 𝔸 (Prod.fst : X × Y → X) := by
+  simp [Equivariant]
+
+lemma Prod.snd_equivariant : Equivariant 𝔸 (Prod.snd : X × Y → Y) := by
+  simp [Equivariant]
+
+end Products
+
+/-!
+## Coproducts
+
+Sums of two nominal sets also form a nominal set, where supp (inl x) = supp x and supp (inr y) = supp y.
+-/
+section Coproducts
+
+instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X ⊕ Y) where
+
+variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
+
+private lemma NominalSet.supp_coproduct₁' {x : X} : PermSet.HasSupport 𝔸 (.inl x : X ⊕ Y) (supp 𝔸 x) := by
+  intro π hπ
+  simp [PermSet.fix']
+  exact supp_is_support 𝔸 hπ
+
+private lemma NominalSet.supp_coproduct₂' {y : Y} : PermSet.HasSupport 𝔸 (.inr y : X ⊕ Y) (supp 𝔸 y) := by
+  intro π hπ
+  simp [PermSet.fix']
+  exact supp_is_support 𝔸 hπ
+
+instance : NominalSet 𝔸 (X ⊕ Y) where
+  fin_supp := by
+    intro xy
+    cases xy with
+    | inl x => use NominalSet.supp 𝔸 x; exact ⟨NominalSet.supp_coproduct₁' 𝔸, NominalSet.supp_finite 𝔸⟩
+    | inr y => use NominalSet.supp 𝔸 y; exact ⟨NominalSet.supp_coproduct₂' 𝔸, NominalSet.supp_finite 𝔸⟩
+
+@[simp] lemma NominalSet.supp_coproduct₁ {x : X} : supp 𝔸 (.inl x : X ⊕ Y) = supp 𝔸 x := by
+  ext b; constructor
+  · apply support_subset_supp
+    · exact supp_coproduct₁' 𝔸
+    · exact supp_finite 𝔸
+  · intro hb S hS
+    suffices PermSet.HasSupport 𝔸 x S by apply hb; exact ⟨this, hS.out.right⟩
+    intro π hπ
+    suffices π ∈ PermSet.fix' 𝔸 (.inl x : X ⊕ Y) by simp [PermSet.fix'] at this; exact this
+    exact (hS.out.left hπ).out
+
+@[simp] lemma NominalSet.supp_coproduct₂ {y : Y} : supp 𝔸 (.inr y : X ⊕ Y) = supp 𝔸 y := by
+  ext b; constructor
+  · apply support_subset_supp
+    · exact supp_coproduct₂' 𝔸
+    · exact supp_finite 𝔸
+  · intro hb S hS
+    suffices PermSet.HasSupport 𝔸 y S by apply hb; exact ⟨this, hS.out.right⟩
+    intro π hπ
+    suffices π ∈ PermSet.fix' 𝔸 (.inr y : X ⊕ Y) by simp [PermSet.fix'] at this; exact this
+    exact (hS.out.left hπ).out
+
+@[simp] lemma NominalSet.fresh_coproduct₁ {a : 𝔸} {x : X} : a # (.inl x : X ⊕ Y) ↔ a # x := by
+  simp [IsFresh]
+
+@[simp] lemma NominalSet.fresh_coproduct₂ {a : 𝔸} {y : Y} : a # (.inr y : X ⊕ Y) ↔ a # y := by
+  simp [IsFresh]
+
+lemma Sum.inl_equivariant : Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by
+  simp [Equivariant]
+
+lemma Sum.inr_equivariant : Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by
+  simp [Equivariant]
+
+end Coproducts