Decomposition of L(m+1, n+1)

We decompose Lmn (m+1) (n+1) into a disjoint union based on the last (smallest) part of the partition:

• If the last part is 0, drop it to get an element of Lmn m (n+1).
• If the last part is positive, subtract 1 from all parts to get Lmn (m+1) n.

def YoungLattice.Lmn.shiftDown {m n : ℕ} (p : Lmn (m + 1) (n + 1)) (h : ↑p (Fin.last m) ≠ 0) : Lmn (m + 1) n

Subtract 1 from all parts of a partition whose smallest part is positive.

def YoungLattice.Lmn.shiftUp {m n : ℕ} (q : Lmn (m + 1) n) : Lmn (m + 1) (n + 1)

Add 1 to all parts of a partition.

def YoungLattice.Lmn.restrictToInit {m n : ℕ} (p : Lmn (m + 1) (n + 1)) (_h : ↑p (Fin.last m) = 0) : Lmn m (n + 1)

Restrict an antitone function on Fin (m+1) to Fin m (dropping the last index).

def YoungLattice.Lmn.extendZero {m n : ℕ} (q : Lmn m (n + 1)) : Lmn (m + 1) (n + 1)

Extend a partition by appending 0 as the last (smallest) part.

theorem YoungLattice.Lmn.extendZero_last {m n : ℕ} (q : Lmn m (n + 1)) : ↑q.extendZero (Fin.last m) = 0

theorem YoungLattice.Lmn.shiftUp_last_ne_zero {m n : ℕ} (q : Lmn (m + 1) n) : ↑q.shiftUp (Fin.last m) ≠ 0

noncomputable def YoungLattice.Lmn.sumEquiv (m n : ℕ) : Lmn (m + 1) (n + 1) ≃ Lmn m (n + 1) ⊕ Lmn (m + 1) n

Decomposition: Lmn (m+1) (n+1) ≃ Lmn m (n+1) ⊕ Lmn (m+1) n. Split based on whether the smallest part (at index Fin.last m) is zero or positive.

Cardinality

theorem YoungLattice.Lmn.card_succ_succ (m n : ℕ) : Fintype.card (Lmn (m + 1) (n + 1)) = Fintype.card (Lmn m (n + 1)) + Fintype.card (Lmn (m + 1) n)

theorem YoungLattice.Lmn.card_zero (n : ℕ) : Fintype.card (Lmn 0 n) = 1

theorem YoungLattice.Lmn.card_right_zero (m : ℕ) : Fintype.card (Lmn m 0) = 1

theorem YoungLattice.Lmn.card_eq_choose (m n : ℕ) : Fintype.card (Lmn m n) = (m + n).choose m

Proposition 6.3. The number of partitions fitting in an m × n rectangle equals the binomial coefficient C(m+n, m).