diff options
Diffstat (limited to 'Nominal/Equivariance.lean')
| -rw-r--r-- | Nominal/Equivariance.lean | 16 |
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 /-! |