OAI.UniversalTensorSquares.universal_tensor_square
OpenThe theorem states that for every natural number n>0 with n different from 2, 4 and 9, there is a Young diagram λ with n cells such that three things hold. First, for every Young diagram ν with n cells, the Kronecker coefficient of (λ,λ,ν) is positive; here, using the canonical tableaux (arbitrary but fixed bijections from {0,…,n-1} to the cells), this coefficient is the complex dimension of the space of S_n-equivariant linear maps from the Specht representation of ν into the tensor product of the Specht representation of λ with itself, so every irreducible Specht representation of S_n occurs in the tensor square of λ's Specht representation. Second, the Specht representation of λ is irreducible; it is defined as the cyclic subrepresentation, inside the permutation representation on functions from Fin n to Fin(number of rows of λ), generated by the polytabloid, a signed sum over the column-stabilizing subgroup of translates of the indicator of the row-index word. Third, for every finite-dimensional complex irreducible representation ρ of the symmetric group S_n on Fin n, on any module V in the stated universe, there exists an injective S_n-equivariant linear map from ρ into the tensor square of the Specht representation of λ, so this tensor square contains a copy of every irreducible representation.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/UniversalTensorSquares.lean; bytes 2978..3810 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_UniversalTensorSquares namespace OAI noncomputable section open scoped TensorProduct universe uG uV namespace UniversalTensorSquares universe u
theorem universal_tensor_square
(n : ℕ) (hn : 0 < n) (h2 : n ≠ 2) (h4 : n ≠ 4) (h9 : n ≠ 9) :
∃ (lam : YoungDiagram) (hlam : lam.card = n),
(∀ (ν : YoungDiagram) (hν : ν.card = n),
0 < Saxl.kronecker (Saxl.canonicalTableau lam hlam)
(Saxl.canonicalTableau lam hlam) (Saxl.canonicalTableau ν hν)) ∧
Representation.IsIrreducible (Saxl.spechtRep (Saxl.canonicalTableau lam hlam)) ∧
∀ (V : Type u) [AddCommGroup V] [Module ℂ V] [Module.Finite ℂ V]
(ρ : Representation ℂ (Equiv.Perm (Fin n)) V) [Representation.IsIrreducible ρ],
∃ F : Representation.IntertwiningMap ρ
((Saxl.spechtRep (Saxl.canonicalTableau lam hlam)).tprod
(Saxl.spechtRep (Saxl.canonicalTableau lam hlam))),
Function.Injective F := by
sorry
end UniversalTensorSquares
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.