From 992aa8fdd40521d2cc7ed4759bce92c912cbeb80 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Mon, 20 Oct 2025 13:13:33 +0200
Subject: further work

---
 Nominal/Basic.lean | 204 ++++++++++++++++++++++++++---------------------------
 1 file changed, 100 insertions(+), 104 deletions(-)

(limited to 'Nominal/Basic.lean')

diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean
index 534759d..eb10b44 100644
--- a/Nominal/Basic.lean
+++ b/Nominal/Basic.lean
@@ -1,123 +1,125 @@
 import Mathlib.Tactic
+import Nominal.Permutations
+/-!
+# Basic Definitions
 
-section Permutations
+This file provides basic definitions for nominal sets.
+-/
 
-variable {X : Type}
+/-!
+## (FPerm 𝔸)-Sets
 
-notation "⸨" a "," b "⸩" => Equiv.swap a b
-
--- The support of a permutation; i.e., the set of elements where the permutation actually maps the element to a different one.
-def Equiv.Perm.supp (π : Equiv.Perm X) : Set X :=
-  {x | π x ≠ x}
-
-@[simp]
-theorem mem_support (π : Equiv.Perm X) (x : X) : x ∈ π.supp ↔ π x ≠ x := by
-  simp [Equiv.Perm.supp]
-
--- The support of the identity function is the empty set.
-lemma supp_one : (1 : Equiv.Perm X).supp = ∅ := by
-  rw [Set.eq_empty_iff_forall_notMem]
-  intro x hx
-  contradiction
-
--- The support of the inverse function is the same as the function's support.
-lemma supp_inv (π : Equiv.Perm X) : π⁻¹.supp = π.supp := by
-  simp [Equiv.Perm.supp, Equiv.Perm.set_support_inv_eq]
-
--- The support of two concatenated permutations is a subset of the individual supports as a union.
-lemma supp_mul_subset (π τ : Equiv.Perm X) : (π * τ).supp ⊆ π.supp ∪ τ.supp := by
-  simp [Equiv.Perm.supp]
-  apply Equiv.Perm.set_support_mul_subset
-
-lemma supp_swap [DecidableEq X] {x y : X} (h : x ≠ y) : ⸨x, y⸩.supp = {x, y} := by
-  ext z
-  by_cases hx : z = x
-  · simpa [hx] using h.symm
-  · by_cases hy : z = y
-    · simpa [Equiv.swap_apply_of_ne_of_ne, hx, hy] using h
-    · simp [Equiv.swap_apply_of_ne_of_ne, hx, hy]
-
--- The group of (finitely supported) permutations.
-def FPerm (X: Type) : Subgroup (Equiv.Perm X) where
-  carrier := {π | π.supp.Finite}
-  mul_mem' {π τ} hπ hτ := by
-    apply (hπ.union hτ).subset
-    exact supp_mul_subset π τ
-  one_mem' := by
-    simp [supp_one]
-  inv_mem' {x} hx := by
-    simp [supp_inv]
-    exact hx
-
-lemma supp_swap_finite [DecidableEq X] (x y : X) : ⸨x, y⸩ ∈ FPerm X := by
-  by_cases hx : x = y
-  · rw [<-Equiv.swap_eq_one_iff] at hx
-    simp [hx]
-  · simp [FPerm, supp_swap hx]
-
-lemma supp_mul_finite {π τ : Equiv.Perm X} (hπ : π ∈ FPerm X) (hτ : τ ∈ FPerm X) : (π * τ) ∈ FPerm X :=
-  (FPerm X).mul_mem hπ hτ
-
-lemma supp_inv_finite {π : Equiv.Perm X} (hπ : π ∈ FPerm X) : π⁻¹ ∈ FPerm X :=
-  (FPerm X).inv_mem hπ
-
--- Since FPerm is a subgroup of Perm, it is also a group.
-instance (X : Type) : Group (FPerm X) :=
-  Subgroup.toGroup (FPerm X)
-
--- Since FPerm is a subset of Perm, we can coerce it into a function.
-instance (X : Type) : CoeFun (FPerm X) (fun _ => X → X) where
-  coe π := (↑π : Equiv.Perm X)
-
-example : FPerm ℕ := ⟨⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩, by simp [supp_swap_finite, supp_mul_finite]⟩
-
-end Permutations
-
-section GSets
+Sets equipped with a permutation operation.
+-/
+section PermSet
 
 variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
--- A G-set is a set X equipped with a group action •: (FPerm 𝔸) × X → X.
-class GSet (X : Type) extends MulAction (FPerm 𝔸) X
+/-- A set X equipped with a group action •: (FPerm 𝔸) × X → X. -/
+class PermSet (X : Type) extends MulAction (FPerm 𝔸) X
 
-instance : GSet 𝔸 𝔸 where
+/-- The set of atoms itself forms a G-Set. -/
+instance : PermSet 𝔸 𝔸 where
   smul π a := π a
   one_smul := by aesop
   mul_smul := by aesop
 
