From 5dde77b6db9fc78094363f91e0c6643a84be513e Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Wed, 29 Oct 2025 00:40:13 +0100 Subject: refactor equivariance namespaces --- Nominal/Equivariance.lean | 60 +++++++++++++++++++++++------------------------ 1 file changed, 30 insertions(+), 30 deletions(-) (limited to 'Nominal/Equivariance.lean') diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 3166e71..7087076 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -20,23 +20,19 @@ 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 Equivariant (f : X β†’ Y) : Prop := +def Function.Equivariant (f : X β†’ Y) : Prop := βˆ€ (x : X) (Ο€ : FPerm 𝔸), f (Ο€ β€’ x) = Ο€ β€’ f x /-- A set is equivariant if it is closed under permutations. -/ -def EquivariantSet (S : Set X) : Prop := +def Set.Equivariant (S : Set X) : Prop := βˆ€ (x : X) (Ο€ : FPerm 𝔸), x ∈ S β†’ Ο€ β€’ x ∈ S /-- A binary relation is equivariant if it is closed under permutations. -/ -def EquivariantRelation (R : Rel X Y) : Prop := +def Rel.Equivariant (R : Rel X Y) : Prop := βˆ€ (x : X) (y : Y) (Ο€ : FPerm 𝔸), R x y β†’ R (Ο€ β€’ x) (Ο€ β€’ y) -/-- Extended setoid definition that also requires the relation to be equivariant. -/ -class EquivariantSetoid (X : Type) [PermSet 𝔸 X] extends Setoid X where - equivariant : EquivariantRelation 𝔸 r - /-- For equivariant sets, we even have "if and only if". -/ -lemma equivariant_set_iff {S : Set X} : EquivariantSet 𝔸 S ↔ βˆ€ (x : X) (Ο€ : FPerm 𝔸), x ∈ S ↔ Ο€ β€’ x ∈ S := by +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 @@ -48,7 +44,7 @@ lemma equivariant_set_iff {S : Set X} : EquivariantSet 𝔸 S ↔ βˆ€ (x : X) ( exact (h x Ο€).mp hx /-- For equivariant relations, we even have "if and only if". -/ -lemma equivariant_relation_iff {R : Rel X Y} : EquivariantRelation 𝔸 R ↔ βˆ€ (x : X) (y : Y) (Ο€ : FPerm 𝔸), R x y ↔ R (Ο€ β€’ x) (Ο€ β€’ y) := by +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 @@ -71,18 +67,18 @@ section Trivial variable {X Y Z : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] [PermSet 𝔸 Z] /-- The identity function is equivariant. -/ -lemma id_equivariant : Equivariant 𝔸 (id : X β†’ X) := by - simp [Equivariant] +lemma id_equivariant : Function.Equivariant 𝔸 (id : X β†’ X) := by + simp [Function.Equivariant] /-- The composition of two equivariant functions is equivariant. -/ -lemma comp_equivariant {f : Y β†’ Z} {g : X β†’ Y} : Equivariant 𝔸 f β†’ Equivariant 𝔸 g β†’ Equivariant 𝔸 (f ∘ g) := by +lemma comp_equivariant {f : Y β†’ Z} {g : X β†’ Y} : Function.Equivariant 𝔸 f β†’ Function.Equivariant 𝔸 g β†’ Function.Equivariant 𝔸 (f ∘ g) := by intro hf hg x Ο€ calc f (g (Ο€ β€’ x)) = f (Ο€ β€’ g x) := by rw [hg] _ = Ο€ β€’ (f (g x)) := by rw [hf] /-- The subset relation is equivariant. -/ -lemma subset_equivariant : EquivariantRelation 𝔸 (Set.Subset : Set X β†’ Set X β†’ Prop) := by +lemma Set.subset_equivariant : Rel.Equivariant 𝔸 (Set.Subset : Set X β†’ Set X β†’ Prop) := by 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] @@ -99,7 +95,7 @@ section Support variable {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] -namespace Equivariant +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 @@ -118,10 +114,10 @@ lemma preserve_support_inj {x : X} {f : X β†’ Y} {S : Set 𝔸} : Equivariant have : Ο€ β€’ f x = f x := hsupp hΟ€ contradiction -end Equivariant +end Function.Equivariant /-- HasSupport is an equivariant relation. -/ -lemma PermSet.support_equivariant : EquivariantRelation 𝔸 (HasSupport 𝔸 : X β†’ Set 𝔸 β†’ Prop) := by +lemma PermSet.support_equivariant : Rel.Equivariant 𝔸 (HasSupport 𝔸 : X β†’ Set 𝔸 β†’ Prop) := by intro x S Ο€ hS Οƒ hΟƒ have hfix : (π⁻¹ * Οƒ * Ο€) ∈ fix 𝔸 S := by intro a ha @@ -149,7 +145,7 @@ section Nominal variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] -namespace Equivariant +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 @@ -173,21 +169,21 @@ lemma preserve_fresh_inj {a : 𝔸} {x : X} {f : X β†’ Y} : Equivariant 𝔸 f intro hequi hinj rw [NominalSet.IsFresh, NominalSet.IsFresh, supp_eq_if_inj 𝔸 hequi hinj] -end Equivariant +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 : Equivariant 𝔸 f) (hsurj : Function.Surjective f) : NominalSet 𝔸 Y where +def NominalSet.fromEquivariantSurjective {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y] (f : X β†’ Y) (hequi : 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 Equivariant.preserve_support 𝔸 hequi (supp_is_support 𝔸) + exact Function.Equivariant.preserve_support 𝔸 hequi (supp_is_support 𝔸) Β· exact supp_finite 𝔸 /-- supp is an equivariant function. -/ -lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X β†’ Set 𝔸) := by +lemma NominalSet.supp_equivariant : Function.Equivariant 𝔸 (supp 𝔸 : X β†’ Set 𝔸) := by intro x Ο€; ext a; constructor Β· apply support_subset_supp 𝔸 Β· apply PermSet.support_equivariant @@ -208,7 +204,7 @@ lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X β†’ Set 𝔸 exact hS.out.right /-- Freshness is an equivariant relation. -/ -lemma NominalSet.fresh_equivariant : EquivariantRelation 𝔸 (NominalSet.IsFresh : 𝔸 β†’ X β†’ Prop) := by +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] @@ -221,13 +217,13 @@ For propositions of the form `И a, a R x`, where `R` is an equivariant relation -/ section Freshness -namespace Equivariance +namespace Rel.Equivariant 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₁ : EquivariantRelation 𝔸 R β†’ (И a, R a x) β†’ (βˆƒ a, a # x ∧ R a x) := by +private lemma for_fresh_iff₁ : Equivariant 𝔸 R β†’ (И a, R a x) β†’ (βˆƒ a, a # x ∧ R a x) := by intro hequi h apply Set.Finite.infinite_compl at h simp at h @@ -236,7 +232,7 @@ private lemma for_fresh_iff₁ : EquivariantRelation 𝔸 R β†’ (И a, R a x) simp only [Set.mem_diff, Set.mem_setOf_eq] at ha use a; exact ha.symm -private lemma for_fresh_iffβ‚‚ : EquivariantRelation 𝔸 R β†’ (βˆƒ a, a # x ∧ R a x) β†’ (βˆ€ a, a # x β†’ R a x) := by +private lemma for_fresh_iffβ‚‚ : Equivariant 𝔸 R β†’ (βˆƒ a, a # x ∧ R a x) β†’ (βˆ€ a, a # x β†’ R a x) := by intro hequi h obtain ⟨a, ⟨hfresha, ha⟩⟩ := h intro b hfreshb @@ -245,7 +241,7 @@ private lemma for_fresh_iffβ‚‚ : EquivariantRelation 𝔸 R β†’ (βˆƒ a, a # x rw [NominalSet.fresh_swap_fix 𝔸 hfresha hfreshb] at hmem exact hmem -private lemma for_fresh_iff₃ : EquivariantRelation 𝔸 R β†’ (βˆ€ a, a # x β†’ R a x) β†’ (И a, R a x) := by +private lemma for_fresh_iff₃ : Equivariant 𝔸 R β†’ (βˆ€ a, a # x β†’ R a x) β†’ (И a, R a x) := by intro hequi h have hsub : {a : 𝔸 | R a x}ᢜ βŠ† NominalSet.supp 𝔸 x := by rw [Set.compl_subset_comm] @@ -256,7 +252,7 @@ private lemma for_fresh_iff₃ : EquivariantRelation 𝔸 R β†’ (βˆ€ a, 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 : EquivariantRelation 𝔸 R β†’ ((И a, R a x) ↔ (βˆƒ a, a # x ∧ R a x)) := by +lemma for_fresh_iff_exists : Equivariant 𝔸 R β†’ ((И a, R a x) ↔ (βˆƒ a, a # x ∧ R a x)) := by intro hequi; constructor Β· intro h apply for_fresh_iff₁ 𝔸 hequi @@ -267,7 +263,7 @@ lemma for_fresh_iff_exists : EquivariantRelation 𝔸 R β†’ ((И a, R a x) ↔ ( exact h /-- The quantifier in `И a, a R x` is equivalent to "for all fresh `a`". -/ -lemma for_fresh_iff_all : EquivariantRelation 𝔸 R β†’ ((И a, R a x) ↔ (βˆ€ a, a # x β†’ R a x)) := by +lemma for_fresh_iff_all : Equivariant 𝔸 R β†’ ((И a, R a x) ↔ (βˆ€ a, a # x β†’ R a x)) := by intro hequi; constructor Β· intro h apply for_fresh_iffβ‚‚ 𝔸 hequi @@ -277,7 +273,7 @@ lemma for_fresh_iff_all : EquivariantRelation 𝔸 R β†’ ((И a, R a x) ↔ (βˆ€ apply for_fresh_iff₃ 𝔸 hequi exact h -end Equivariance +end Rel.Equivariant end Freshness @@ -293,7 +289,7 @@ structure EquivariantMap (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] where /-- The underlying function. -/ toFun : X β†’ Y /-- Proof of equivariance. -/ - equivariant : Equivariant 𝔸 toFun + equivariant : Function.Equivariant 𝔸 toFun /-- We write `X β†’β‚‘ Y` or `X β†’β‚‘[𝔸] Y` for an equivariant map X β†’ Y. -/ infixr:25 " β†’β‚‘ " => EquivariantMap _ @@ -331,4 +327,8 @@ 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 -- cgit v1.3.1