Documentation

Mathlib.Combinatorics.Young.YoungDiagram

Young diagrams #

A Young diagram is a finite set of up-left justified boxes:

□□□□□
□□□
□□□
□

This Young diagram corresponds to the [5, 3, 3, 1] partition of 12.

We represent it as a lower set in ℕ × ℕ in the product partial order. We write (i, j) ∈ μ to say that (i, j) (in matrix coordinates) is in the Young diagram μ.

Main definitions #

Notation #

In "English notation", a Young diagram is drawn so that (i1, j1) ≤ (i2, j2) means (i1, j1) is weakly up-and-left of (i2, j2). This terminology is used below, e.g. in YoungDiagram.up_left_mem.

Tags #

Young diagram

References #

https://en.wikipedia.org/wiki/Young_tableau

theorem YoungDiagram.ext (x : YoungDiagram) (y : YoungDiagram) (cells : x.cells = y.cells) :
x = y
theorem YoungDiagram.ext_iff (x : YoungDiagram) (y : YoungDiagram) :
x = y x.cells = y.cells
structure YoungDiagram :
  • cells : Finset ( × )

    A finite set which represents a finite collection of cells on the ℕ × ℕ grid.

  • isLowerSet : IsLowerSet s.cells

    Cells are up-left justified, witnessed by the fact that cells is a lower set in ℕ × ℕ.

A Young diagram is a finite collection of cells on the ℕ × ℕ grid such that whenever a cell is present, so are all the ones above and to the left of it. Like matrices, an (i, j) cell is a cell in row i and column j, where rows are enumerated downward and columns rightward.

Young diagrams are modeled as finite sets in ℕ × ℕ that are lower sets with respect to the standard order on products.

