Saxl
DefinitionWordSpace(n,d) is the complex vector space of functions from words Fin n → Fin d to ℂ, and the symmetric group Sym(n) acts on it by (g·f)(a)=f(a∘g). For a representation ρ of a group on a complex vector space and a vector v, cyclic(ρ,v) is the subrepresentation spanned by all ρ(g)v. A Tableau of a Young diagram μ with n cells is a bijection from Fin n to the cells of μ, and canonicalTableau fixes one such bijection when the cell count equals n. For a tableau t, rowWord(t) sends each position i to the row index of its cell, viewed as a word with alphabet size equal to the number of rows of μ, and columnGroup(t) is the subgroup of permutations g preserving the column of every position's cell. The polytabloid of t is the sum over g in the column group of sign(g) times g applied to the indicator of rowWord(t) in the word space. The Specht module Specht(t) is the cyclic subrepresentation of the word space generated by this polytabloid, and spechtRep(t) is the resulting Sym(n)-representation. kronecker(a,b,t) is the complex dimension of the space of Sym(n)-equivariant maps from Specht(t) into the tensor product of Specht(a) and Specht(b) under the diagonal action. staircase(m) is the Young diagram of cells (i,j) with i,j<m and i+j<m. SaxlConjecture is a defined proposition, not an established theorem, stating that for every m≥1 and every Young diagram μ with the same number of cells as staircase(m), kronecker of the canonical staircase tableau with itself and a canonical tableau of μ is positive.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/Saxl.lean; bytes 16..4371
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
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μ)
end Saxl
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.