prove supp of preterms

1 files changed, 39 insertions, 0 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 7087076..4ba580d 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -77,6 +77,12 @@ lemma comp_equivariant {f : Y → Z} {g : X → Y} : Function.Equivariant 𝔸 f
     f (g (π • x)) = f (π • g x)   := by rw [hg]
     _             = π • (f (g x)) := by rw [hf]
 
+/-- If a function is equivariant, its inverse is also equivariant. -/
+lemma Function.inv_equivariant {f : X → Y} {inv : Y → X} : Function.LeftInverse inv f → Function.RightInverse inv f → Function.Equivariant 𝔸 f → Function.Equivariant 𝔸 inv := by
+  intro hleft hright hequi y π
+  apply hleft.injective
+  rw [hequi, hright, hright]
+
 /-- The subset relation is equivariant. -/
 lemma Set.subset_equivariant : Rel.Equivariant 𝔸 (Set.Subset : Set X → Set X → Prop) := by
   intro S T π hST x hx
@@ -332,3 +338,36 @@ class EquivariantSetoid (X : Type) [PermSet 𝔸 X] extends Setoid X where
   equivariant : Rel.Equivariant 𝔸 r
 
 end BundledFunction
+
+/-!
+## Equivalences
+
+If two types are equivalent and the conversion function is also equivariant, we know some additional information about nominal set structures.
+-/
+section Equivalence
+
+/-- An equivalence where the function is equivariant. -/
+structure EquivariantEquiv (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] extends Equiv X Y where
+  toFun_equivariant : Function.Equivariant 𝔸 toFun
+  invFun_equivariant : Function.Equivariant 𝔸 invFun := Function.inv_equivariant 𝔸 left_inv right_inv toFun_equivariant
+
+def Equivariant.Equiv.symm {𝔸 X Y : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] [PermSet 𝔸 X] [PermSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : EquivariantEquiv 𝔸 Y X :=
+  { toFun := equiv.invFun
+    invFun := equiv.toFun
+    toFun_equivariant := equiv.invFun_equivariant
+    left_inv := equiv.right_inv
+    right_inv := equiv.left_inv
+  }
+
+/-- If an (FPerm 𝔸)-Set is equivalent to a nominal set, it is also a nominal set. -/
+def NominalSet.fromEquivariantEquiv {X Y : Type} [PermSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : NominalSet 𝔸 X :=
+  NominalSet.fromEquivariantSurjective 𝔸 equiv.invFun equiv.invFun_equivariant equiv.symm.surjective
+
+/-- If two nominal sets are equivalent, the corresponding least supports are equal. -/
+lemma EquivariantEquiv.supp_eq {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) (x : X) : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 (equiv.toFun x) := by
+  symm
+  apply Function.Equivariant.supp_eq_if_inj
+  · exact equiv.toFun_equivariant
+  · exact equiv.injective
+
+end Equivalence