Instances For
    @[simp]
    theorem YoungDiagram.mem_cells {μ : YoungDiagram} (c : × ) :
    c μ.cells c μ
    @[simp]
    theorem YoungDiagram.mem_mk (c : × ) (cells : Finset ( × )) (isLowerSet : IsLowerSet cells) :
    c { cells := cells, isLowerSet := isLowerSet } c cells
    theorem YoungDiagram.up_left_mem (μ : YoungDiagram) {i1 : } {i2 : } {j1 : } {j2 : } (hi : i1 i2) (hj : j1 j2) (hcell : (i2, j2) μ) :
    (i1, j1) μ

    In "English notation", a Young diagram is drawn so that (i1, j1) ≤ (i2, j2) means (i1, j1) is weakly up-and-left of (i2, j2).

    @[simp]
    theorem YoungDiagram.cells_subset_iff {μ : YoungDiagram} {ν : YoungDiagram} :
    μ.cells ν.cells μ ν
    @[simp]
    theorem YoungDiagram.cells_ssubset_iff {μ : YoungDiagram} {ν : YoungDiagram} :
    μ.cells ν.cells μ < ν
    @[simp]
    theorem YoungDiagram.cells_sup (μ : YoungDiagram) (ν : YoungDiagram) :
    (μ ν).cells = μ.cells ν.cells
    @[simp]
    theorem YoungDiagram.coe_sup (μ : YoungDiagram) (ν : YoungDiagram) :
    ↑(μ ν) = μ ν
    @[simp]
    theorem YoungDiagram.mem_sup {μ : YoungDiagram} {ν : YoungDiagram} {x : × } :
    x μ ν x μ x ν
    @[simp]
    theorem YoungDiagram.cells_inf (μ : YoungDiagram) (ν : YoungDiagram) :
    (μ ν).cells = μ.cells ν.cells
    @[simp]
    theorem YoungDiagram.coe_inf (μ : YoungDiagram) (ν : YoungDiagram) :
    ↑(μ ν) = μ ν
    @[simp]
    theorem YoungDiagram.mem_inf {μ : YoungDiagram} {ν : YoungDiagram} {x : × } :
    x μ ν x μ x ν
    @[simp]
    @[reducible]

    Cardinality of a Young diagram

    Instances For

      The transpose of a Young diagram is obtained by swapping i's with j's.

      Instances For

        Transposing Young diagrams is an OrderIso.

        Instances For

          Rows and row lengths of Young diagrams. #

          This section defines μ.row and μ.rowLen, with the following API: 1. (i, j) ∈ μ ↔ j < μ.rowLen i 2. μ.row i = {i} ×ˢ (Finset.range (μ.rowLen i)) 3. μ.rowLen i = (μ.row i).card 4. ∀ {i1 i2}, i1 ≤ i2 → μ.rowLen i2 ≤ μ.rowLen i1

          Note: #3 is not convenient for defining μ.rowLen; instead, μ.rowLen is defined as the smallest j such that (i, j) ∉ μ.

          The i-th row of a Young diagram consists of the cells whose first coordinate is i.

          Instances For
            theorem YoungDiagram.mem_row_iff {μ : YoungDiagram} {i : } {c : × } :
            c YoungDiagram.row μ i c μ c.fst = i
            theorem YoungDiagram.mk_mem_row_iff {μ : YoungDiagram} {i : } {j : } :
            (i, j) YoungDiagram.row μ i (i, j) μ
            theorem YoungDiagram.exists_not_mem_row (μ : YoungDiagram) (i : ) :
            j, ¬(i, j) μ

            Length of a row of a Young diagram

            Instances For
              theorem YoungDiagram.rowLen_anti (μ : YoungDiagram) (i1 : ) (i2 : ) (hi : i1 i2) :

              Columns and column lengths of Young diagrams. #

              This section has an identical API to the rows section.

              The j-th column of a Young diagram consists of the cells whose second coordinate is j.

              Instances For
                theorem YoungDiagram.mem_col_iff {μ : YoungDiagram} {j : } {c : × } :
                c YoungDiagram.col μ j c μ c.snd = j
                theorem YoungDiagram.mk_mem_col_iff {μ : YoungDiagram} {i : } {j : } :
                (i, j) YoungDiagram.col μ j (i, j) μ
                theorem YoungDiagram.exists_not_mem_col (μ : YoungDiagram) (j : ) :
                i, ¬(i, j) μ.cells

                Length of a column of a Young diagram

                Instances For
                  theorem YoungDiagram.colLen_anti (μ : YoungDiagram) (j1 : ) (j2 : ) (hj : j1 j2) :

                  The list of row lengths of a Young diagram #

                  This section defines μ.rowLens : List, the list of row lengths of a Young diagram μ.

                  1. YoungDiagram.rowLens_sorted : It is weakly decreasing (List.Sorted (· ≥ ·)).
                  2. YoungDiagram.rowLens_pos : It is strictly positive.

                  List of row lengths of a Young diagram

                  Instances For

                    Equivalence between Young diagrams and lists of natural numbers #

                    This section defines the equivalence between Young diagrams μ and weakly decreasing lists w of positive natural numbers, corresponding to row lengths of the diagram: YoungDiagram.equivListRowLens : YoungDiagram ≃ {w : List ℕ // w.Sorted (· ≥ ·) ∧ ∀ x ∈ w, 0 < x}

                    The two directions are YoungDiagram.rowLens (defined above) and YoungDiagram.ofRowLens.

                    The cells making up a YoungDiagram from a list of row lengths

                    Equations
                    Instances For
                      theorem YoungDiagram.mem_cellsOfRowLens {w : List } {c : × } :
                      c YoungDiagram.cellsOfRowLens w h, c.snd < List.get w { val := c.fst, isLt := h }
                      def YoungDiagram.ofRowLens (w : List ) (hw : List.Sorted (fun x x_1 => x x_1) w) :

                      Young diagram from a sorted list

                      Instances For
                        theorem YoungDiagram.mem_ofRowLens {w : List } {hw : List.Sorted (fun x x_1 => x x_1) w} {c : × } :
                        c YoungDiagram.ofRowLens w hw h, c.snd < List.get w { val := c.fst, isLt := h }
                        theorem YoungDiagram.rowLens_length_ofRowLens {w : List } {hw : List.Sorted (fun x x_1 => x x_1) w} (hpos : ∀ (x : ), x w0 < x) :

                        The number of rows in ofRowLens w hw is the length of w

                        theorem YoungDiagram.rowLen_ofRowLens {w : List } {hw : List.Sorted (fun x x_1 => x x_1) w} (i : Fin (List.length w)) :

                        The length of the ith row in ofRowLens w hw is the ith entry of w

                        The left_inv direction of the equivalence

                        theorem YoungDiagram.rowLens_ofRowLens_eq_self {w : List } {hw : List.Sorted (fun x x_1 => x x_1) w} (hpos : ∀ (x : ), x w0 < x) :

                        The right_inv direction of the equivalence

                        @[simp]
                        theorem YoungDiagram.equivListRowLens_symm_apply (ww : { w // List.Sorted (fun x x_1 => x x_1) w ∀ (x : ), x w0 < x }) :
                        YoungDiagram.equivListRowLens.symm ww = YoungDiagram.ofRowLens ww (_ : List.Sorted (fun x x_1 => x x_1) ww)
                        def YoungDiagram.equivListRowLens :
                        YoungDiagram { w // List.Sorted (fun x x_1 => x x_1) w ∀ (x : ), x w0 < x }

                        Equivalence between Young diagrams and weakly decreasing lists of positive natural numbers. A Young diagram μ is equivalent to a list of row lengths.

                        Instances For