refactor equivariance namespaces

1 files changed, 30 insertions, 30 deletions

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