add some proofs about specific least supports

1 files changed, 61 insertions, 15 deletions

diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean
index 7bc6e1c..1a7f6ac 100644
--- a/Nominal/Basic.lean
+++ b/Nominal/Basic.lean
@@ -31,17 +31,21 @@ instance : PermSet 𝔸 (FPerm 𝔸) where
   one_smul := by intro; rfl
   mul_smul := by intro _ _ _; rfl
 
+class DiscretePermSet (X : Type) extends PermSet 𝔸 X where
+  is_discrete : ∀ (x : X) (π : FPerm 𝔸), π • x = x
+
 /-- A discrete (FPerm 𝔸)-Set where permutations do not change anything. -/
-def PermSet.discrete (X : Type) : PermSet 𝔸 X where
+def PermSet.discrete (X : Type) : DiscretePermSet 𝔸 X where
   smul π x := x
   one_smul := by intro; rfl
   mul_smul := by intro _ _ _; rfl
+  is_discrete := by intro _ _; rfl
 
 /-- We consider Unit a discrete (FPerm 𝔸)-Set. -/
-instance : PermSet 𝔸 Unit := PermSet.discrete 𝔸 Unit
+instance : DiscretePermSet 𝔸 Unit := PermSet.discrete 𝔸 Unit
 
 /-- We consider Bool a discrete (FPerm 𝔸)-Set. -/
-instance : PermSet 𝔸 Bool := PermSet.discrete 𝔸 Bool
+instance : DiscretePermSet 𝔸 Bool := PermSet.discrete 𝔸 Bool
 
 end PermSet
 
@@ -117,13 +121,13 @@ end Support
 /-!
 ## Basic Nominal Set Definition
 
-Nominal sets are then just G-Sets where all elements are finitely supported.
+Nominal sets are then just (FPerm 𝔸)-Sets where all elements are finitely supported.
 -/
 section NominalSet
 
 variable (𝔸 : Type)
 
-/-- A G-Set X is nominal if every x ∈ X is finitely supported. -/
+/-- An (FPerm 𝔸)-Set X is nominal if every x ∈ X is finitely supported. -/
 class NominalSet (X : Type) extends PermSet 𝔸 X where
   finsupp : ∀ (x : X), ∃ (S : Set 𝔸), PermSet.HasSupport 𝔸 x S ∧ S.Finite
 
@@ -132,7 +136,7 @@ namespace NominalSet
 variable {X : Type} [nom : NominalSet 𝔸 X]
 
 /-- For every element x of a nominal set, there exists a least finite support, denoted "supp x". --/
-noncomputable def supp (x : X) : Set 𝔸 :=
+def supp (x : X) : Set 𝔸 :=
   ⋂₀ { S : Set 𝔸 | PermSet.HasSupport 𝔸 x S ∧ S.Finite }
 
 /-- The least finite support in a nominal set is always finite. -/
@@ -173,38 +177,80 @@ lemma supp_is_support {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := by
   · intro T hT
     exact hT.right
 
+lemma support_subset_supp {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → S.Finite → supp 𝔸 x ⊆ S := by
+  intro hsupp hfin
+  apply Set.sInter_subset_of_mem
+  exact ⟨hsupp, hfin⟩
+
 end NominalSet
 
+private lemma NominalSet.supp_atoms' {a : 𝔸} : PermSet.HasSupport 𝔸 a {a} := by
+  simp [PermSet.fix']
+
 /-- The set of atoms is a nominal set, where supp a = {a}. -/
 instance : NominalSet 𝔸 𝔸 where
   finsupp := by
     intro a
     use {a}
     constructor
-    · intro π hπ
-      aesop
+    · exact NominalSet.supp_atoms' 𝔸
     · simp
 
--- TODO: Prove supp a = {a}
+lemma NominalSet.supp_atoms [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by
+  ext b; constructor
+  · apply support_subset_supp
+    · apply NominalSet.supp_atoms'
+    · simp
+  · suffices : a ∈ supp 𝔸 a
+    -- TODO: Shorten
+    · simp; intro h; rw [h]; assumption
+    · intro S ⟨hsuppS, hfinS⟩
+      by_contra
+      have hfin : ({a} ∪ S).Finite := by
+        apply Set.finite_union.mpr; simp [hfinS]
+      obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset hfin.toFinset
+      have h₁ : c ≠ a := by aesop
+      have h₂ : c ∉ S := by aesop
+      have h₃ : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by
+        intro d hd
+        rw [show ⸨a,c⸩ • d = (Equiv.swap a c) d from rfl]
+        apply Equiv.Perm.supp_notin
+        rw [Equiv.Perm.supp_swap]
+        aesop
+      have h₄ : ⸨a, c⸩ • a = c := by
+        simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl]
+      unfold PermSet.HasSupport at hsuppS
+      specialize hsuppS h₃
+      simp [PermSet.fix'] at hsuppS
+      aesop
+
+class DiscreteNominalSet (X : Type) extends NominalSet 𝔸 X, DiscretePermSet 𝔸 X
+
+private lemma NominalSet.supp_discrete' {X : Type} [disc : DiscretePermSet 𝔸 X] {x : X} : PermSet.HasSupport 𝔸 x ∅ := by
+  intro π hπ
+  simp [PermSet.fix']
+  exact DiscretePermSet.is_discrete x π
 
 /-- Every set can be made into a discrete nominal set where every element has empty support. -/
-def NominalSet.discrete (X : Type) : NominalSet 𝔸 X :=
+def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X :=
 { PermSet.discrete 𝔸 X with
   finsupp := by
     intro x
     use {}
     constructor
-    · intro π hπ
-      aesop
+    · intro π hπ; simp [PermSet.fix']; rfl
     · simp
 }
 
--- TODO: Prove supp x = ∅
+lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
+  rw [← Set.subset_empty_iff]
+  apply Set.sInter_subset_of_mem
+  exact ⟨NominalSet.supp_discrete' 𝔸, Set.finite_empty⟩
 
 /-- We consider Unit a discrete nominal set. -/
-instance : NominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit
+instance : DiscreteNominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit
 
 /-- We consider Bool a discrete nominal set. -/
-instance : NominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool
+instance : DiscreteNominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool
 
 end NominalSet