import Mathlib.Tactic
import Nominal.Permutations
/-!
# Basic Definitions

This file provides basic definitions for nominal sets.
-/

/-!
## (FPerm 𝔸)-Sets

Sets equipped with a permutation operation.
-/
section PermSet

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. -/
instance : PermSet 𝔸 𝔸 where
  smul π a := π a
  one_smul := by aesop
  mul_smul := by aesop

/-- 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

/-- 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 (𝔸 : Type) {X : Type} [PermSet 𝔸 X]

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. -/
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

@[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

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 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]

/-- 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}
    constructor
    · intro π hπ
      aesop
    · simp

-- 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 {}
    constructor
    · intro π hπ
      aesop
    · simp

-- TODO: Prove supp x = ∅

/-- We consider Unit a discrete nominal set. -/
instance : NominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit

/-- We consider Bool a discrete nominal set. -/
instance : NominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool

end NominalSet