feat(Combinatorics): link Nat.Partition to YoungDiagram

Mathlib.lean

@@ -3551,6 +3551,7 @@ public import Mathlib.Combinatorics.Enumerative.InclusionExclusion
 public import Mathlib.Combinatorics.Enumerative.Partition.Basic
 public import Mathlib.Combinatorics.Enumerative.Partition.GenFun
 public import Mathlib.Combinatorics.Enumerative.Partition.Glaisher
+public import Mathlib.Combinatorics.Enumerative.Partition.YoungDiagram
 public import Mathlib.Combinatorics.Enumerative.Pentagonal
 public import Mathlib.Combinatorics.Enumerative.Schroder
 public import Mathlib.Combinatorics.Enumerative.Stirling

Mathlib/Combinatorics/Enumerative/Partition/Basic.lean

@@ -31,10 +31,6 @@ related results.
 The representation of a partition as a multiset is very handy as multisets are very flexible and
 already have a well-developed API.
 
-## TODO
-
-Link this to Young diagrams.
-
 ## Tags
 
 Partition

Mathlib/Combinatorics/Enumerative/Partition/YoungDiagram.lean

@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2026 Kevin Gomez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Gomez
+-/
+module
+
+public import Mathlib.Combinatorics.Enumerative.Partition.Basic
+public import Mathlib.Combinatorics.Young.YoungDiagram
+
+/-!
+# Young diagram of a partition
+
+This file defines the equivalence between Young diagrams `μ` with cardinality `n` and
+partitions of `n`, where each row of the diagram becomes a part of the partition.
+The two directions are `YoungDiagram.toPartition` and `YoungDiagram.ofPartition`.
+
+Using this equivalence, the conjugate of a partition is also defined. Given the Young
+diagram `μ` representing a partition `λ`, its conjugate `λ'` is the partition obtained
+by flipping `μ` about the main diagonal, i.e. the columns of `μ` are the parts of `λ'`.
+This is implemented here directly via `YoungDiagram.transpose`.
+
+-/
+
+@[expose] public section
+
+namespace YoungDiagram
+
+/-- Convert a Young diagram to a partition. -/
+def toPartition {n : ℕ} (μ : YoungDiagram) (h : μ.card = n) : Nat.Partition n where
+  parts := μ.rowLens
+  parts_pos := μ.pos_of_mem_rowLens _
+  parts_sum := by simp [sum_rowLens_eq_card, h]
+
+/-- Convert a partition to a Young diagram. -/
+def ofPartition {n : ℕ} (p : Nat.Partition n) : YoungDiagram :=
+  ofRowLens
+    (p.parts.sort (· ≥ ·))
+    (Multiset.pairwise_sort p.parts (· ≥ ·)).sortedGE
+
+@[simp]
+theorem rowLens_ofPartition_eq_sort_parts {n : ℕ} (p : Nat.Partition n) :
+    (ofPartition p).rowLens = p.parts.sort (· ≥ ·) := by
+  grind [ofPartition, rowLens_ofRowLens_eq_self, Multiset.mem_sort]
+
+@[simp]
+theorem card_ofPartition {n : ℕ} (p : Nat.Partition n) :
+    (ofPartition p).card = n := by
+  rw [← sum_rowLens_eq_card, rowLens_ofPartition_eq_sort_parts]
+  calc
+    (p.parts.sort (· ≥ ·)).sum
+      = (↑(p.parts.sort (· ≥ ·)) : Multiset ℕ).sum := Multiset.sum_coe _
+    _ = p.parts.sum := by rw [Multiset.sort_eq]
+    _ = n := p.parts_sum
+
+@[simp]
+theorem ofPartition_toPartition {n : ℕ} {μ : YoungDiagram} (h : μ.card = n) :
+    ofPartition (μ.toPartition h) = μ := by
+  simp [ofPartition, toPartition, List.mergeSort_eq_self (· ≥ ·) μ.rowLens_sorted.pairwise,
+    ofRowLens_to_rowLens_eq_self]
+
+@[simp]
+theorem toPartition_ofPartition {n : ℕ} {p : Nat.Partition n} :
+    (ofPartition p).toPartition (card_ofPartition p) = p := by
+  ext
+  simp [toPartition]
+
+/-- Equivalence between Young diagrams of cardinality `n` and partitions of `n`. -/
+def equivPartition {n : ℕ} : { μ : YoungDiagram // μ.card = n } ≃ Nat.Partition n where
+  toFun μ := toPartition μ μ.2
+  invFun p := ⟨ofPartition p, card_ofPartition p⟩
+  left_inv := fun ⟨_, h⟩ => Subtype.mk_eq_mk.mpr (ofPartition_toPartition h)
+  right_inv := fun _ => toPartition_ofPartition
+
+end YoungDiagram
+
+namespace Nat.Partition
+
+/-- Conjugate a partition (equivalent to transposing its Young diagram). -/
+def conjugate {n : ℕ} (p : Partition n) : Partition n :=
+  (YoungDiagram.ofPartition p).transpose.toPartition (by
+    rw [YoungDiagram.card_transpose, YoungDiagram.card_ofPartition]
+  )
+
+/-- Conjugation is an involution. -/
+@[simp]
+theorem conjugate_conjugate {n : ℕ} (p : Partition n) : p.conjugate.conjugate = p := by
+  ext
+  simp [conjugate]
+
+end Nat.Partition

Mathlib/Combinatorics/Young/YoungDiagram.lean

@@ -5,10 +5,12 @@ Authors: Jake Levinson
 -/
 module
 
+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 public import Mathlib.Data.Finset.Preimage
 public import Mathlib.Data.Finset.Prod
 public import Mathlib.Data.SetLike.Basic
 public import Mathlib.Order.UpperLower.Basic
+public import Mathlib.Order.Interval.Finset.Nat
 
 /-!
 # Young diagrams
@@ -234,6 +236,10 @@ protected theorem transpose_mono {μ ν : YoungDiagram} (h_le : μ ≤ ν) : μ.
 def transposeOrderIso : YoungDiagram ≃o YoungDiagram :=
   ⟨⟨transpose, transpose, fun _ => by simp, fun _ => by simp⟩, by simp⟩
 
+@[simp]
+lemma card_transpose (μ : YoungDiagram) : μ.transpose.card = μ.card := by
+  simp [transpose, YoungDiagram.card]
+
 end Transpose
 
 section Rows
@@ -379,6 +385,19 @@ theorem pos_of_mem_rowLens (μ : YoungDiagram) (x : ℕ) (hx : x ∈ μ.rowLens)
   obtain ⟨i, hi, rfl : μ.rowLen i = x⟩ := hx
   rwa [List.mem_range, ← mem_iff_lt_colLen, mem_iff_lt_rowLen] at hi
 
+@[simp]
+lemma sum_rowLens_eq_card (μ : YoungDiagram) : μ.rowLens.sum = μ.card := by
+  have hf : ∀ c ∈ μ.cells, c.1 ∈ Finset.range (μ.colLen 0) := by
+    intro c hc
+    rw [Finset.mem_range, ← YoungDiagram.mem_iff_lt_colLen]
+    exact μ.up_left_mem (le_refl _) (Nat.zero_le _) hc
+  have hr : ∀ i ∈ Finset.range (μ.colLen 0), ({c ∈ μ.cells | c.1 = i}).card = μ.rowLen i := by
+    intro i _hi
+    rw [YoungDiagram.rowLen_eq_card, row]
+  rw [YoungDiagram.card, Finset.card_eq_sum_card_fiberwise hf, Finset.sum_congr rfl hr,
+    YoungDiagram.rowLens, ← List.sum_toFinset, List.toFinset_range]
+  exact List.nodup_range
+
 end RowLens
 
 section EquivListRowLens