Standard Young tableaux

A standard Young tableau of shape μ is a bijective labeling of the cells of μ by Fin μ.card that increases strictly from left to right and from top to bottom. This file defines standard Young tableaux, their finite cardinality standardCount, and transposition. Its underlying labeling is the existing YoungTableau μ type, so the general tableau API applies without converting between parallel representations.

The labels start at zero, following the Fin μ.card convention in the Schur--Weyl roadmap.

References

• W. Fulton, Young Tableaux, Section 1.1.
• Schur--Weyl roadmap, Layer 0.
• Mathlib's Mathlib.Combinatorics.Young.YoungDiagram, for Young diagrams and their transposition.

structure TauCeti.StandardYoungTableau (μ : YoungDiagram) : Type

A standard Young tableau of shape μ is a bijective labeling of its cells by Fin μ.card, strictly increasing along rows and columns.

• toTableau : YoungTableau μ

  The underlying Young tableau.

• row_strict' {i j₁ j₂ : ℕ} (h : j₁ < j₂) (hcell : (i, j₂) ∈ μ) : self.toTableau ⟨(i, j₁), ⋯⟩ < self.toTableau ⟨(i, j₂), hcell⟩

  Labels increase strictly from left to right.

• col_strict' {i₁ i₂ j : ℕ} (h : i₁ < i₂) (hcell : (i₂, j) ∈ μ) : self.toTableau ⟨(i₁, j), ⋯⟩ < self.toTableau ⟨(i₂, j), hcell⟩

  Labels increase strictly from top to bottom.

@[instance_reducible]

instance TauCeti.StandardYoungTableau.instFunLike {μ : YoungDiagram} : FunLike (StandardYoungTableau μ) (↥μ.cells) (Fin μ.card)

Equations

• TauCeti.StandardYoungTableau.instFunLike = { coe := fun (T : TauCeti.StandardYoungTableau μ) => ⇑T.toTableau, coe_injective := ⋯ }

@[simp]

theorem TauCeti.StandardYoungTableau.coe_toTableau {μ : YoungDiagram} (T : StandardYoungTableau μ) : ⇑T.toTableau = ⇑T

The underlying function of a standard Young tableau is its underlying tableau.

@[simp]

theorem TauCeti.StandardYoungTableau.toTableau_apply {μ : YoungDiagram} (T : StandardYoungTableau μ) (c : ↥μ.cells) : T.toTableau c = T c

Evaluating the underlying tableau agrees with evaluating the standard tableau.

theorem TauCeti.StandardYoungTableau.ext {μ : YoungDiagram} {T U : StandardYoungTableau μ} (h : ∀ (c : ↥μ.cells), T c = U c) : T = U

Two standard Young tableaux are equal when all of their entries agree.

theorem TauCeti.StandardYoungTableau.ext_iff {μ : YoungDiagram} {T U : StandardYoungTableau μ} : T = U ↔ ∀ (c : ↥μ.cells), T c = U c

theorem TauCeti.StandardYoungTableau.bijective {μ : YoungDiagram} (T : StandardYoungTableau μ) : Function.Bijective ⇑T

The entries of a standard Young tableau form a bijection.

theorem TauCeti.StandardYoungTableau.injective {μ : YoungDiagram} (T : StandardYoungTableau μ) : Function.Injective ⇑T

The entries of a standard Young tableau are injective.

theorem TauCeti.StandardYoungTableau.surjective {μ : YoungDiagram} (T : StandardYoungTableau μ) : Function.Surjective ⇑T

Every label occurs in a standard Young tableau.

theorem TauCeti.StandardYoungTableau.row_strict {μ : YoungDiagram} (T : StandardYoungTableau μ) {i j₁ j₂ : ℕ} (h : j₁ < j₂) (hcell : (i, j₂) ∈ μ) : T ⟨(i, j₁), ⋯⟩ < T ⟨(i, j₂), hcell⟩

Entries of a standard Young tableau increase strictly from left to right.

theorem TauCeti.StandardYoungTableau.col_strict {μ : YoungDiagram} (T : StandardYoungTableau μ) {i₁ i₂ j : ℕ} (h : i₁ < i₂) (hcell : (i₂, j) ∈ μ) : T ⟨(i₁, j), ⋯⟩ < T ⟨(i₂, j), hcell⟩

Entries of a standard Young tableau increase strictly from top to bottom.

def TauCeti.StandardYoungTableau.transpose {μ : YoungDiagram} (T : StandardYoungTableau μ) : StandardYoungTableau μ.transpose

Transpose a standard Young tableau by swapping its rows and columns while preserving its labels.

Equations

• T.transpose = { toTableau := (TauCeti.StandardYoungTableau.transposeCellEquiv✝ μ).trans (Equiv.trans T.toTableau (finCongr ⋯)), row_strict' := ⋯, col_strict' := ⋯ }

@[simp]

theorem TauCeti.StandardYoungTableau.transpose_apply_val {μ : YoungDiagram} (T : StandardYoungTableau μ) (c : ↥μ.transpose.cells) : ↑(T.transpose c) = ↑(T ⟨(↑c).swap, ⋯⟩)

Transposition preserves the numeric label of each cell.

def TauCeti.StandardYoungTableau.transposeEquiv (μ : YoungDiagram) : StandardYoungTableau μ ≃ StandardYoungTableau μ.transpose

Transposition is an equivalence between standard Young tableaux of conjugate shapes.

Equations

• TauCeti.StandardYoungTableau.transposeEquiv μ = { toFun := TauCeti.StandardYoungTableau.transpose, invFun := TauCeti.StandardYoungTableau.untranspose✝, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.StandardYoungTableau.transposeEquiv_apply {μ : YoungDiagram} (T : StandardYoungTableau μ) : (transposeEquiv μ) T = T.transpose

The forward map of transposeEquiv is tableau transposition.

@[simp]

theorem TauCeti.StandardYoungTableau.transposeEquiv_symm_apply_val {μ : YoungDiagram} (T : StandardYoungTableau μ.transpose) (c : ↥μ.cells) : ↑(((transposeEquiv μ).symm T) c) = ↑(T ⟨(↑c).swap, ⋯⟩)

The inverse transpose equivalence swaps cells while preserving their numeric labels.

@[instance_reducible]

noncomputable instance TauCeti.StandardYoungTableau.instFintype (μ : YoungDiagram) : Fintype (StandardYoungTableau μ)

Standard Young tableaux of a fixed shape form a finite type.

Equations

• TauCeti.StandardYoungTableau.instFintype μ = FunLike.fintype (TauCeti.StandardYoungTableau μ)

noncomputable def TauCeti.standardCount (μ : YoungDiagram) : ℕ

The number of standard Young tableaux of shape μ.

Equations

• TauCeti.standardCount μ = Fintype.card (TauCeti.StandardYoungTableau μ)

theorem TauCeti.standardCount_def (μ : YoungDiagram) : standardCount μ = Fintype.card (StandardYoungTableau μ)

The number of standard Young tableaux is the cardinality of their finite type.

@[simp]

theorem TauCeti.standardCount_transpose (μ : YoungDiagram) : standardCount μ.transpose = standardCount μ

Transposing a Young diagram does not change its number of standard Young tableaux.