Conjugate partitions and dominance

This file defines the conjugate of a natural-number partition by transposing its Young diagram. It proves that conjugation is an involution and reverses the dominance order.

The reversal theorem is the remaining part of the “Orders on partitions” target in Layer 0 of the symmetric-group and Schur–Weyl roadmap. It supplies the order duality used later for the row/column symmetry of Specht modules and permutation modules.

The Young diagrams of the two extreme partitions, which the duality exchanges, are recorded with the partition–diagram correspondence in TauCeti/Combinatorics/Young/Partitions.lean (TauCeti.rowLen_diagramOf_ones_le_one and TauCeti.colLen_diagramOf_indiscrete_le_one).

References

• W. Fulton, Young Tableaux, London Mathematical Society Student Texts 35, §1.1.
• Mathlib PR #42725 (Kim Morrison) — the draft upstream adaptation of the dominance material; the dot-notation Dominates.conjugate and the name and orientation of conjugate_dominates_conjugate_iff follow the form prepared for that PR.

def TauCeti.conjugate {n : ℕ} (μ : n.Partition) : n.Partition

The conjugate of a partition is obtained by transposing its Young diagram.

Equations

• TauCeti.conjugate μ = TauCeti.toPartition (TauCeti.diagramOf μ).transpose ⋯

@[simp]

theorem TauCeti.conjugate_parts {n : ℕ} (μ : n.Partition) : (conjugate μ).parts = ↑(diagramOf μ).transpose.rowLens

The parts of the conjugate partition are the row lengths of the transposed diagram.

@[simp]

theorem TauCeti.diagramOf_conjugate {n : ℕ} (μ : n.Partition) : diagramOf (conjugate μ) = (diagramOf μ).transpose

The Young diagram of the conjugate partition is the transposed Young diagram.

@[simp]

theorem TauCeti.conjugate_conjugate {n : ℕ} (μ : n.Partition) : conjugate (conjugate μ) = μ

Conjugating a partition twice recovers the original partition.

theorem TauCeti.conjugate_parts_sort {n : ℕ} (μ : n.Partition) : ((conjugate μ).parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2) = (diagramOf μ).transpose.rowLens

The decreasing parts of the conjugate partition are the row lengths of the transposed diagram.

theorem TauCeti.Dominates.conjugate {n : ℕ} {μ ν : n.Partition} (h : Dominates μ ν) : Dominates (conjugate ν) (conjugate μ)

Conjugation of partitions reverses dominance. If μ dominates ν, then the conjugate of ν dominates the conjugate of μ.

@[simp]

theorem TauCeti.conjugate_dominates_conjugate_iff {n : ℕ} {μ ν : n.Partition} : Dominates (conjugate μ) (conjugate ν) ↔ Dominates ν μ

Conjugation of partitions reverses dominance: the conjugate of μ dominates the conjugate of ν exactly when ν dominates μ.