refactor equivariant props to use type classes

1 files changed, 82 insertions, 29 deletions

diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 7f461ac..dcca75b 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -140,11 +140,11 @@ instance : NominalSet 𝔸 (X × Y) where
 lemma supp_comm {x : X} {y : Y} : NominalSet.supp 𝔸 (x, y) = NominalSet.supp 𝔸 (y, x) := by
   simp; apply Set.union_comm
 
-lemma fst_equivariant : Function.Equivariant 𝔸 (Prod.fst : X × Y → X) := by
-  simp [Function.Equivariant]
+instance instFstEquivariant : Function.Equivariant 𝔸 (Prod.fst : X × Y → X) := by
+  constructor; simp
 
-lemma snd_equivariant : Function.Equivariant 𝔸 (Prod.snd : X × Y → Y) := by
-  simp [Function.Equivariant]
+instance instSndEquivariant : Function.Equivariant 𝔸 (Prod.snd : X × Y → Y) := by
+  constructor; simp
 
 end Prod
 
@@ -212,11 +212,11 @@ instance : NominalSet 𝔸 (X ⊕ Y) where
 @[simp] lemma fresh_inr {a : 𝔸} {y : Y} : a # (.inr y : X ⊕ Y) ↔ a # y := by
   simp [NominalSet.IsFresh]
 
-lemma inl_equivariant : Function.Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by
-  simp [Function.Equivariant]
+instance instInlEquivariant : Function.Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by
+  constructor; simp
 
-lemma inr_equivariant : Function.Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by
-  simp [Function.Equivariant]
+instance instInrEquivariant : Function.Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by
+  constructor; simp
 
 end Sum
 
@@ -231,17 +231,18 @@ section Quotient
 
 namespace Quotient
 
-variable {X : Type} [PermSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X}
+variable {X : Type} [PermSet 𝔸 X] {setoid : Setoid X} [Rel.Equivariant 𝔸 setoid.r]
 
-instance : SMul (FPerm 𝔸) (Quotient setoid.toSetoid) where
+instance : SMul (FPerm 𝔸) (Quotient setoid) where
   smul π := Quotient.lift (fun x => ⟦π • x⟧) (by
     intro x y hxy
     simp only [Quotient.eq]
-    apply setoid.equivariant x y π hxy)
+    rw [← Rel.equivariant 𝔸 setoid.r]
+    exact hxy)
 
-@[simp] lemma smul_quotient (π : FPerm 𝔸) (x : X) : (π • Quotient.mk setoid.toSetoid x) = ⟦π • x⟧ := rfl
+@[simp] lemma smul_quotient (π : FPerm 𝔸) (x : X) : (π • Quotient.mk setoid x) = ⟦π • x⟧ := rfl
 
-instance : PermSet 𝔸 (Quotient setoid.toSetoid) where
+instance : PermSet 𝔸 (Quotient setoid) where
   one_smul := by
     apply Quotient.ind
     intro x
@@ -251,32 +252,33 @@ instance : PermSet 𝔸 (Quotient setoid.toSetoid) where
     apply Quotient.ind
     simp [mul_smul]
 
-lemma mk_equivariant : Function.Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by
-  simp [Function.Equivariant]
+instance instMkEquivariant : Function.Equivariant 𝔸 (Quotient.mk setoid) := by
+  constructor; simp
 
-lemma lift_equivariant
-    {Y : Type} [PermSet 𝔸 Y] (f : X → Y) (h : ∀ (a b : X), a ≈ b → f a = f b) :
-    Function.Equivariant 𝔸 f → Function.Equivariant 𝔸 (Quotient.lift f h) := by
-  intro hequi x π
+def lift_equivariant
+    {Y : Type} [PermSet 𝔸 Y] (f : X → Y) [Function.Equivariant 𝔸 f]
+    (h : ∀ (a b : X), a ≈ b → f a = f b) :
+    Function.Equivariant 𝔸 (Quotient.lift f h) := by
+  constructor; intro x π
   obtain ⟨x', hx'⟩ := x.exists_rep
