UniversalTensorSquares

Definition

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

WordSpace(n,d) is the complex vector space of functions from words Fin n → Fin d (length-n words over d letters) to ℂ, and wordRep(n,d) is the representation of the symmetric group on n letters in which a permutation g sends a function f to the function a ↦ f(a∘g), that is, it acts by permuting word positions. For a representation ρ and vector v, cyclic(ρ,v) is the subrepresentation spanned over ℂ by all translates ρ(g)v. For a Young diagram μ, a Tableau is a bijection from Fin n onto the cells of μ, and canonicalTableau picks one such bijection when μ has n cells. For a tableau t, rowWord(t) is the word recording the row coordinate of the cell assigned to each position, taking values in Fin(μ.colLen 0), and columnGroup(t) is the subgroup of permutations that preserve the column coordinate of every position. The polytabloid of t is the sum over g in the column group of sign(g) times wordRep applied to g and the indicator function of the word rowWord(t). The Specht module of t is the cyclic subrepresentation of wordRep(n, μ.colLen 0) generated by this polytabloid, with spechtRep its induced symmetric-group representation. Finally kronecker(a,b,t) is the complex dimension of the space of intertwining maps from the Specht representation of t to the tensor product of the Specht representations of a and b, for tableaux a, b, t of shapes α, β, μ on n points. The block also opens an empty UniversalTensorSquares namespace and states no theorem.

Definition code

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/UniversalTensorSquares.lean; bytes 16..2978
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib

namespace OAI

/-! Universal tensor squares of irreducible complex symmetric-group representations. -/

noncomputable section

open scoped TensorProduct

universe uG uV

namespace Saxl

abbrev WordSpace (n d : ℕ) := (Fin n → Fin d) → ℂ

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

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

abbrev Tableau (n : ℕ) (μ : YoungDiagram) := Fin n ≃ μ.cells

def canonicalTableau {n : ℕ} (μ : YoungDiagram) (hn : μ.card = n) : Tableau n μ :=
  (Fintype.equivFinOfCardEq (by simpa using hn)).symm

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)⟩

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

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)

def spechtSub {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :=
  cyclic (wordRep n (μ.colLen 0)) (polytabloid t)

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

def spechtRep {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :
    Representation ℂ (Equiv.Perm (Fin n)) (Specht t) :=
  (spechtSub t).toRepresentation

def kronecker {n : ℕ} {α β μ : YoungDiagram}
    (a : Tableau n α) (b : Tableau n β) (t : Tableau n μ) : ℕ :=
  Module.finrank ℂ (Representation.IntertwiningMap (spechtRep t)
    ((spechtRep a).tprod (spechtRep b)))

end Saxl

namespace UniversalTensorSquares

universe u



end UniversalTensorSquares
end
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/UniversalTensorSquares.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by wurtle · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph