The cyclic staircase module inside the tensor square of the staircase Specht module

Definition

OAI_RepresentationTheory_Saxl_CyclicTensor

by Shuze Chen · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

oai-mathrepresentation-theorysymmetric-group

This file contains three general constructions for complex group representations and uses them to place an explicit cyclic module inside the tensor square of the staircase Specht module. Throughout, $G$ is a group, representations are complex vector spaces with a linear $G$ -action, and an intertwiner is a $G$ -equivariant linear map.

Equal subrepresentations. If $S=T$ are equal subrepresentations of a representation, the identity map is an isomorphism of representations $S\cong T$ .
Image of an injective intertwiner. If $f:V\to W$ is an injective intertwiner, then $f$ is an isomorphism of representations from $V$ onto the subrepresentation $f(V)\subseteq W$ .
Pull-back along an injective intertwiner. If $f:V\to W$ is an injective intertwiner and $S\subseteq W$ is a subrepresentation with $S\subseteq f(V)$ , then $f^{-1}|_S:S\to V$ (the inclusion $S\hookrightarrow f(V)$ followed by the inverse of the isomorphism in item 2) is an intertwiner.
The staircase cyclic module and its embedding. Fix $m\in\mathbb{N}$ and let $\delta_m=\{(i,j)\in\mathbb{N}^2: i+j<m\}$ be the staircase diagram, with $n=|\delta_m|=m(m+1)/2$ cells and $m$ rows. Write $[d]=\{0,\dots,d-1\}$ . The symmetric group $S_n$ acts on the word space $W_{n,d}$ of functions $x$ on words $a:[n]\to[d]$ by permuting positions, $(g\cdot x)(a)=x(a\circ g)$ . Let $T$ be the fixed canonical tableau of $\delta_m$ (a bijection from the positions $[n]$ to the cells) and $T'$ the transposed tableau, which puts position $p$ at the transpose of the cell $T(p)$ . Write $e_T,e_{T'}\in W_{n,m}$ for their polytabloids (signed sums, over the column-preserving permutations, of the indicator of the row word) and $S^{\delta_m}$ for the Specht module spanned by the $S_n$ -orbit of $e_T$ ; both polytabloids lie in $S^{\delta_m}$ . Reading a word over the pair alphabet $[m]\times[m]$ as a pair of words $(a,b)$ identifies $W_{n,m}\otimes W_{n,m}\cong W_{n,m^2}$ via $x\otimes y\mapsto\bigl((a,b)\mapsto x(a)\,y(b)\bigr)$ . The staircase cyclic module is

