name abstraction functor

1 files changed, 16 insertions, 0 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 0fe9f91..3166e71 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -163,6 +163,16 @@ lemma supp_eq_if_inj {x : X} {f : X → Y} : Equivariant 𝔸 f → Function.Inj
   intro hequi hinj
   simp [NominalSet.supp, preserve_support_inj 𝔸 hequi hinj]
 
+/-- If f is equivariant and a # x, then a # f x. -/
+lemma preserve_fresh {a : 𝔸} {x : X} {f : X → Y} : Equivariant 𝔸 f → a # x → a # f x := by
+  intro hequi hx ha
+  exact hx ((supp_subset 𝔸 hequi) ha)
+
+/-- If f is equivariant and injective, then a # x iff a # f x. -/
+lemma preserve_fresh_inj {a : 𝔸} {x : X} {f : X → Y} : Equivariant 𝔸 f → Function.Injective f → (a # x ↔ a # f x) := by
+  intro hequi hinj
+  rw [NominalSet.IsFresh, NominalSet.IsFresh, supp_eq_if_inj 𝔸 hequi hinj]
+
 end Equivariant
 
 /-- If there is an equivariant surjection from a nominal set into an (FPerm 𝔸)-Set, then that set is nominal. -/
@@ -306,6 +316,12 @@ def id : X →ₑ[𝔸] X := ⟨_root_.id, id_equivariant 𝔸⟩
 def comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : X →ₑ[𝔸] Z := ⟨f ∘ g, comp_equivariant 𝔸 f.equivariant g.equivariant⟩
 
 @[simp]
+lemma id_app (x : X) : id 𝔸 x = x := rfl
+
+@[simp]
+lemma comp_app (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) (x : X) : comp 𝔸 f g x = f (g x) := rfl
+
+@[simp]
 lemma toFun_eq_coe {f : X →ₑ[𝔸] Y} : f.toFun = (f : X → Y) :=
   rfl