import Mathlib.Tactic

section Permutations

variable {X : Type}

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

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

instance : GSet 𝔸 𝔸 where
  smul π a := π a
  one_smul := by aesop
  mul_smul := by aesop

instance discreteGSet (X : Type) : GSet 𝔸 X where
  smul π x := x
  one_smul := by aesop
  mul_smul := by aesop

instance : GSet 𝔸 Unit := discreteGSet 𝔸 Unit
instance : GSet 𝔸 Bool := discreteGSet 𝔸 Bool

variable {X : Type} [GSet 𝔸 X]

-- 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.
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.
def HasSupport (x : X) (S : Set 𝔸) : Prop :=
  fix 𝔸 S ⊆ fix' 𝔸 x

end GSets

section NominalSets

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

instance : Nominal 𝔸 𝔸 where
  finsupp := by
    intro a
    use {a}
    constructor
    · intro π hπ
      aesop
    · simp

instance discreteNominal (X : Type) : Nominal 𝔸 X where
  finsupp := by
    intro x
    use {}
    constructor
    · intro π hπ
      aesop
    · simp

instance : Nominal 𝔸 Unit := discreteNominal 𝔸 Unit
instance : Nominal 𝔸 Bool := discreteNominal 𝔸 Bool

variable {X : Type} [nom : Nominal 𝔸 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 𝔸 | 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

end NominalSets