From 71a6a3d5b6f4b428b463bc4a0766c91d8c1d5768 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Wed, 3 Dec 2025 20:34:41 +0100 Subject: refactor equivariant props to use type classes --- Nominal/Equivariance.lean | 224 +++++++++++++++++++++++++--------------------- 1 file changed, 124 insertions(+), 100 deletions(-) (limited to 'Nominal/Equivariance.lean') diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 4ba580d..2682a55 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -20,40 +20,42 @@ section Definition variable {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] /-- A function is equivariant if it is invariant to applying a permutation before or after the function. -/ -def Function.Equivariant (f : X β†’ Y) : Prop := - βˆ€ (x : X) (Ο€ : FPerm 𝔸), f (Ο€ β€’ x) = Ο€ β€’ f x +class inductive Function.Equivariant (f : X β†’ Y) : Prop + | intro : (βˆ€ (x : X) (Ο€ : FPerm 𝔸), f (Ο€ β€’ x) = Ο€ β€’ f x) β†’ Equivariant f -/-- A set is equivariant if it is closed under permutations. -/ -def Set.Equivariant (S : Set X) : Prop := - βˆ€ (x : X) (Ο€ : FPerm 𝔸), x ∈ S β†’ Ο€ β€’ x ∈ S +lemma Function.equivariant (f : X β†’ Y) [Equivariant 𝔸 f] : + βˆ€ (x : X) (Ο€ : FPerm 𝔸), f (Ο€ β€’ x) = Ο€ β€’ f x := by + cases (inferInstanceAs (Equivariant 𝔸 f)); assumption -/-- A binary relation is equivariant if it is closed under permutations. -/ -def Rel.Equivariant (R : Rel X Y) : Prop := - βˆ€ (x : X) (y : Y) (Ο€ : FPerm 𝔸), R x y β†’ R (Ο€ β€’ x) (Ο€ β€’ y) +/-- A set is equivariant if it is closed under permutations. -/ +class inductive Set.Equivariant (S : Set X) : Prop + | intro : (βˆ€ (x : X) (Ο€ : FPerm 𝔸), x ∈ S β†’ Ο€ β€’ x ∈ S) β†’ Equivariant S /-- For equivariant sets, we even have "if and only if". -/ -lemma Set.Equivariant.iff {S : Set X} : Set.Equivariant 𝔸 S ↔ βˆ€ (x : X) (Ο€ : FPerm 𝔸), x ∈ S ↔ Ο€ β€’ x ∈ S := by - constructor - Β· intro h x Ο€; constructor - Β· intro hx; exact h x Ο€ hx - Β· intro hx - apply (h (Ο€ β€’ x) π⁻¹) at hx - simp only [inv_smul_smul] at hx - exact hx - Β· intro h x Ο€ hx - exact (h x Ο€).mp hx +lemma Set.equivariant (S : Set X) [Equivariant 𝔸 S] : + βˆ€ (x : X) (Ο€ : FPerm 𝔸), x ∈ S ↔ Ο€ β€’ x ∈ S := by + cases (inferInstanceAs (Equivariant 𝔸 S)); rename_i h + intro x Ο€; constructor + Β· intro hx; exact h x Ο€ hx + Β· intro hx + apply (h (Ο€ β€’ x) π⁻¹) at hx + simp only [inv_smul_smul] at hx + exact hx + +/-- A binary relation is equivariant if it is closed under permutations. -/ +class inductive Rel.Equivariant (R : Rel X Y) : Prop + | intro : (βˆ€ (x : X) (y : Y) (Ο€ : FPerm 𝔸), R x y β†’ R (Ο€ β€’ x) (Ο€ β€’ y)) β†’ Equivariant R /-- For equivariant relations, we even have "if and only if". -/ -lemma Rel.Equivariant.iff {R : Rel X Y} : Rel.Equivariant 𝔸 R ↔ βˆ€ (x : X) (y : Y) (Ο€ : FPerm 𝔸), R x y ↔ R (Ο€ β€’ x) (Ο€ β€’ y) := by - constructor - Β· intro h x y Ο€; constructor - Β· intro hxy; exact h x y Ο€ hxy - Β· intro hxy - apply (h (Ο€ β€’ x) (Ο€ β€’ y) π⁻¹) at hxy - simp only [inv_smul_smul] at hxy - exact hxy - Β· intro h x y Ο€ hxy - exact (h x y Ο€).mp hxy +lemma Rel.equivariant (R : Rel X Y) [Rel.Equivariant 𝔸 R] : + βˆ€ (x : X) (y : Y) (Ο€ : FPerm 𝔸), R x y ↔ R (Ο€ β€’ x) (Ο€ β€’ y) := by + cases (inferInstanceAs (Equivariant 𝔸 R)); rename_i h + intro x y Ο€; constructor + Β· intro hxy; exact h x y Ο€ hxy + Β· intro hxy + apply (h (Ο€ β€’ x) (Ο€ β€’ y) π⁻¹) at hxy + simp only [inv_smul_smul] at hxy + exact hxy end Definition @@ -67,25 +69,32 @@ section Trivial variable {X Y Z : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] [PermSet 𝔸 Z] /-- The identity function is equivariant. -/ -lemma id_equivariant : Function.Equivariant 𝔸 (id : X β†’ X) := by - simp [Function.Equivariant] +instance Function.Equivariant.id : Function.Equivariant 𝔸 (id : X β†’ X) := by + constructor + simp /-- The composition of two equivariant functions is equivariant. -/ -lemma comp_equivariant {f : Y β†’ Z} {g : X β†’ Y} : Function.Equivariant 𝔸 f β†’ Function.Equivariant 𝔸 g β†’ Function.Equivariant 𝔸 (f ∘ g) := by - intro hf hg x Ο€ +instance Function.Equivariant.comp + {f : Y β†’ Z} [Function.Equivariant 𝔸 f] {g : X β†’ Y} [Function.Equivariant 𝔸 g] : + Function.Equivariant 𝔸 (f ∘ g) := by + constructor; intro x Ο€ calc - f (g (Ο€ β€’ x)) = f (Ο€ β€’ g x) := by rw [hg] - _ = Ο€ β€’ (f (g x)) := by rw [hf] + f (g (Ο€ β€’ x)) = f (Ο€ β€’ g x) := by rw [← Function.equivariant 𝔸 g] + _ = Ο€ β€’ (f (g x)) := by rw [← Function.equivariant 𝔸 f] /-- 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 Ο€ +def Function.Equivariant.inv + {f : X β†’ Y} [Function.Equivariant 𝔸 f] {inv : Y β†’ X} + (hleft : Function.LeftInverse inv f) + (hright : Function.RightInverse inv f) : + Function.Equivariant 𝔸 inv := by + constructor; intro y Ο€ apply hleft.injective - rw [hequi, hright, hright] + rw [Function.equivariant 𝔸 f, 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 +instance Set.Equivariant.subset : Rel.Equivariant 𝔸 (Set.Subset : Set X β†’ Set X β†’ Prop) := by + constructor; intro S T Ο€ hST x hx rw [Set.mem_smul_set_iff_inv_smul_mem] at hx rw [Set.mem_smul_set_iff_inv_smul_mem] exact hST hx @@ -104,27 +113,29 @@ variable {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] namespace Function.Equivariant /-- Equivariant functions preserve supports. -/ -lemma preserve_support {x : X} {f : X β†’ Y} {S : Set 𝔸} : Equivariant 𝔸 f β†’ PermSet.HasSupport 𝔸 x S β†’ PermSet.HasSupport 𝔸 (f x) S := by - intro hequi hsupp Ο€ hΟ€ +lemma preserve_support {x : X} {f : X β†’ Y} [Equivariant 𝔸 f] {S : Set 𝔸} : + PermSet.HasSupport 𝔸 x S β†’ PermSet.HasSupport 𝔸 (f x) S := by + intro hsupp Ο€ hΟ€ calc - Ο€ β€’ f x = f (Ο€ β€’ x) := by rw [← hequi] + Ο€ β€’ f x = f (Ο€ β€’ x) := by rw [← equivariant 𝔸 f] _ = f x := by rw [hsupp hΟ€] /-- Equivariant injective functions exactly preserve supports. -/ -lemma preserve_support_inj {x : X} {f : X β†’ Y} {S : Set 𝔸} : Equivariant 𝔸 f β†’ f.Injective β†’ (PermSet.HasSupport 𝔸 x S ↔ PermSet.HasSupport 𝔸 (f x) S) := by - intro hequi hinj; constructor - Β· exact preserve_support 𝔸 hequi +lemma preserve_support_inj {x : X} {f : X β†’ Y} [Equivariant 𝔸 f] {S : Set 𝔸} : + f.Injective β†’ (PermSet.HasSupport 𝔸 x S ↔ PermSet.HasSupport 𝔸 (f x) S) := by + intro hinj; constructor + Β· exact preserve_support 𝔸 Β· intro hsupp Ο€ hΟ€ by_contra h - have : Ο€ β€’ f x β‰  f x := by rw [← hequi]; exact fun a => h (hinj a) + have : Ο€ β€’ f x β‰  f x := by rw [← equivariant 𝔸 f]; intro hcontra; exact h (hinj hcontra) have : Ο€ β€’ f x = f x := hsupp hΟ€ contradiction end Function.Equivariant /-- HasSupport is an equivariant relation. -/ -lemma PermSet.support_equivariant : Rel.Equivariant 𝔸 (HasSupport 𝔸 : X β†’ Set 𝔸 β†’ Prop) := by - intro x S Ο€ hS Οƒ hΟƒ +instance PermSet.instHasSupportEquivariant : Rel.Equivariant 𝔸 (HasSupport 𝔸 : X β†’ Set 𝔸 β†’ Prop) := by + constructor; intro x S Ο€ hS Οƒ hΟƒ have hfix : (π⁻¹ * Οƒ * Ο€) ∈ fix 𝔸 S := by intro a ha calc @@ -154,52 +165,58 @@ variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] namespace Function.Equivariant /-- If f is equivariant, then supp (f x) βŠ† supp x. -/ -lemma supp_subset {x : X} {f : X β†’ Y} : Equivariant 𝔸 f β†’ NominalSet.supp 𝔸 (f x) βŠ† NominalSet.supp 𝔸 x := by - intro hequi +lemma supp_subset {x : X} {f : X β†’ Y} [Equivariant 𝔸 f] : + NominalSet.supp 𝔸 (f x) βŠ† NominalSet.supp 𝔸 x := by apply NominalSet.support_subset_supp - Β· exact preserve_support 𝔸 hequi (NominalSet.supp_is_support 𝔸) + Β· exact preserve_support 𝔸 (NominalSet.supp_is_support 𝔸) Β· exact NominalSet.supp_finite 𝔸 /-- If f is equivariant and injective, then supp (f x) = supp x. -/ -lemma supp_eq_if_inj {x : X} {f : X β†’ Y} : Equivariant 𝔸 f β†’ Function.Injective f β†’ NominalSet.supp 𝔸 (f x) = NominalSet.supp 𝔸 x := by - intro hequi hinj - simp [NominalSet.supp, preserve_support_inj 𝔸 hequi hinj] +lemma supp_eq_if_inj {x : X} {f : X β†’ Y} [Equivariant 𝔸 f] : + Function.Injective f β†’ NominalSet.supp 𝔸 (f x) = NominalSet.supp 𝔸 x := by + intro hinj + simp [NominalSet.supp, preserve_support_inj 𝔸 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) +lemma preserve_fresh {a : 𝔸} {x : X} {f : X β†’ Y} [Equivariant 𝔸 f] : a # x β†’ a # f x := by + intro hx ha + exact hx (supp_subset 𝔸 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] +lemma preserve_fresh_inj {a : 𝔸} {x : X} {f : X β†’ Y} [Equivariant 𝔸 f] : + Function.Injective f β†’ (a # x ↔ a # f x) := by + intro hinj + rw [NominalSet.IsFresh, NominalSet.IsFresh, supp_eq_if_inj 𝔸 hinj] end Function.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 : Function.Equivariant 𝔸 f) (hsurj : Function.Surjective f) : NominalSet 𝔸 Y where +def NominalSet.ofEquivariantSurjective + {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y] + (f : X β†’ Y) [Function.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 Function.Equivariant.preserve_support 𝔸 hequi (supp_is_support 𝔸) + exact Function.Equivariant.preserve_support 𝔸 (supp_is_support 𝔸) Β· exact supp_finite 𝔸 /-- supp is an equivariant function. -/ -lemma NominalSet.supp_equivariant : Function.Equivariant 𝔸 (supp 𝔸 : X β†’ Set 𝔸) := by - intro x Ο€; ext a; constructor +instance NominalSet.instSuppEquivariant : Function.Equivariant 𝔸 (supp 𝔸 : X β†’ Set 𝔸) := by + constructor; intro x Ο€ + ext a; constructor Β· apply support_subset_supp 𝔸 - Β· apply PermSet.support_equivariant + Β· rw [← Rel.equivariant 𝔸 (PermSet.HasSupport 𝔸)] exact supp_is_support 𝔸 Β· apply Set.Finite.smul_set exact supp_finite 𝔸 Β· intro ha S hS have hsupp : PermSet.HasSupport 𝔸 x (π⁻¹ β€’ S) := by rw [show x = π⁻¹ β€’ Ο€ β€’ x by exact eq_inv_smul_iff.mpr rfl] - apply PermSet.support_equivariant + rw [← Rel.equivariant 𝔸 (PermSet.HasSupport 𝔸)] exact hS.out.left rw [Set.mem_smul_set_iff_inv_smul_mem] at ha suffices π⁻¹ β€’ a ∈ π⁻¹ β€’ S by rw [Set.smul_mem_smul_set_iff] at this; assumption @@ -210,9 +227,9 @@ lemma NominalSet.supp_equivariant : Function.Equivariant 𝔸 (supp 𝔸 : X β†’ exact hS.out.right /-- Freshness is an equivariant relation. -/ -lemma NominalSet.fresh_equivariant : Rel.Equivariant 𝔸 (NominalSet.IsFresh : 𝔸 β†’ X β†’ Prop) := by - intro x y Ο€ h - rwa [IsFresh, supp_equivariant, Set.smul_mem_smul_set_iff] +instance NominalSet.instFreshEquivariant : Rel.Equivariant 𝔸 (NominalSet.IsFresh : 𝔸 β†’ X β†’ Prop) := by + constructor; intro x y Ο€ h + rwa [IsFresh, Function.equivariant 𝔸 (supp 𝔸), Set.smul_mem_smul_set_iff] end Nominal @@ -229,8 +246,8 @@ variable {X : Type} [NominalSet 𝔸 X] {R: Rel 𝔸 X} {x : X} -- We continue with a circular implication chain argument to show these equivalences. -private lemma for_fresh_iff₁ : Equivariant 𝔸 R β†’ (И a, R a x) β†’ (βˆƒ a, a # x ∧ R a x) := by - intro hequi h +private lemma for_fresh_iff₁ : (И a, R a x) β†’ (βˆƒ a, a # x ∧ R a x) := by + intro h apply Set.Finite.infinite_compl at h simp at h have hinf : ({a | R a x} \ NominalSet.supp 𝔸 x).Infinite := Set.Infinite.diff h (NominalSet.supp_finite 𝔸) @@ -238,17 +255,16 @@ private lemma for_fresh_iff₁ : Equivariant 𝔸 R β†’ (И a, R a x) β†’ (βˆƒ a simp only [Set.mem_diff, Set.mem_setOf_eq] at ha use a; exact ha.symm -private lemma for_fresh_iffβ‚‚ : Equivariant 𝔸 R β†’ (βˆƒ a, a # x ∧ R a x) β†’ (βˆ€ a, a # x β†’ R a x) := by - intro hequi h +private lemma for_fresh_iffβ‚‚ [Rel.Equivariant 𝔸 R] : (βˆƒ a, a # x ∧ R a x) β†’ (βˆ€ a, a # x β†’ R a x) := by + intro h obtain ⟨a, ⟨hfresha, ha⟩⟩ := h intro b hfreshb - have hmem := hequi a x βΈ¨a, bβΈ© ha - rw [PermSet.atom_swap, Equiv.swap_apply_left] at hmem - rw [NominalSet.fresh_swap_fix 𝔸 hfresha hfreshb] at hmem - exact hmem + rw [Rel.equivariant 𝔸 R b x βΈ¨a, bβΈ©] + rw [PermSet.atom_swap, Equiv.swap_apply_right, NominalSet.fresh_swap_fix 𝔸 hfresha hfreshb] + exact ha -private lemma for_fresh_iff₃ : Equivariant 𝔸 R β†’ (βˆ€ a, a # x β†’ R a x) β†’ (И a, R a x) := by - intro hequi h +private lemma for_fresh_iff₃ : (βˆ€ a, a # x β†’ R a x) β†’ (И a, R a x) := by + intro h have hsub : {a : 𝔸 | R a x}ᢜ βŠ† NominalSet.supp 𝔸 x := by rw [Set.compl_subset_comm] intro a ha @@ -258,25 +274,25 @@ private lemma for_fresh_iff₃ : Equivariant 𝔸 R β†’ (βˆ€ a, a # x β†’ R a x) apply Set.Finite.subset (NominalSet.supp_finite 𝔸) hsub /-- The quantifier in `И a, a R x` is equivalent to "for any fresh `a`". -/ -lemma for_fresh_iff_exists : Equivariant 𝔸 R β†’ ((И a, R a x) ↔ (βˆƒ a, a # x ∧ R a x)) := by - intro hequi; constructor +lemma for_fresh_iff_exists [Rel.Equivariant 𝔸 R] : ((И a, R a x) ↔ (βˆƒ a, a # x ∧ R a x)) := by + constructor Β· intro h - apply for_fresh_iff₁ 𝔸 hequi + apply for_fresh_iff₁ exact h Β· intro h - apply for_fresh_iff₃ 𝔸 hequi - apply for_fresh_iffβ‚‚ 𝔸 hequi + apply for_fresh_iff₃ + apply for_fresh_iffβ‚‚ exact h /-- The quantifier in `И a, a R x` is equivalent to "for all fresh `a`". -/ -lemma for_fresh_iff_all : Equivariant 𝔸 R β†’ ((И a, R a x) ↔ (βˆ€ a, a # x β†’ R a x)) := by - intro hequi; constructor +lemma for_fresh_iff_all [Rel.Equivariant 𝔸 R] : ((И a, R a x) ↔ (βˆ€ a, a # x β†’ R a x)) := by + constructor Β· intro h - apply for_fresh_iffβ‚‚ 𝔸 hequi - apply for_fresh_iff₁ 𝔸 hequi + apply for_fresh_iffβ‚‚ + apply for_fresh_iff₁ exact h Β· intro h - apply for_fresh_iff₃ 𝔸 hequi + apply for_fresh_iff₃ exact h end Rel.Equivariant @@ -305,6 +321,9 @@ notation:25 X " β†’β‚‘[" A "] " Y => EquivariantMap A X Y variable {X Y Z : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] [PermSet 𝔸 Z] +instance EquivariantMap.toFunEquivariant (f : X β†’β‚‘[𝔸] Y) : Function.Equivariant 𝔸 f.toFun := + f.equivariant + instance : FunLike (X β†’β‚‘[𝔸] Y) X Y where coe := EquivariantMap.toFun coe_injective' f g h := by cases f; cases g; congr @@ -312,10 +331,10 @@ instance : FunLike (X β†’β‚‘[𝔸] Y) X Y where namespace EquivariantMap /-- The identity function. -/ -def id : X β†’β‚‘[𝔸] X := ⟨_root_.id, id_equivariant π”ΈβŸ© +def id : X β†’β‚‘[𝔸] X := ⟨_root_.id, inferInstance⟩ /-- Function composition. -/ -def comp (f : Y β†’β‚‘[𝔸] Z) (g : X β†’β‚‘[𝔸] Y) : X β†’β‚‘[𝔸] Z := ⟨f ∘ g, comp_equivariant 𝔸 f.equivariant g.equivariant⟩ +def comp (f : Y β†’β‚‘[𝔸] Z) (g : X β†’β‚‘[𝔸] Y) : X β†’β‚‘[𝔸] Z := ⟨f.toFun ∘ g.toFun, inferInstance⟩ @[simp] lemma id_app (x : X) : id 𝔸 x = x := rfl @@ -333,10 +352,6 @@ lemma ext {f g : X β†’β‚‘[𝔸] Y} (h : βˆ€ a, f a = g a) : f = g := end EquivariantMap -/-- Extended setoid definition that also requires the relation to be equivariant. -/ -class EquivariantSetoid (X : Type) [PermSet 𝔸 X] extends Setoid X where - equivariant : Rel.Equivariant 𝔸 r - end BundledFunction /-! @@ -349,7 +364,7 @@ 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 + invFun_equivariant : Function.Equivariant 𝔸 invFun := Function.Equivariant.inv 𝔸 left_inv right_inv def Equivariant.Equiv.symm {𝔸 X Y : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] [PermSet 𝔸 X] [PermSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : EquivariantEquiv 𝔸 Y X := { toFun := equiv.invFun @@ -359,15 +374,24 @@ def Equivariant.Equiv.symm {𝔸 X Y : Type} [Infinite 𝔸] [Countable 𝔸] [D right_inv := equiv.left_inv } +instance EquivariantEquiv.toFunEquivariant + {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] + (equiv : EquivariantEquiv 𝔸 X Y) : Function.Equivariant 𝔸 equiv.toFun := + equiv.toFun_equivariant + +instance EquivariantEquiv.invFunEquivariant + {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] + (equiv : EquivariantEquiv 𝔸 X Y) : Function.Equivariant 𝔸 equiv.invFun := + equiv.invFun_equivariant + /-- 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 +def NominalSet.ofEquivariantEquiv {X Y : Type} [PermSet 𝔸 X] [NominalSet 𝔸 Y] (equiv : EquivariantEquiv 𝔸 X Y) : NominalSet 𝔸 X := + NominalSet.ofEquivariantSurjective 𝔸 equiv.invFun 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 + exact equiv.injective end Equivalence -- cgit v1.3.1