From 0504bfded36c773cde9a252c1ee058e0bcfab6f0 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Mon, 20 Oct 2025 22:23:31 +0200
Subject: prove things about intersections and supports

---
 Nominal/Basic.lean | 75 ++++++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 67 insertions(+), 8 deletions(-)

(limited to 'Nominal/Basic.lean')

diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean
index eb10b44..2858516 100644
--- a/Nominal/Basic.lean
+++ b/Nominal/Basic.lean
@@ -1,5 +1,6 @@
 import Mathlib.Tactic
 import Nominal.Permutations
+import Nominal.Helpers.Finset
 /-!
 # Basic Definitions
 
@@ -18,20 +19,20 @@ variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 /-- A set X equipped with a group action •: (FPerm 𝔸) × X → X. -/
 class PermSet (X : Type) extends MulAction (FPerm 𝔸) X
 
-/-- The set of atoms itself forms a G-Set. -/
+/-- The set of atoms itself forms a (FPerm 𝔸)-Set. -/
 instance : PermSet 𝔸 𝔸 where
   smul π a := π a
   one_smul := by aesop
   mul_smul := by aesop
 
-/-- The set of finite permutations forms a G-Set. -/
+/-- The set of finite permutations forms a (FPerm 𝔸)-Set. -/
 instance : PermSet 𝔸 (FPerm 𝔸) where
   smul π τ := π * τ
   one_smul := by aesop
   mul_smul := by aesop
 
 /-- A discrete (FPerm 𝔸)-Set where permutations do not change anything. -/
-instance PermSet.discrete (X : Type) : PermSet 𝔸 X where
+def PermSet.discrete (X : Type) : PermSet 𝔸 X where
   smul π x := x
   one_smul := by aesop
   mul_smul := by aesop
@@ -68,8 +69,12 @@ def HasSupport (x : X) (S : Set 𝔸) : Prop :=
   fix 𝔸 S ⊆ fix' 𝔸 x
 
 @[simp]
-lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ fix 𝔸 S ⊆ fix' 𝔸 x := by
-  rfl
+lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ ∀ (π : FPerm 𝔸), (∀ x ∈ S, π x = x) → π ∈ fix' 𝔸 x := by
+  constructor
+  · intro hsupp π hπ
+    aesop
+  · intro hsupp π hπ
+    aesop
 
 lemma support_subset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ T → HasSupport 𝔸 x T := by
   intro hS hsub π hπ
@@ -80,6 +85,31 @@ lemma support_subset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ T
 lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by
   sorry
 
+lemma support_sInter {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) := by
+  suffices (C : Finset (Set 𝔸)) : C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C.toSet) ∧ (⋂₀ C.toSet).Finite
+  · intro hfin
+    rw [show C = hfin.toFinset.toSet by simp]
+    intro hne h
+    exact (this hfin.toFinset hne h).left
+  · have : DecidableEq (Set 𝔸) := Classical.typeDecidableEq (Set 𝔸)
+    apply Finset.Nonempty.induction
+    · intro S hS
+      rw [show ⋂₀ ({S} : Finset (Set 𝔸)).toSet = S by simp]
+      apply hS
+      simp
+    · intro S C' hS hC' hsing
+      rw [show (⋂₀ (insert S C' : Finset (Set 𝔸))) = S ∩ (⋂₀ C') by aesop]
+      have hother : (∀ S ∈ C', HasSupport 𝔸 x S ∧ S.Finite) := by
+        intro S' hS'
+        apply hsing
+        exact Finset.mem_insert_of_mem hS'
+      specialize hC' hother
+      specialize hsing S (by simp)
+      constructor
+      · apply support_inter 𝔸 hsing.left hsing.right hC'.left hC'.right
+      · apply Set.Finite.inter_of_left
+        exact hsing.right
+
 end PermSet
 
 end Support
@@ -103,7 +133,7 @@ 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 𝔸 :=
-  ⋂₀ { S : Set 𝔸 | PermSet.HasSupport 𝔸 x S }
+  ⋂₀ { S : Set 𝔸 | PermSet.HasSupport 𝔸 x S ∧ S.Finite }
 
 /-- The least finite support in a nominal set is always finite. -/
 lemma supp_finite {x : X} : (supp 𝔸 x).Finite := by
@@ -114,7 +144,34 @@ lemma supp_finite {x : X} : (supp 𝔸 x).Finite := by
   · grind
 
 /-- The least finite support is itself a support. -/
-lemma supp_is_support {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := sorry
+lemma supp_is_support {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := by
+  obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.finsupp x
+  have suppf : (supp 𝔸 x = ⋂₀ { T : Set 𝔸 | T ⊆ S ∧ PermSet.HasSupport 𝔸 x T ∧ T.Finite }) := by
+    unfold supp; ext a
+    constructor
+    · intro h T hT
+      apply h
+      exact hT.out.right
+    · intro h T hT
+      suffices : a ∈ S ∩ T
+      · apply Set.mem_of_mem_inter_right; assumption
+      · apply h
+        constructor
+        · exact Set.inter_subset_left
+        · constructor
+          · exact PermSet.support_inter 𝔸 hsuppS hfinS hT.out.left hT.out.right
+          · apply Set.Finite.inter_of_left; assumption
+  rw [suppf]
+  apply PermSet.support_sInter
+  · apply Set.Finite.subset
+    · apply Set.Finite.powerset
+      exact hfinS
+    · intro T hT
+      exact hT.out.left
+  · use S
+    exact ⟨by rfl, ⟨hsuppS, hfinS⟩⟩
+  · intro T hT
+    exact hT.right
 
 end NominalSet
 
@@ -131,7 +188,8 @@ instance : NominalSet 𝔸 𝔸 where
 -- TODO: Prove supp a = {a}
 
 /-- Every set can be made into a discrete nominal set where every element has empty support. -/
-instance NominalSet.discrete (X : Type) : NominalSet 𝔸 X where
+def NominalSet.discrete (X : Type) : NominalSet 𝔸 X :=
+{ PermSet.discrete 𝔸 X with
   finsupp := by
     intro x
     use {}
@@ -139,6 +197,7 @@ instance NominalSet.discrete (X : Type) : NominalSet 𝔸 X where
     · intro π hπ
       aesop
     · simp
+}
 
 -- TODO: Prove supp x = ∅
 
-- 
cgit v1.3.1