fs constructions

4 files changed, 335 insertions, 1 deletions

diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 7a88eeb..a7aec47 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -398,7 +398,7 @@ instance : PermSet � S where
     exact MulAction.one_smul x.val
   mul_smul π τ x := by
     apply Subtype.ext
-    exact SemigroupAction.mul_smul π τ x.val
+    exact mul_smul π τ x.val
 
 @[simp] lemma smul_val (π : FPerm �) (x : S) : (π • x).val = π • x.val := rfl
 
diff --git a/Nominal/Instances/Finsupp.lean b/Nominal/Instances/Finsupp.lean
new file mode 100644
index 0000000..360c88a
--- /dev/null
+++ b/Nominal/Instances/Finsupp.lean
@@ -0,0 +1,312 @@
+import Mathlib
+import Nominal.Support
+import Nominal.Equivariance
+import Nominal.Category
+import Nominal.Permutations
+import Nominal.Instances.Basic
+
+/-!
+# Constructing Finitely Supported Sets
+
+We can restrict arbitrary `(FPerm �)`-sets to finitely supported subsets, which are nominal sets.
+
+Examples of this include finitely supported sets (`FinsuppSet`) and finitely supported functions (`FinsuppFunction`).
+-/
+
+variable (� : Type) [Infinite �] [Countable �] [DecidableEq �]
+
+namespace PermSet
+
+/-!
+## Finitely Supported Subsets
+
+We first define how every `PermSet` can be restricted to its finitely supported elements (`Finsupp`), which form a
+nominal set.
+-/
+section FSSubsets
+
+/-- Restrict a type to its finitely supported elements -/
+abbrev Finsupp (X : Type) [PermSet � X] : Type :=
+  { x : X // ∃ S, PermSet.HasSupport � x S ∧ S.Finite }
+
+namespace Finsupp
+
+variable {X : Type} [PermSet � X]
+
+instance : PermSet � (Finsupp � X) where
+  smul π x := ⟨π • x.val, by
+    obtain ⟨S, ⟨hS�, hS₂⟩⟩ := x.prop
+    use π • S; constructor
+    · rw [� Rel.equivariant � (HasSupport �)]
+      exact hS�
+    · exact Set.Finite.smul_set hS₂⟩
+  one_smul x := by
+    apply Subtype.ext
+    exact MulAction.one_smul x.val
+  mul_smul π τ x := by
+    apply Subtype.ext
+    exact mul_smul π τ x.val
+
+@[simp] lemma smul_val (π : FPerm �) (x : Finsupp � X) : (π • x).val = π • x.val := rfl
+
+instance instValEquivariant : Function.Equivariant � (Subtype.val : Finsupp � X → X) := by
+  constructor; simp
+
+instance : NominalSet � (Finsupp � X) where
+  fin_supp x := by
+    obtain ⟨S, ⟨hS�, hS₂⟩⟩ := x.prop
+    use S; constructor
+    · intro π hπ
+      apply Subtype.ext
+      exact hS� hπ
+    · exact hS₂
+
+end Finsupp
+
+end FSSubsets
+
+/-!
+## Finitely Supported Sets
+
+Since the powerset of an (FPerm �)-set is an (FPerm �)-set, we can restrict ourselves to finitely supported sets to
+construct a nominal set `FinsuppSet`.
+
+Furthermore, common binary operations such as union, intersection, and difference are equivariant functions.
+-/
+section FSSets
+
+abbrev FinsuppSet (X : Type) [PermSet � X] : Type :=
+  Finsupp � (Set X)
+
+namespace FinsuppSet
+
+variable (X Y : Type) [NominalSet � X] [NominalSet � Y]
+
+private def union' : (FinsuppSet � X × FinsuppSet � X) → Set X :=
+  fun (S�, S₂) ↦ S�.val ∪ S₂.val
+
+instance : Function.Equivariant � (union' � X) := by
+  constructor; intro (S�, S₂) π
+  simp only [union', PermSet.Finsupp.smul_val]
+  exact Eq.symm Set.smul_set_union
+
+def union : (FinsuppSet � X × FinsuppSet � X) → FinsuppSet � X :=
+  fun p ↦ ⟨union' � X p, by
+    use NominalSet.supp � p; constructor
+    · apply Function.Equivariant.preserve_support
+      apply NominalSet.supp_is_support
+    · apply NominalSet.supp_finite⟩
+
+instance : Function.Equivariant � (union � X) := by
+  constructor; intro p π
+  apply Subtype.ext
+  simp only [union, Finsupp.smul_val]
+  apply Function.equivariant
+
+instance : Union (FinsuppSet � X) := ⟨Function.curry (union � X)⟩
+
+@[simp] lemma union_val {S� S₂ : FinsuppSet � X} :
+    (S� ∪ S₂).val = S�.val ∪ S₂.val := rfl
+
+@[simp] lemma union_equivariant {S� S₂ : FinsuppSet � X} {π : FPerm �} :
+    π • (S� ∪ S₂) = π • S� ∪ π • S₂ := by
+  show π • (union _ _ (S�, S₂)) = union _ _ (π • (S�, S₂))
+  rw [� Function.equivariant]
+
+private def inter' : (FinsuppSet � X × FinsuppSet � X) → Set X :=
+  fun (S�, S₂) ↦ S�.val ∩ S₂.val
+
+instance : Function.Equivariant � (inter' � X) := by
+  constructor; intro (S�, S₂) π
+  simp only [inter', PermSet.Finsupp.smul_val]
+  exact Eq.symm Set.smul_set_inter
+
+def inter : (FinsuppSet � X × FinsuppSet � X) → FinsuppSet � X :=
+  fun p ↦ ⟨inter' � X p, by
+    use NominalSet.supp � p; constructor
+    · apply Function.Equivariant.preserve_support
+      apply NominalSet.supp_is_support
+    · apply NominalSet.supp_finite⟩
+
+instance : Function.Equivariant � (inter � X) := by
+  constructor; intro p π
+  apply Subtype.ext
+  simp only [inter, Finsupp.smul_val]
+  apply Function.equivariant
+
+instance : Inter (FinsuppSet � X) := ⟨Function.curry (inter � X)⟩
+
+@[simp] lemma inter_val {S� S₂ : FinsuppSet � X} :
+    (S� ∩ S₂).val = S�.val ∩ S₂.val := rfl
+
+@[simp] lemma inter_equivariant {S� S₂ : FinsuppSet � X} {π : FPerm �} :
+    π • (S� ∩ S₂) = π • S� ∩ π • S₂ := by
+  show π • (inter _ _ (S�, S₂)) = inter _ _ (π • (S�, S₂))
+  rw [� Function.equivariant]
+
+private def sdiff' : (FinsuppSet � X × FinsuppSet � X) → Set X :=
+  fun (S�, S₂) ↦ S�.val \ S₂.val
+
+instance : Function.Equivariant � (sdiff' � X) := by
+  constructor; intro (S�, S₂) π
+  simp only [sdiff', PermSet.Finsupp.smul_val]
+  exact Eq.symm Set.smul_set_sdiff
+
+def sdiff : (FinsuppSet � X × FinsuppSet � X) → FinsuppSet � X :=
+  fun p ↦ ⟨sdiff' � X p, by
+    use NominalSet.supp � p; constructor
+    · apply Function.Equivariant.preserve_support
+      apply NominalSet.supp_is_support
+    · apply NominalSet.supp_finite⟩
+
+instance : Function.Equivariant � (sdiff � X) := by
+  constructor; intro p π
+  apply Subtype.ext
+  simp only [sdiff, Finsupp.smul_val]
+  apply Function.equivariant
+
+instance : SDiff (FinsuppSet � X) := ⟨Function.curry (sdiff � X)⟩
+
+@[simp] lemma sdiff_val {S� S₂ : FinsuppSet � X} :
+    (S� \ S₂).val = S�.val \ S₂.val := rfl
+
+@[simp] lemma sdiff_equivariant {S� S₂ : FinsuppSet � X} {π : FPerm �} :
+    π • (S� \ S₂) = π • S� \ π • S₂ := by
+  show π • (sdiff _ _ (S�, S₂)) = sdiff _ _ (π • (S�, S₂))
+  rw [� Function.equivariant]
+
+end FinsuppSet
+
+end FSSets
+
+/-!
+## Finitely Supported Functions
+
+Since functions between (FPerm �)-sets are an (FPerm �)-set, we can restrict ourselves to finitely supported functions
+to construct a nominal set `FinsuppFunction`.
+
+Furthermore, there is an isomorphism between finietly supported functions (X →fs Y) and sets �fs (X × Y).
+-/
+section FSFunctions
+
+abbrev FinsuppFunction (X Y : Type) [PermSet � X] [PermSet � Y] : Type :=
+  Finsupp � (X → Y)
+
+lemma FinsuppFunction.supp_image {X Y : Type} [NominalSet � X] [NominalSet � Y] (f : PermSet.FinsuppFunction � X Y) :
+    ∀ x, PermSet.HasSupport � (f.val x) (NominalSet.supp � f ∪ NominalSet.supp � x) := by
+  intro x π hπ
+  have hπ� : π ∈ PermSet.fix � (NominalSet.supp � f) := by
+    apply PermSet.fix_antitone_mem � hπ; exact Set.subset_union_left
+  have hπ₂ : π ∈ PermSet.fix � (NominalSet.supp � x) := by
+    apply PermSet.fix_antitone_mem � hπ; exact Set.subset_union_right
+  suffices (π • f).val (π • x) = f.val x by
+    simp at this
+    exact this
+  rw [show π • f = f from NominalSet.supp_is_support � hπ�]
+  rw [show π • x = x from NominalSet.supp_is_support � hπ₂]
+
+variable (X Y : Type) [NominalSet � X] [NominalSet � Y]
+
+namespace Finsupp
+
+private def flatten' (f : X → PermSet.FinsuppSet � Y) : Set (X × Y) :=
+  {p : X × Y | p.snd ∈ (f p.fst).val}
+
+instance : Function.Equivariant � (flatten' � X Y) := by
+  constructor
+  intro f π; ext ⟨x, y⟩; constructor
+  · simp only [flatten', PermSet.smul_function, PermSet.Finsupp.smul_val, Set.mem_setOf_eq]
+    intro hy
+    have hy' : π�¹ • y ∈ π�¹ • π • (f (π�¹ • x)).val := by
+      rw [Set.smul_mem_smul_set_iff]; exact hy
+    rw [inv_smul_smul] at hy'
+    rw [show (x, y) = π • (π�¹ • x, π�¹ • y) by simp]
+    rw [Set.smul_mem_smul_set_iff]
+    exact hy'
+  · intro hxy
+    have hxy' : π�¹ • (x, y) ∈ π�¹ • π • flatten' � X Y f := by
+      rw [Set.smul_mem_smul_set_iff]; exact hxy
+    simp only [inv_smul_smul, Prod.smul_mk, flatten', Set.mem_setOf_eq] at hxy'
+    simp only [flatten', PermSet.smul_function, PermSet.Finsupp.smul_val, Set.mem_setOf_eq]
+    have hy : π • π�¹ • y ∈ π • (f (π�¹ • x)).val := by
+      rw [Set.smul_mem_smul_set_iff]; exact hxy'
+    simp only [smul_inv_smul] at hy
+    exact hy
+
+def flatten (f : PermSet.FinsuppFunction � X (PermSet.FinsuppSet � Y)) :
+    PermSet.FinsuppSet � (X × Y) :=
+  ⟨flatten' � X Y f.val, by
+    obtain ⟨S, ⟨hS�, hS₂⟩⟩ := f.prop
+    use S; constructor
+    · apply Function.Equivariant.preserve_support
+      exact hS�
+    · exact hS₂⟩
+
+instance : Function.Equivariant � (flatten � X Y) := by
+  constructor; intro p π
+  apply Subtype.ext
+  simp only [flatten, Finsupp.smul_val]
+  apply Function.equivariant
+
+private def unflatten' (S : PermSet.FinsuppSet � (X × Y)) : X → (PermSet.FinsuppSet � Y) :=
+  fun x ↦ ⟨{y : Y | (x, y) ∈ S.val}, by
+    use NominalSet.supp � S ∪ NominalSet.supp � x; constructor
+    · intro π hπ
+      have hfixx : π�¹ • x = x := by
+        apply NominalSet.supp_is_support
+        rw [� PermSet.fix_inv]
+        exact PermSet.fix_antitone_mem � hπ Set.subset_union_right
+      have hfixS : π�¹ • S = S := by
+        apply NominalSet.supp_is_support
+        rw [� PermSet.fix_inv]
+        exact PermSet.fix_antitone_mem � hπ Set.subset_union_left
+      ext y; constructor
+      · intro hy
+        simp only [Set.mem_smul_set_iff_inv_smul_mem, Set.mem_setOf_eq] at hy
+        rw [� hfixx, � hfixS, smul_val, Set.mem_inv_smul_set_iff, Prod.smul_mk, smul_inv_smul, smul_inv_smul] at hy
+        exact hy
+      · intro hy
+        simp only [Set.mem_smul_set_iff_inv_smul_mem, Set.mem_setOf_eq]
+        simp only [Set.mem_setOf_eq] at hy
+        have hy' : (π�¹ • x, π�¹ • y) ∈ π�¹ • S.val := Set.smul_mem_smul_set hy
+        rw [hfixx, � smul_val, hfixS] at hy'
+        exact hy'
+    · simp only [Set.finite_union]; constructor
+      · exact NominalSet.supp_finite �
+      · exact NominalSet.supp_finite �⟩
+
+instance : Function.Equivariant � (unflatten' � X Y) := by
+  constructor
+  intro S π
+  ext x y
+  simp only [unflatten', smul_val, Set.mem_setOf_eq, smul_function]
+  simp only [Set.mem_smul_set_iff_inv_smul_mem, Set.mem_setOf_eq, Prod.smul_mk]
+
+def unflatten (S : PermSet.FinsuppSet � (X × Y)) : PermSet.FinsuppFunction � X (PermSet.FinsuppSet � Y) :=
+  ⟨unflatten' � X Y S, by
+    obtain ⟨A, ⟨hS�, hS₂⟩⟩ := S.prop
+    use A; constructor
+    · apply Function.Equivariant.preserve_support
+      rw [� Function.Equivariant.preserve_support_inj � Subtype.val_injective] at hS�
+      exact hS�
+    · exact hS₂⟩
+
+instance : Function.Equivariant � (unflatten � X Y) := by
+  constructor; intro p π
+  apply Subtype.ext
+  simp only [unflatten, Finsupp.smul_val]
+  apply Function.equivariant
+
+def flattenEquiv  :
+    EquivariantEquiv �
+      (PermSet.FinsuppFunction � X (PermSet.FinsuppSet � Y))
+      (PermSet.FinsuppSet � (X × Y)) where
+  toFun := flatten � X Y
+  invFun := unflatten � X Y
+  toFun_equivariant := inferInstance
+
+end Finsupp
+
+end FSFunctions
+
+end PermSet
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index f1115d3..6119df3 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -259,4 +259,16 @@ lemma PermSet.atom_set_swap_left {a b : �} {S : Set �} : a ∈ S ↔ b ∈
 lemma PermSet.atom_set_swap_right {a b : �} {S : Set �} : b ∈ S ↔ a ∈ ⸨a, b⸩ • S := by
   rw [FPerm.swap_comm, atom_set_swap_left]
 
+instance {X Y : Type} [SMul (FPerm �) X] [SMul (FPerm �) Y] : SMul (FPerm �) (X → Y) where
+  smul π f := fun x ↦ π • f (π�¹ • x)
+
+@[simp] lemma PermSet.smul_function {X Y : Type} [PermSet � X] [PermSet � Y] (π : FPerm �)
+    (f : X → Y) (x : X) : (π • f) x = π • f (π�¹ • x) :=
+  rfl
+
+/-- Functions between (FPerm �)-sets form (FPerm �)-sets with (π • f) x = π • f (π�¹ • x). -/
+instance {X Y : Type} [PermSet � X] [PermSet � Y] : PermSet � (X → Y) where
+  one_smul f := by ext x; simp
+  mul_smul π τ f := by ext x; simp [mul_smul]
+
 end PermSet
diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index fde20c7..bb2ec92 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -33,6 +33,11 @@ def fix (A : Set X) : Set (FPerm �) :=
 def HasSupport (x : X) (S : Set �) : Prop :=
   fix � S ⊆ fix' � x
 
+lemma perm_fixes_iff_inv_fixes {X : Type} [PermSet � X] (π : FPerm �) (x : X) : π • x = x ↔ π�¹ • x = x := by
+  constructor
+  · intro h; nth_rw 1 [� h]; simp
+  · intro h; nth_rw 1 [� h]; simp
+
 /-- fix is antitone: If S ⊆ T, then fix S ⊇ fix T. -/
 lemma fix_antitone {X : Type} [PermSet � X] {S T : Set X} : S ⊆ T → PermSet.fix � T ⊆ PermSet.fix � S := by
   intro hsub π hπ x hx
@@ -48,6 +53,11 @@ lemma fix_antitone_mem {X : Type} [PermSet ð�”¸ X] {S T : Set X} {Ï€ : FPerm ð�”
 lemma fix_union {X : Type} [PermSet � X] {S T : Set X} : PermSet.fix � (S ∪ T) ⊆ PermSet.fix � S ∩ PermSet.fix � T := by
   apply Set.subset_inter <;> all_goals simp [fix_antitone]
 
+lemma fix_inv {X : Type} [PermSet � X] {S : Set X} {π : FPerm �} : π ∈ PermSet.fix � S ↔ π�¹ ∈ PermSet.fix � S := by
+  constructor
+  · intro h x hx; rw [� perm_fixes_iff_inv_fixes]; exact h x hx
+  · intro h x hx; rw [perm_fixes_iff_inv_fixes]; exact h x hx
+
 /-- Alternative definition with fix � S unfolded. -/
 lemma support_iff {x : X} {S : Set �} : HasSupport � x S ↔ ∀ (π : FPerm �), (∀ x ∈ S, π x = x) → π ∈ fix' � x := by
   simp [HasSupport, fix, fix']