-instance discreteGSet (X : Type) : GSet 𝔸 X where
+/-- The set of finite permutations forms a G-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
   smul π x := x
   one_smul := by aesop
   mul_smul := by aesop
 
-instance : GSet 𝔸 Unit := discreteGSet 𝔸 Unit
-instance : GSet 𝔸 Bool := discreteGSet 𝔸 Bool
+/-- We consider Unit a discrete (FPerm 𝔸)-Set. -/
+instance : PermSet 𝔸 Unit := PermSet.discrete 𝔸 Unit
+
+/-- We consider Bool a discrete (FPerm 𝔸)-Set. -/
+instance : PermSet 𝔸 Bool := PermSet.discrete 𝔸 Bool
+
+end PermSet
+
+/-!
+## Support Definitions
+
+We can define the notion of "supports" on elements of (FPerm 𝔸)-Sets as the atoms which need to be left unchanged to also fix the element.
+-/
+section Support
 
-variable {X : Type} [GSet 𝔸 X]
+variable (𝔸 : Type) {X : Type} [PermSet 𝔸 X]
 
--- The permutations that leave an element x unchanged.
+namespace PermSet
+
+/-- The permutations that leave an element x unchanged. -/
 def fix' (x : X) : Set (FPerm 𝔸) :=
   { π : FPerm 𝔸 | π • x = x }
 
--- The permutations that leave all elements in A unchanged.
+/-- The permutations that leave all elements in A unchanged. -/
 def fix (A : Set X) : Set (FPerm 𝔸) :=
   { π : FPerm 𝔸 | ∀ x ∈ A, π • x = x }
 
--- A set S ⊆ 𝔸 is a support for x if every permutation that fixes S also leaves x unchanged.
+/-- A set S ⊆ 𝔸 is a support for x if every permutation that fixes S also leaves x unchanged. -/
 def HasSupport (x : X) (S : Set 𝔸) : Prop :=
   fix 𝔸 S ⊆ fix' 𝔸 x
 
-end GSets
+@[simp]
+lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ fix 𝔸 S ⊆ fix' 𝔸 x := by
+  rfl
+
+lemma support_subset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ T → HasSupport 𝔸 x T := by
+  intro hS hsub π hπ
+  apply hS
+  intro a
+  aesop
+
+lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by
+  sorry
+
+end PermSet
 
-section NominalSets
+end Support
+
+/-!
+## Basic Nominal Set Definition
+
+Nominal sets are then just G-Sets where all elements are finitely supported.
+-/
+section NominalSet
 
 variable (𝔸 : Type)
 
--- A G-Set X is nominal if every x ∈ X is finitely supported.
-class Nominal (X : Type) extends GSet 𝔸 X where
-  finsupp : ∀ (x : X), ∃ (S : Set 𝔸), HasSupport 𝔸 x S ∧ S.Finite
+/-- A G-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
+
+namespace NominalSet
+
+variable {X : Type} [nom : NominalSet 𝔸 X]
 
-instance : Nominal 𝔸 𝔸 where
+/-- 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 }
+
+/-- The least finite support in a nominal set is always finite. -/
+lemma supp_finite {x : X} : (supp 𝔸 x).Finite := by
+  unfold supp
+  obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.finsupp x
+  apply Set.Finite.subset
+  · exact hfinS
+  · grind
+
+/-- The least finite support is itself a support. -/
+lemma supp_is_support {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := sorry
+
+end NominalSet
+
+/-- The set of atoms is a nominal set, where supp a = {a}. -/
+instance : NominalSet 𝔸 𝔸 where
   finsupp := by
     intro a
     use {a}
@@ -126,7 +128,10 @@ instance : Nominal 𝔸 𝔸 where
       aesop
     · simp
 
-instance discreteNominal (X : Type) : Nominal 𝔸 X 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
   finsupp := by
     intro x
     use {}
@@ -135,21 +140,12 @@ instance discreteNominal (X : Type) : Nominal 𝔸 X where
       aesop
     · simp
 
-instance : Nominal 𝔸 Unit := discreteNominal 𝔸 Unit
-instance : Nominal 𝔸 Bool := discreteNominal 𝔸 Bool
+-- TODO: Prove supp x = ∅
 
-variable {X : Type} [nom : Nominal 𝔸 X]
+/-- We consider Unit a discrete nominal set. -/
+instance : NominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit
 
--- 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 𝔸 | HasSupport 𝔸 x S }
-
--- The least finite support in a nominal set is always finite.
-theorem supp_finite (x : X) : (supp 𝔸 x).Finite := by
-  unfold supp
-  obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.finsupp x
-  apply Set.Finite.subset
-  · exact hfinS
-  · grind
+/-- We consider Bool a discrete nominal set. -/
+instance : NominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool
 
-end NominalSets
+end NominalSet
-- 
cgit v1.3.1