import Mathlib

namespace OAI

noncomputable section

open scoped TensorProduct

universe uG uV

namespace Saxl

/- Coefficients of position tensors on an alphabet of size `d`. -/
abbrev WordSpace (n d : ℕ) := (Fin n → Fin d) → ℂ

/- The position action satisfies `g e_a = e_(a ∘ g⁻¹)`. -/
def wordRep (n d : ℕ) : Representation ℂ (Equiv.Perm (Fin n)) (WordSpace n d) where
  toFun g :=
    { toFun := fun f a => f (a ∘ g)
      map_add' := by intros; rfl
      map_smul' := by intros; rfl }
  map_one' := by ext f a; rfl
  map_mul' g h := by ext f a; rfl

/- The cyclic subrepresentation generated by an actual vector. -/
def cyclic {G : Type uG} {V : Type uV} [Group G] [AddCommGroup V] [Module ℂ V]
    (ρ : Representation ℂ G V) (v : V) : Subrepresentation ρ where
  toSubmodule := Submodule.span ℂ (Set.range fun g : G => ρ g v)
  apply_mem_toSubmodule g := by
    intro x hx
    induction hx using Submodule.span_induction with
    | mem x hx =>
      obtain ⟨h, rfl⟩ := hx
      apply Submodule.subset_span
      exact ⟨g * h, by simp only [map_mul, Module.End.mul_apply]⟩
    | zero => simp
    | add x y hx hy ihx ihy =>
      simpa only [map_add] using Submodule.add_mem _ ihx ihy
    | smul a x hx ih =>
      simpa only [map_smul] using Submodule.smul_mem _ a ih

/- A tableau is an enumeration of all cells by the position set. -/
abbrev Tableau (n : ℕ) (μ : YoungDiagram) := Fin n ≃ μ.cells

/- One fixed tableau; changing its enumeration gives an isomorphic Specht module. -/
def canonicalTableau {n : ℕ} (μ : YoungDiagram) (hn : μ.card = n) : Tableau n μ :=
  (Fintype.equivFinOfCardEq (by simpa using hn)).symm

/- The row word corresponding to the tabloid of a tableau. -/
def rowWord {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) : Fin n → Fin (μ.colLen 0) :=
  fun i => ⟨(t i).val.1, YoungDiagram.mem_iff_lt_colLen.mp
    (μ.up_left_mem le_rfl (Nat.zero_le _) (t i).property)⟩

/- The column permutations of a tableau. -/
def columnGroup {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :
    Subgroup (Equiv.Perm (Fin n)) where
  carrier := {g | ∀ i, (t (g i)).val.2 = (t i).val.2}
  one_mem' := by intro i; rfl
  mul_mem' := by
    intro g h hg hh i
    exact (hg (h i)).trans (hh i)
  inv_mem' := by
    intro g hg i
    have h := hg (g⁻¹ i)
    simpa using h.symm

/- The standard column-antisymmetrized row tabloid, with complex coefficients. -/
def polytabloid {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :
    WordSpace n (μ.colLen 0) := by
  classical
  letI := Fintype.ofFinite (columnGroup t)
  exact ∑ g : columnGroup t,
    (((Equiv.Perm.sign (g : Equiv.Perm (Fin n))) : ℤ) : ℂ) •
      wordRep n (μ.colLen 0) (g : Equiv.Perm (Fin n)) (Pi.single (rowWord t) 1)

/- The Specht module, defined as the orbit span of a polytabloid in the
row-tabloid permutation module, realized inside the word space. -/
def spechtSub {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :=
  cyclic (wordRep n (μ.colLen 0)) (polytabloid t)

abbrev Specht {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :=
  (spechtSub t).toSubmodule

/- The genuine symmetric-group representation on the complex Specht module. -/
def spechtRep {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :
    Representation ℂ (Equiv.Perm (Fin n)) (Specht t) :=
  (spechtSub t).toRepresentation

/- Kronecker multiplicity is the complex dimension of Hom, with the
diagonal symmetric-group action on the tensor product. -/
def kronecker {n : ℕ} {α β μ : YoungDiagram}
    (a : Tableau n α) (b : Tableau n β) (t : Tableau n μ) : ℕ :=
  Module.finrank ℂ (Representation.IntertwiningMap (spechtRep t)
    ((spechtRep a).tprod (spechtRep b)))


def staircase (m : ℕ) : YoungDiagram where
  cells := ((Finset.range m) ×ˢ (Finset.range m)).filter (fun x => x.1 + x.2 < m)
  isLowerSet := by
    intro x y hxy hy
    simp only [Finset.mem_coe, Finset.mem_filter, Finset.mem_product,
      Finset.mem_range] at hy ⊢
    exact ⟨⟨lt_of_le_of_lt hxy.1 hy.1.1, lt_of_le_of_lt hxy.2 hy.1.2⟩,
      lt_of_le_of_lt (Nat.add_le_add hxy.1 hxy.2) hy.2⟩


def SaxlConjecture : Prop :=
  ∀ (m : ℕ), 1 ≤ m → ∀ (μ : YoungDiagram) (hμ : μ.card = (staircase m).card),
    0 < kronecker (canonicalTableau (staircase m) rfl)
      (canonicalTableau (staircase m) rfl) (canonicalTableau μ hμ)

theorem saxl_conjecture : SaxlConjecture := by
  sorry

end Saxl

end

end OAI