import Mathlib

/-!
# Finitely supported permutations

This file defines `FPerm`, the subgroup of permutations with finite support.
It also provides basic lemmas about permutation supports and transpositions.
-/

/-!
## Support Definition

Support is defined on Equiv.Perm which also includes infinitely supported permutations.
-/
section Support

variable {X : Type}

namespace Equiv.Perm

/--
The support of a permutation; i.e., the set of elements the permutation actually changes.

Note that, while there is an Equiv.Perm.support, it only works for finite types and thus finite supports.
-/
def supp (π : Equiv.Perm X) : Set X :=
  {x | π x ≠ x}

@[simp]
theorem mem_supp (π : Equiv.Perm X) (x : X) : x ∈ π.supp ↔ π x ≠ x := by rfl

/-- If an element does not occur in the support, the permutation doesn't move it. -/
lemma supp_notin {π : Equiv.Perm X} {x : X} : x ∉ π.supp → π x = x := by
  rw [show (π x = x) ↔ ¬(π x ≠ x) by simp only [ne_eq, not_not]]
  simp [← (mem_supp π x).not]

/-- 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 [supp, set_support_symm_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 only [supp, coe_mul, Function.comp_apply, ne_eq]
  apply set_support_mul_subset

end Equiv.Perm

end Support

/-!
## FPerm Group

The FPerm group is the subgroup of finitely supported permutations.
-/
section Subgroup

/-- 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 Equiv.Perm.supp_mul_subset π τ
  one_mem' := by
    simp [Equiv.Perm.supp_one]
  inv_mem' {x} hx := by
    simp [Equiv.Perm.supp_inv]
    exact hx

variable {X : Type}

namespace FPerm

lemma mem_mul {π τ : Equiv.Perm X} (hπ : π ∈ FPerm X) (hτ : τ ∈ FPerm X) : (π * τ) ∈ FPerm X :=
  (FPerm X).mul_mem hπ hτ

lemma mem_inv {π : Equiv.Perm X} (hπ : π ∈ FPerm X) : π⁻¹ ∈ FPerm X :=
  (FPerm X).inv_mem hπ

end FPerm

/-- Since FPerm is a subset of Equiv.Perm, we can coerce it into a function. -/
instance (X : Type) : CoeFun (FPerm X) (fun _ => X → X) where
  coe π := (↑π : Equiv.Perm X)

end Subgroup

/-!
## Transpositions

Transpositions are a special case of finite permutations, where only (at most) two elements are swapped.
-/
section Transposition

variable {X : Type} [DecidableEq X]

namespace Equiv.Perm

/-- The support of a transposition (x y). -/
lemma supp_swap {x y : X} : (Equiv.swap x y).supp = if x ≠ y then {x, y} else ∅ := by
  by_cases h : x = y
  · simp [h, supp]
  · simp [h]; ext z
    by_cases hx : z = x
    · simp [hx, Ne.symm h]
    · by_cases hy : z = y
      · simp [hy, h]
      · simp [Equiv.swap_apply_of_ne_of_ne, hx, hy]

end Equiv.Perm

namespace FPerm

/-- Extensionality lemma for finite permutations. -/
lemma ext {X : Type} {π₁ π₂ : FPerm X} : π₁.val = π₂.val → π₁ = π₂ := by
  intro h; ext; rw [h]

/-- Transpositions are finite permutations. -/
def swap (x y : X) : FPerm X := ⟨Equiv.swap x y, by
  apply Set.Finite.subset
  · apply ({x, y} : Finset X).finite_toSet
  · by_cases h : x = y <;> all_goals simp [Equiv.Perm.supp_swap, h]⟩

notation "⸨" a "," b "⸩" => FPerm.swap a b

/-- Lifting of Equiv.mul_swap_eq_swap_mul to finite permutations. -/
lemma mul_swap_eq_swap_mul {π : FPerm X} {a b : X} : π * ⸨a, b⸩ = ⸨π a, π b⸩ * π := by
  apply ext
  apply Equiv.mul_swap_eq_swap_mul

/-- Lifting of Equiv.swap_mul_self to finite permutations. -/
lemma swap_mul_self {a b : X} : ⸨a, b⸩ * ⸨a, b⸩ = 1 := by
  apply ext
  simp [swap]

/-- Lifting of Equiv.swap_self to finite permutations.-/
lemma swap_self {a : X} : ⸨a, a⸩ = 1 := by
  ext
  simp [swap]

/-- Lifting of Equiv.swap_comm to finite permutations. -/
lemma swap_comm {a b : X} : ⸨a, b⸩ = ⸨b, a⸩ := by
  apply ext
  simp [swap, Equiv.swap_comm]

/-- Lifting of Equiv.swap_apply_of_ne_of_ne to finite permutations. -/
lemma swap_apply_of_ne_of_ne {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by
  intro ha hb
  simp [swap, Equiv.swap_apply_of_ne_of_ne, ha, hb]

/-- Lifting of Equiv.swap_apply_left to finite permutations. -/
@[simp]
lemma swap_apply_left (a b : X) : ⸨a, b⸩ a = b := by
  simp [swap]

/-- Lifting of Equiv.swap_apply_right to finite permutations. -/
@[simp]
lemma swap_apply_right (a b : X) : ⸨a, b⸩ b = a := by
  simp [swap]

/-- Lifting of Equiv.swap_inv to finite permutations. -/
@[simp]
lemma swap_inv (a b : X) : ⸨a, b⸩⁻¹ = ⸨a, b⸩ := by
  apply ext
  simp [swap]

end FPerm

example : FPerm ℕ := ⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩

end Transposition

/-!
## (FPerm 𝔸)-Sets

Sets equipped with a permutation operation.
-/
section PermSet

/-- A set X equipped with a group action •: (FPerm 𝔸) × X → X. -/
class PermSet (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (X : Type) extends MulAction (FPerm 𝔸) X

variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]

/-- An (FPerm 𝔸)-set is orbit-finite if there are only finitely many different orbits. -/
class OrbitFinite (X : Type) [PermSet 𝔸 X] where
  fin_orbits : Finite (Quotient (MulAction.orbitRel (FPerm 𝔸) X))

/-- The set of atoms itself forms an (FPerm 𝔸)-Set. -/
instance : PermSet 𝔸 𝔸 where
  smul π a := π a
  one_smul := by intro; rfl
  mul_smul := by intro _ _ _; rfl

instance : OrbitFinite 𝔸 𝔸 where
  fin_orbits := Finite.of_equiv Unit
    { toFun _ := Quotient.mk _ (inferInstance : Nonempty 𝔸).some
      invFun _ := ()
      right_inv := by
        let chosen := (inferInstance : Nonempty 𝔸).some
        apply Quotient.ind; intro a
        rw [Quotient.eq]
        show chosen ∈ MulAction.orbit (FPerm 𝔸) a
        use ⸨chosen, a⸩
        exact FPerm.swap_apply_right chosen a
    }

/-- The set of finite permutations forms an (FPerm 𝔸)-Set. -/
instance : PermSet 𝔸 (FPerm 𝔸) where
  smul π τ := π * τ
  one_smul := by intro; rfl
  mul_smul := by intro _ _ _; rfl

open Pointwise

/-- The powerset of an (FPerm 𝔸)-Set forms an (FPerm 𝔸)-Set using pointwise permutation. -/
instance {X : Type} [PermSet 𝔸 X] : PermSet 𝔸 (Set X) where

/-- Simplification for swaps applied to an atom. -/
@[simp] lemma PermSet.atom_swap {a b c : 𝔸} : ⸨a, b⸩ • c = (Equiv.swap a b) c := by rfl

/-- Given x = (a b) y, we also know y = (a b) x. -/
lemma PermSet.swap_switch {X : Type} [PermSet 𝔸 X] {a b : 𝔸} {x y : X} : x = ⸨a, b⸩ • y → y = ⸨a, b⸩ • x := by
  intro h
  have h' : ⸨a, b⸩ • x = ⸨a, b⸩ • ⸨a, b⸩ • y := by congr
  rw [← mul_smul, FPerm.swap_mul_self, one_smul] at h'
  exact h'.symm

/-- If the element is not affected by the swap, membership of it is the same as before the swap. -/
lemma PermSet.atom_set_swap_ne_ne {a b c : 𝔸} {S : Set 𝔸} : c ≠ a → c ≠ b → (c ∈ S ↔ c ∈ ⸨a, b⸩ • S) := by
  intro ha hb
  constructor
  · intro h
    rw [← FPerm.swap_apply_of_ne_of_ne ha hb]
    exact Set.smul_mem_smul_set h
  · intro h
    have h' : ⸨a, b⸩ c ∈ ⸨a, b⸩ • ⸨a, b⸩ • S := Set.smul_mem_smul_set h
    rw [FPerm.swap_apply_of_ne_of_ne ha hb, ← mul_smul, FPerm.swap_mul_self, one_smul] at h'
    exact h'

/-- If an element is swapped, its membership is exactly that of the other element in the swapped set. -/
lemma PermSet.atom_set_swap_left {a b : 𝔸} {S : Set 𝔸} : a ∈ S ↔ b ∈ ⸨a, b⸩ • S := by
  constructor
  · intro h
    have h' : ⸨a, b⸩ a ∈ ⸨a, b⸩ • S := Set.smul_mem_smul_set h
    rw [FPerm.swap_apply_left] at h'
    exact h'
  · intro h
    have h' : ⸨a, b⸩ b ∈ ⸨a, b⸩ • ⸨a, b⸩ • S := Set.smul_mem_smul_set h
    rw [FPerm.swap_apply_right, ← mul_smul, FPerm.swap_mul_self, one_smul] at h'
    exact h'

/-- If an element is swapped, its membership is exactly that of the other element in the swapped set. -/
lemma PermSet.atom_set_swap_right {a b : 𝔸} {S : Set 𝔸} : b ∈ S ↔ a ∈ ⸨a, b⸩ • S := by
  rw [FPerm.swap_comm, atom_set_swap_left]

end PermSet