C_m=\operatorname{span}_{\mathbb{C}}\{\,g\cdot(e_{T'}\otimes e_T): g\in S_n\,\}\subseteq W_{n,m^2},

and the composite $S^{\delta_m}\otimes S^{\delta_m}\hookrightarrow W_{n,m}\otimes W_{n,m}\cong W_{n,m^2}$ is an injective intertwiner for the diagonal action whose image contains $C_m$ . Item 3 then gives an injective intertwiner

\Psi_m:C_m\longrightarrow S^{\delta_m}\otimes S^{\delta_m}.

Cyclic form of the staircase Saxl statement. The proposition $\mathrm{CS}$ asserts: for every $m\ge1$ and every Young diagram $\mu$ with $|\mu|=|\delta_m|$ , there is a nonzero intertwiner $S^\mu\to C_m$ , where $S^\mu$ is the Specht module of $\mu$ built from its fixed canonical tableau on the positions $[n]$ .

Because $\Psi_m$ is injective, composing with it turns a nonzero intertwiner $S^\mu\to C_m$ into a nonzero intertwiner $S^\mu\to S^{\delta_m}\otimes S^{\delta_m}$ . Hence $\mathrm{CS}$ implies that every Specht module of size $m(m+1)/2$ occurs in the tensor square of the staircase Specht module, which is the Kronecker-multiplicity form of the Saxl conjecture for staircases. The advantage of $C_m$ is that it is generated by the single explicit vector $e_{T'}\otimes e_T$ , so occurrences of $S^\mu$ can be certified by computations with that vector.

Formalization Note The items are equivOfSubrepEq, intertwiningRangeEquiv, intertwiningLiftSubrep, staircaseToTensor m and CyclicSaxlConjecture; $C_m$ is staircaseCyclic m. Letters of $[m]\times[m]$ are encoded in Fin (m*m) by finProdFinEquiv, the number of rows $m$ appears as (staircase m).colLen 0, and the two lifted maps are marked irreducible.

Definition code

-- Generated from openai/math@1581d4c lean/OAI/RepresentationTheory/Saxl/CyclicTensor.lean by skeleton subtraction
-- (upload_full_project.md Phase 3): Definitions bundle for the Saxl mission closure.
-- Kept: reachable definitions/instances and the theorems their bodies or the node statements cite.
-- Project imports rewritten to platform modules; otherwise byte-identical to the source.
import Mathlib
import Definitions.Def_Saxl
import Definitions.Def_OAI_RepresentationTheory_Saxl_Basic
import Definitions.Def_OAI_RepresentationTheory_Saxl_Polytabloid
import Definitions.Def_OAI_RepresentationTheory_Saxl_SpechtSubmodule
import Definitions.Def_OAI_RepresentationTheory_Saxl_SpechtDuality
import Definitions.Def_OAI_RepresentationTheory_Saxl_TableauTransport
import Definitions.Def_OAI_RepresentationTheory_Saxl_StaircaseTensor
import Definitions.Def_OAI_RepresentationTheory_Saxl_HighProjection
import Definitions.Def_OAI_RepresentationTheory_Saxl_CoordinateSector
import Definitions.Def_OAI_RepresentationTheory_Saxl_PositionSplit
import Definitions.Def_OAI_RepresentationTheory_Saxl_BandFactorization
import Definitions.Def_OAI_RepresentationTheory_Saxl_PathAlternation
import Definitions.Def_OAI_RepresentationTheory_Saxl_BandMatrices
import Definitions.Def_OAI_RepresentationTheory_Saxl_PathContraction
import Definitions.Def_OAI_RepresentationTheory_Saxl_ColumnContraction
import Definitions.Def_OAI_RepresentationTheory_Saxl_BandPairing
import Definitions.Def_OAI_RepresentationTheory_Saxl_CyclicSector
import Definitions.Def_OAI_RepresentationTheory_Saxl_BandSupport
import Definitions.Def_OAI_RepresentationTheory_Saxl_ShapeRigidity
import Definitions.Def_OAI_RepresentationTheory_Saxl_SpechtClassification
import Definitions.Def_OAI_RepresentationTheory_Saxl_SupportSeparation
import Definitions.Def_OAI_RepresentationTheory_Saxl_PositionTensor
import Definitions.Def_OAI_RepresentationTheory_Saxl_BandOrbit
import Definitions.Def_OAI_RepresentationTheory_Saxl_BandGlue
import Definitions.Def_OAI_RepresentationTheory_Saxl_SignEquivalence
import Definitions.Def_OAI_RepresentationTheory_Saxl_PieriRestriction
import Definitions.Def_OAI_RepresentationTheory_Saxl_StripExtension
import Definitions.Def_OAI_RepresentationTheory_Saxl_SizedStrips
import Definitions.Def_OAI_RepresentationTheory_Saxl_HorizontalRemoval
import Definitions.Def_OAI_RepresentationTheory_Saxl_YoungRule

namespace OAI

noncomputable section

open scoped TensorProduct

universe uG uX uY

namespace Saxl

def equivOfSubrepEq {G : Type uG} {X : Type uX} [Group G] [AddCommGroup X] [Module ℂ X]
    {ρ : Representation ℂ G X} (S T : Subrepresentation ρ) (h : S = T) :
    Representation.Equiv S.toRepresentation T.toRepresentation := by
  subst T
  exact Representation.Equiv.refl _

/- Positive Young rule as a concrete orbit map (including reordered contents). -/
def intertwiningRangeEquiv {G : Type uG} {X : Type uX} {Y : Type uY} [Group G] [AddCommGroup X] [Module ℂ X]
    [AddCommGroup Y] [Module ℂ Y] {ρ : Representation ℂ G X} {σ : Representation ℂ G Y}
    (f : Representation.IntertwiningMap ρ σ) (hf : Function.Injective f) :
    ρ.Equiv f.range.toRepresentation where
  toLinearEquiv := LinearEquiv.ofInjective f.toLinearMap hf
  isIntertwining' g := by
    apply LinearMap.ext
    intro x
    apply Subtype.ext
    exact LinearMap.congr_fun (f.isIntertwining' g) x

def intertwiningLiftSubrep {G : Type uG} {X : Type uX} {Y : Type uY} [Group G] [AddCommGroup X] [Module ℂ X]
    [AddCommGroup Y] [Module ℂ Y] {ρ : Representation ℂ G X} {σ : Representation ℂ G Y}
    (f : Representation.IntertwiningMap ρ σ) (hf : Function.Injective f)
    (S : Subrepresentation σ) (hS : S ≤ f.range) :
    Representation.IntertwiningMap S.toRepresentation ρ := by
  let e : ρ.Equiv f.range.toRepresentation := intertwiningRangeEquiv f hf
  let i : Representation.IntertwiningMap S.toRepresentation f.range.toRepresentation :=
    { toLinearMap := Submodule.inclusion hS, isIntertwining' := fun _ => rfl }
  exact e.symm.toIntertwiningMap.comp i

attribute [irreducible] intertwiningLiftSubrep

/- The genuine cyclic module is embedded in the actual staircase Specht square. -/
def staircaseToTensor (m : ℕ) :
    Representation.IntertwiningMap (staircaseCyclic m).toRepresentation
      ((spechtRep (stairTableau m)).tprod (spechtRep (stairTableau m))) :=
  @intertwiningLiftSubrep (Equiv.Perm (Fin (staircase m).card))
    (Specht (stairTableau m) ⊗[ℂ] Specht (stairTableau m))
    (WordSpace (staircase m).card ((staircase m).colLen 0 * (staircase m).colLen 0))
    _ _ _ _ _
    ((spechtRep (stairTableau m)).tprod (spechtRep (stairTableau m)))
    (wordRep (staircase m).card ((staircase m).colLen 0 * (staircase m).colLen 0))
    (staircaseTensorMap m) (staircaseTensorMap_injective m)
    (staircaseCyclic m) (staircaseCyclic_le_tensorRange m)

attribute [irreducible] staircaseToTensor

/- Every Specht type occurs in the specified staircase cyclic module. -/
def CyclicSaxlConjecture : Prop :=
  ∀ m, 1 ≤ m → ∀ (μ : YoungDiagram) (hμ : μ.card = (staircase m).card),
    ∃ f : Representation.IntertwiningMap (spechtRep (canonicalTableau μ hμ))
      (staircaseCyclic m).toRepresentation, f ≠ 0

/- A proof of cyclic support proves the original Kronecker-multiplicity target. -/
end Saxl

end

end OAI

Source

https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/OAI/RepresentationTheory/Saxl/CyclicTensor.lean

View graph