start working on alpha equivalence proofs

1 files changed, 16 insertions, 0 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 50cf7c2..57c6d11 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -161,6 +161,17 @@ lemma supp_eq_if_inj {x : X} {f : X → Y} : Equivariant 𝔸 f → Function.Inj
 
 end Equivariant
 
+/-- If there is an equivariant surjection from a nominal set into an (FPerm 𝔸)-Set, then that set is nominal. -/
+def NominalSet.fromEquivariantSurjective {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y] (f : X → Y) (hequi : Equivariant 𝔸 f) (hsurj : Function.Surjective f) : NominalSet 𝔸 Y where
+  fin_supp := by
+    intro y
+    obtain ⟨x, hx⟩ := hsurj y
+    use (NominalSet.supp 𝔸 x)
+    constructor
+    · rw [← hx]
+      exact Equivariant.preserve_support 𝔸 hequi (supp_is_support 𝔸)
+    · exact supp_finite 𝔸
+
 /-- supp is an equivariant function. -/
 lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸) := by
   intro x π; ext a; constructor
@@ -182,6 +193,11 @@ lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸
     · apply Set.Finite.smul_set
       exact hS.out.right
 
+/-- Freshness is an equivariant relation. -/
+lemma NominalSet.fresh_equivariant : EquivariantRelation 𝔸 (NominalSet.IsFresh : 𝔸 → X → Prop) := by
+  intro x y π h
+  rwa [IsFresh, supp_equivariant, Set.smul_mem_smul_set_iff]
+
 end Nominal
 
 /-!