Hook lengths after erasing a corner

Erasing a corner c from a Young diagram shortens precisely the hooks based strictly to the left of c in its row and strictly above c in its column. The row- and column-length comparisons live with the erasure API in TauCeti.Combinatorics.Young.Corner; this file applies them to hook lengths, proves the three pointwise cases, and packages them as a single conditional formula.

The final product identity rewrites the hook product of the smaller diagram entirely in terms of the hooks of the original diagram. It is the local input needed to combine the corner recursion for standardCount with the hook-product recurrence in the multiplicative hook-length formula.

Main results

• YoungDiagram.IsCorner.rowLen_erase and YoungDiagram.IsCorner.colLen_erase describe the row and column lengths after a corner is erased.
• YoungDiagram.IsCorner.hookLength_erase_of_same_row and YoungDiagram.IsCorner.hookLength_erase_of_same_col say that the affected hooks drop by one.
• YoungDiagram.IsCorner.hookLength_erase is the combined pointwise comparison.
• YoungDiagram.IsCorner.prod_hookLength_erase compares the complete hook products.

References

• B. E. Sagan, The Symmetric Group, Section 3.10.
• Schur--Weyl roadmap, Layer 5: the multiplicative hook-length formula.

Pointwise hook-length comparison

theorem YoungDiagram.IsCorner.hookLength_erase_of_same_row {μ : YoungDiagram} {c d : ℕ × ℕ} (h : μ.IsCorner c) (hd : d ∈ μ.erase c) (hrow : d.1 = c.1) : (μ.erase c).hookLength d + 1 = μ.hookLength d

Erasing a corner decreases by one the hook length of every surviving cell in its row.

theorem YoungDiagram.IsCorner.hookLength_erase_of_same_col {μ : YoungDiagram} {c d : ℕ × ℕ} (h : μ.IsCorner c) (hd : d ∈ μ.erase c) (hcol : d.2 = c.2) : (μ.erase c).hookLength d + 1 = μ.hookLength d

Erasing a corner decreases by one the hook length of every surviving cell in its column.

theorem YoungDiagram.IsCorner.hookLength_erase_of_ne_row_of_ne_col {μ : YoungDiagram} {c d : ℕ × ℕ} (h : μ.IsCorner c) (hrow : d.1 ≠ c.1) (hcol : d.2 ≠ c.2) : (μ.erase c).hookLength d = μ.hookLength d

Erasing a corner leaves unchanged the hook length of a cell outside its row and column.

@[simp]

theorem YoungDiagram.IsCorner.hookLength_erase {μ : YoungDiagram} {c d : ℕ × ℕ} (h : μ.IsCorner c) (hd : d ∈ μ.erase c) : (μ.erase c).hookLength d = if d.1 = c.1 ∨ d.2 = c.2 then μ.hookLength d - 1 else μ.hookLength d

Hook lengths under corner erasure. A surviving hook drops by one exactly when its base cell lies in the erased corner's row or column; every other hook is unchanged.

The hook product after erasure

theorem YoungDiagram.IsCorner.prod_hookLength_erase {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : ∏ d ∈ (μ.erase c).cells, (μ.erase c).hookLength d = ∏ d ∈ μ.cells.erase c, if d.1 = c.1 ∨ d.2 = c.2 then μ.hookLength d - 1 else μ.hookLength d

The hook product after erasing a corner, expressed using only the original diagram: remove the corner's own factor, subtract one from the hooks based in its row or column, and leave all other factors unchanged.