diff --git a/Mathlib.lean b/Mathlib.lean index 1e5e2a2ac83c42..42a513cfe0d882 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean index 4bb7639e6fa7b9..ec69caf8594461 100644 --- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean +++ b/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 diff --git a/Mathlib/Combinatorics/Enumerative/Partition/YoungDiagram.lean b/Mathlib/Combinatorics/Enumerative/Partition/YoungDiagram.lean new file mode 100644 index 00000000000000..66642de0bba792 --- /dev/null +++ b/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 diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean index 1cd2854a0ba10b..d10e02861c9842 100644 --- a/Mathlib/Combinatorics/Young/YoungDiagram.lean +++ b/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