-  simp [← hx', hequi x' π]
+  simp [← hx', Function.equivariant 𝔸 f]
 
-variable {X : Type} [NominalSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X}
+variable {X : Type} [NominalSet 𝔸 X] {setoid : Setoid X} [Rel.Equivariant 𝔸 setoid.r]
 
-instance : NominalSet 𝔸 (Quotient setoid.toSetoid) :=
-  NominalSet.fromEquivariantSurjective 𝔸 (Quotient.mk setoid.toSetoid) (mk_equivariant 𝔸) mk_surjective
+instance : NominalSet 𝔸 (Quotient setoid) :=
+  NominalSet.ofEquivariantSurjective 𝔸 (Quotient.mk setoid) mk_surjective
 
-lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) = {a | ∀ (x' : X), x' ≈ x → a ∈ NominalSet.supp 𝔸 x'} := by
+lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid x) = {a | ∀ (x' : X), x' ≈ x → a ∈ NominalSet.supp 𝔸 x'} := by
   ext a
   constructor
   · intro ha x' hx'
     rw [← Quotient.sound hx'] at ha
-    have hsub : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x') ⊆ NominalSet.supp 𝔸 x' :=
-      Function.Equivariant.supp_subset 𝔸 (mk_equivariant 𝔸)
+    have hsub : NominalSet.supp 𝔸 (Quotient.mk setoid x') ⊆ NominalSet.supp 𝔸 x' :=
+      Function.Equivariant.supp_subset 𝔸
     exact hsub ha
   · contrapose; intro ha
     simp only [Set.mem_setOf_eq, Classical.not_imp, not_forall]
-    have hfin₁ : (NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x)).Finite := NominalSet.supp_finite 𝔸
+    have hfin₁ : (NominalSet.supp 𝔸 (Quotient.mk setoid x)).Finite := NominalSet.supp_finite 𝔸
     have hfin₂ : (NominalSet.supp 𝔸 x).Finite := NominalSet.supp_finite 𝔸
     -- Show that we can find a fresh c for which (a c) • ⟦x⟧ = ⟦x⟧
     obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset (hfin₁.toFinset ∪ hfin₂.toFinset)
@@ -285,15 +287,66 @@ lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) = {a |
     · apply Quotient.exact
       rw [← smul_quotient]
       exact NominalSet.fresh_swap_fix 𝔸 ha hc.left
-    · rw [NominalSet.supp_equivariant, Set.mem_smul_set_iff_inv_smul_mem]
+    · rw [Function.equivariant 𝔸 (NominalSet.supp 𝔸), Set.mem_smul_set_iff_inv_smul_mem]
       simp only [FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left]
       exact hc.right
 
 /-- If an atom is not in the support of the equivalence class, one can always pick a representative where it is not in the least support. -/
-lemma supp_pick_fresh {a : 𝔸} {x : X} : a ∉ NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) → ∃ (y : X), y ≈ x ∧ a ∉ NominalSet.supp 𝔸 y := by
+lemma supp_pick_fresh {a : 𝔸} {x : X} : a ∉ NominalSet.supp 𝔸 (Quotient.mk setoid x) → ∃ (y : X), y ≈ x ∧ a ∉ NominalSet.supp 𝔸 y := by
   contrapose
   simp [not_exists, not_and, not_not, supp]
 
 end Quotient
 
 end Quotient
+
+/-!
+## Subtypes
+
+If X is a nominal set, Y is a subtype of X, and π • x ∈ Y for all π ∈ FPerm 𝔸 and x ∈ X, then Y is
+also a nominal set.
+-/
+section Subtype
+
+namespace Subtype
+
+variable {X : Type} [PermSet 𝔸 X] {S : Set X} [Set.Equivariant 𝔸 S]
+
+instance : PermSet 𝔸 S where
+  smul π x := ⟨π • x.val, by
+    rw [← Set.equivariant 𝔸 S]
+    exact x.prop⟩
+  one_smul x := by
+    apply Subtype.eq
+    exact MulAction.one_smul x.val
+  mul_smul π τ x := by
+    apply Subtype.eq
+    exact MulAction.mul_smul π τ x.val
+
+@[simp] lemma smul_val (π : FPerm 𝔸) (x : S) : (π • x).val = π • x.val := rfl
+
+instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : S → X) := by
+  constructor; simp
+
+variable {X : Type} [NominalSet 𝔸 X] {S : Set X} [Set.Equivariant 𝔸 S]
+
+instance : NominalSet 𝔸 S where
+  fin_supp x := by
+    use NominalSet.supp 𝔸 x.val
+    constructor
+    · intro π hπ
+      apply Subtype.eq
+      exact NominalSet.supp_is_support 𝔸 hπ
+    · exact NominalSet.supp_finite 𝔸
+
+@[simp] lemma supp {x : S} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.val := by
+  symm
+  apply Function.Equivariant.supp_eq_if_inj
+  exact val_injective
+
+@[simp] lemma fresh {a : 𝔸} {x : S} : a # x ↔ a # x.val := by
+  simp [NominalSet.IsFresh]
+
+end Subtype
+
+end Subtype