quotient types as nominal sets

3 files changed, 77 insertions, 3 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 189ca66..0fe9f91 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -31,6 +31,10 @@ def EquivariantSet (S : Set X) : Prop :=
 def EquivariantRelation (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
   constructor
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 2bb389d..2ebe9b1 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -59,7 +59,7 @@ Every set can be made into a discrete nominal set, where supp x = ∅.
 -/
 section Discrete
 
-def NominalSet.discrete (X : Type) : NominalSet.Discrete 𝔸 X where
+def NominalSet.mkDiscrete (X : Type) : NominalSet.Discrete 𝔸 X where
   smul π x := x
   one_smul := by intro; rfl
   mul_smul := by intro _ _ _; rfl
@@ -81,10 +81,10 @@ def NominalSet.discrete (X : Type) : NominalSet.Discrete 𝔸 X where
   simp [IsFresh]
 
 /-- We consider Unit a discrete nominal set. -/
-instance : NominalSet.Discrete 𝔸 Unit := NominalSet.discrete 𝔸 Unit
+instance : NominalSet.Discrete 𝔸 Unit := NominalSet.mkDiscrete 𝔸 Unit
 
 /-- We consider Bool a discrete nominal set. -/
-instance : NominalSet.Discrete 𝔸 Bool := NominalSet.discrete 𝔸 Bool
+instance : NominalSet.Discrete 𝔸 Bool := NominalSet.mkDiscrete 𝔸 Bool
 
 end Discrete
 
@@ -221,3 +221,67 @@ lemma inr_equivariant : Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by
 end Sum
 
 end Coproducts
+
+/-!
+## Quotient Types
+
+If ≈ is an equivariant relation on X × X, then X/≈ is a nominal set with `supp [x] = ⋂₀ {supp y | y ∈ [x]}`.
+-/
+section Quotient
+
+namespace Quotient
+
+variable {X : Type} [PermSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X}
+
+instance : SMul (FPerm 𝔸) (Quotient setoid.toSetoid) where
+  smul π := Quotient.lift (fun x => ⟦π • x⟧) (by
+    intro x y hxy
+    simp only [Quotient.eq]
+    apply setoid.equivariant x y π hxy)
+
+@[simp] lemma smul_quotient (π : FPerm 𝔸) (x : X) : (π • Quotient.mk setoid.toSetoid x) = ⟦π • x⟧ := rfl
+
+instance : PermSet 𝔸 (Quotient setoid.toSetoid) where
+  one_smul := by
+    apply Quotient.ind
+    intro x
+    simp
+  mul_smul := by
+    intro π τ
+    apply Quotient.ind
+    simp [mul_smul]
+
+lemma mk_equivariant : Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by
+  simp [Equivariant]
+
+variable {X : Type} [NominalSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X}
+
+instance : NominalSet 𝔸 (Quotient setoid.toSetoid) :=
+  NominalSet.fromEquivariantSurjective 𝔸 (Quotient.mk setoid.toSetoid) (mk_equivariant 𝔸) mk_surjective
+
+lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid 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' :=
+      Equivariant.supp_subset 𝔸 (mk_equivariant 𝔸)
+    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 𝔸 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)
+    simp only [Finset.mem_union, Set.Finite.mem_toFinset, not_or] at hc
+    use ⸨a, c⸩ • x; constructor
+    · 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]
+      simp only [FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left]
+      exact hc.right
+
+end Quotient
+
+end Quotient
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index a2f8d56..0d6b81c 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -158,6 +158,12 @@ lemma swap_apply_left (a b : X) : ⸨a, b⸩ a = b := by
 lemma swap_apply_right (a b : X) : ⸨a, b⸩ b = a := by
   simp [swap]
 
+/-- Lifting of Equiv.swap_inv to finite permutations. -/
+@[simp]
+lemma swap_inv (a b : X) : ⸨a, b⸩⁻¹ = ⸨a, b⸩ := by
+  apply ext
+  simp [swap]
+
 end FPerm
 
 example : FPerm ℕ := ⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