add equivariant instances

3 files changed, 112 insertions, 2 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 4d23e56..c9a5261 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -31,9 +31,62 @@ def EquivariantSet (S : Set X) : Prop :=
 def EquivariantRelation (R : Rel X Y) : Prop :=
   ∀ (x : X) (y : Y) (π : FPerm �), R x y → R (π • x) (π • y)
 
+/-- For equivariant sets, we even have "if and only if". -/
+lemma equivariant_set_iff {S : Set X} : EquivariantSet � S ↔ ∀ (x : X) (π : FPerm �), x ∈ S ↔ π • x ∈ S := by
+  constructor
+  · intro h x π; constructor
+    · intro hx; exact h x π hx
+    · intro hx
+      apply (h (π • x) π�¹) at hx
+      simp at hx
+      exact hx
+  · intro h x π hx
+    exact (h x π).mp hx
+
+/-- For equivariant relations, we even have "if and only if". -/
+lemma equivariant_relation_iff {R : Rel X Y} : EquivariantRelation � R ↔ ∀ (x : X) (y : Y) (π : FPerm �), R x y ↔ R (π • x) (π • y) := by
+  constructor
+  · intro h x y π; constructor
+    · intro hxy; exact h x y π hxy
+    · intro hxy
+      apply (h (π • x) (π • y) π�¹) at hxy
+      simp at hxy
+      exact hxy
+  · intro h x y π hxy
+    exact (h x y π).mp hxy
+
 end Definition
 
 /-!
+## Trivial Instances
+
+Some trivial instances of equivariant functions, sets, and relations.
+-/
+section Trivial
+
+variable {X Y Z : Type} [PermSet � X] [PermSet � Y] [PermSet � Z]
+
+/-- The identity function is equivariant. -/
+lemma id_equivariant : Equivariant � (id : X → X) := by
+  simp [Equivariant]
+
+/-- The composition of two equivariant functions is equivariant. -/
+lemma comp_equivariant {f : X → Y} {g : Y → Z} : Equivariant � f → Equivariant � g → Equivariant � (g ∘ f) := by
+  intro hf hg x π
+  calc
+    g (f (π • x)) = g (π • f x)   := by rw [hf]
+    _             = π • (g (f x)) := by rw [hg]
+
+/-- The subset relation is equivariant. -/
+lemma subset_equivariant : EquivariantRelation � (Set.Subset : Set X → Set X → Prop) := by
+  intro S T π hST x hx
+  rw [Set.mem_smul_set_iff_inv_smul_mem] at hx
+  rw [Set.mem_smul_set_iff_inv_smul_mem]
+  exact hST hx
+
+end Trivial
+
+/-!
 ## Support
 
 Propositions relating equivariance to support in (FPerm �)-sets.
@@ -63,6 +116,24 @@ lemma preserve_support_inj {x : X} {f : X → Y} {S : Set ð�”¸} : Equivariant ð�
 
 end Equivariant
 
+/-- HasSupport is an equivariant relation. -/
+lemma PermSet.support_equivariant : EquivariantRelation � (HasSupport � : X → Set � → Prop) := by
+  intro x S π hS σ hσ
+  have hfix : (π�¹ * σ * π) ∈ fix � S := by
+    intro a ha
+    calc
+      (π�¹ * σ * π) • a = π�¹ • (σ • (π • a)) := rfl
+      _                 = π�¹ • (π • a)       := by rw [hσ (π • a) (Set.smul_mem_smul_set ha)]
+      _                 = (π�¹ * π) • a       := rfl
+      _                 = (1 : FPerm �) • a   := by rw [@Group.inv_mul_cancel]
+      _                 = a                   := rfl
+  calc
+    σ • (π • x) = (σ * π) • x             := by apply smul_smul
+    _           = (1 * σ * π) • x         := rfl
+    _           = (π * π�¹ * σ * π) • x   := by rw [@mul_inv_cancel]
+    _           = π • ((π�¹ * σ * π) • x) := by symm; apply smul_smul
+    _           = π • x                   := by rw [hS hfix]
+
 end Support
 
 /-!
@@ -90,4 +161,25 @@ lemma supp_eq_if_inj {x : X} {f : X → Y} : Equivariant � f → Function.Inj
 
 end Equivariant
 
+/-- supp is an equivariant function. -/
+lemma NominalSet.supp_equivariant : Equivariant � (supp � : X → Set �) := by
+  intro x π; ext a; constructor
+  · apply support_subset_supp �
+    · apply PermSet.support_equivariant
+      exact supp_is_support �
+    · apply Set.Finite.smul_set
+      exact supp_finite �
+  · intro ha S hS
+    have hsupp : PermSet.HasSupport � x (π�¹ • S) := by
+      rw [show x = π�¹ • π • x by exact eq_inv_smul_iff.mpr rfl]
+      apply PermSet.support_equivariant
+      exact hS.out.left
+    rw [Set.mem_smul_set_iff_inv_smul_mem] at ha
+    suffices π�¹ • a ∈ π�¹ • S by rw [Set.smul_mem_smul_set_iff] at this; assumption
+    suffices supp � x ⊆ π�¹ • S by exact this ha
+    apply support_subset_supp �
+    · exact hsupp
+    · apply Set.Finite.smul_set
+      exact hS.out.right
+
 end Nominal
diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean
index e28fe28..b637b32 100644
--- a/Nominal/Instances.lean
+++ b/Nominal/Instances.lean
@@ -1,5 +1,6 @@
 import Mathlib
 import Nominal.Support
+import Nominal.Equivariance
 
 /-!
 # Instances
@@ -132,6 +133,12 @@ instance : NominalSet � (X × Y) where
 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
 
 /-!
@@ -190,4 +197,10 @@ instance : NominalSet � (X ⊕ Y) where
 @[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
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index c8fdd86..4a3e88f 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -141,16 +141,21 @@ class PermSet (� : Type) [Infinite �] [Countable �] [DecidableEq �]
 
 variable (� : Type) [Infinite �] [Countable �] [DecidableEq �]
 
-/-- The set of atoms itself forms a (FPerm �)-Set. -/
+/-- The set of atoms itself forms an (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. -/
+/-- The set of finite permutations forms an (FPerm �)-Set. -/
 instance : PermSet � (FPerm �) where
   smul π τ := π * τ
   one_smul := by intro; rfl
   mul_smul := by intro _ _ _; rfl
 
+open Pointwise
+
+/-- The powerset of an (FPerm �)-Set forms an (FPerm �)-Set using pointwise permutation. -/
+instance {X : Type} [PermSet � X] : PermSet � (Set X) where
+
 end PermSet