From 8f1d3f45f11aae5d611a66c424b6427f379a8251 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Tue, 28 Oct 2025 23:41:02 +0100 Subject: name abstraction functor --- Nominal/Equivariance.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'Nominal/Equivariance.lean') 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. -/ @@ -305,6 +315,12 @@ def id : X β†’β‚‘[𝔸] X := ⟨_root_.id, id_equivariant π”ΈβŸ© /-- Function composition. -/ 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 -- cgit v1.3.1