The type of grid Young diagrams

def QuotientIsoLmn.GridYoungDiagram (m n : ℕ) : Type

@[implicit_reducible]

instance QuotientIsoLmn.instPartialOrderGridYoungDiagram {m n : ℕ} : PartialOrder (GridYoungDiagram m n)

Maps between L(m,n) and grid Young diagrams

def QuotientIsoLmn.lmnToFinset {m n : ℕ} (p : YoungLattice.Lmn m n) : Finset (Fin m × Fin n)

theorem QuotientIsoLmn.mem_lmnToFinset {m n : ℕ} (p : YoungLattice.Lmn m n) (i : Fin m) (j : Fin n) : (i, j) ∈ lmnToFinset p ↔ ↑j < ↑(↑p i)

theorem QuotientIsoLmn.lmnToFinset_isLeftJustified {m n : ℕ} (p : YoungLattice.Lmn m n) : WreathOrbits.IsLeftJustified (lmnToFinset p)

theorem QuotientIsoLmn.lmnToFinset_rowSize {m n : ℕ} (p : YoungLattice.Lmn m n) (i : Fin m) : WreathOrbits.rowSize (lmnToFinset p) i = ↑(↑p i)

theorem QuotientIsoLmn.lmnToFinset_isGridYoung {m n : ℕ} (p : YoungLattice.Lmn m n) : WreathOrbits.IsGridYoung (lmnToFinset p)

def QuotientIsoLmn.lmnToGridYoung {m n : ℕ} (p : YoungLattice.Lmn m n) : GridYoungDiagram m n

def QuotientIsoLmn.gridYoungToLmn {m n : ℕ} (S : GridYoungDiagram m n) : YoungLattice.Lmn m n

theorem QuotientIsoLmn.gridYoungToLmn_lmnToGridYoung {m n : ℕ} (p : YoungLattice.Lmn m n) : gridYoungToLmn (lmnToGridYoung p) = p

theorem QuotientIsoLmn.lmnToGridYoung_gridYoungToLmn {m n : ℕ} (S : GridYoungDiagram m n) : lmnToGridYoung (gridYoungToLmn S) = S

theorem QuotientIsoLmn.rowSize_le_of_subset {m n : ℕ} {S T : Finset (Fin m × Fin n)} (hST : S ⊆ T) (i : Fin m) : WreathOrbits.rowSize S i ≤ WreathOrbits.rowSize T i

theorem QuotientIsoLmn.gridYoungToLmn_le_iff {m n : ℕ} (S T : GridYoungDiagram m n) : gridYoungToLmn S ≤ gridYoungToLmn T ↔ S ≤ T

noncomputable def QuotientIsoLmn.quotientIsoLmn (m n : ℕ) : GridYoungDiagram m n ≃o YoungLattice.Lmn m n

theorem QuotientIsoLmn.quotient_poset_iso_Lmn (m n : ℕ) : Nonempty (GridYoungDiagram m n ≃o YoungLattice.Lmn m n)

The actual quotient poset B_{R_{mn}}/G_{mn}

def QuotientIsoLmn.wreathSetoid (m n : ℕ) : Setoid (Finset (Fin m × Fin n))

def QuotientIsoLmn.WreathQuotient (m n : ℕ) : Type

theorem QuotientIsoLmn.card_eq_of_sameOrbit {m n : ℕ} {S T : Finset (Fin m × Fin n)} (h : WreathOrbits.SameOrbit S T) : S.card = T.card

def QuotientIsoLmn.wreathQuotientMk {m n : ℕ} (S : Finset (Fin m × Fin n)) : WreathQuotient m n

theorem QuotientIsoLmn.wreathQuotientMk_eq_iff {m n : ℕ} (S T : Finset (Fin m × Fin n)) : wreathQuotientMk S = wreathQuotientMk T ↔ WreathOrbits.SameOrbit S T

theorem QuotientIsoLmn.actOnSet_subset_of_subset {m n : ℕ} (g : WreathOrbits.WreathElem m n) {S T : Finset (Fin m × Fin n)} (h : S ⊆ T) : g.actOnSet S ⊆ g.actOnSet T

theorem QuotientIsoLmn.wreathQuotientMk_actOnSet {m n : ℕ} (g : WreathOrbits.WreathElem m n) (S : Finset (Fin m × Fin n)) : wreathQuotientMk (g.actOnSet S) = wreathQuotientMk S

@[implicit_reducible]

instance QuotientIsoLmn.wreathQuotientPartialOrder {m n : ℕ} : PartialOrder (WreathQuotient m n)

Sorted domination: the key lemma

theorem QuotientIsoLmn.finset_filter_card_eq_sorted_filter_length {m n : ℕ} (S : Finset (Fin m × Fin n)) (p : ℕ → Prop) [DecidablePred p] : {i : Fin m | p (WreathOrbits.rowSize S i)}.card = (List.filter (fun (x : ℕ) => decide (p x)) (WreathOrbits.sortedRowSizes S)).length

Helper: connect Finset.filter.card to the sorted list filter length.

theorem QuotientIsoLmn.card_filter_ge_of_sorted {m n : ℕ} {S : Finset (Fin m × Fin n)} (k : Fin m) (v : ℕ) (hv : v ≤ (WreathOrbits.sortedRowSizes S).getD (↑k) 0) : ↑k + 1 ≤ {i : Fin m | v ≤ WreathOrbits.rowSize S i}.card

Lower bound: ≥ k+1 entries are ≥ v when sorted[k] ≥ v.

theorem QuotientIsoLmn.card_filter_ge_le_of_sorted {m n : ℕ} {T : Finset (Fin m × Fin n)} (k : Fin m) (v : ℕ) (hv : (WreathOrbits.sortedRowSizes T).getD (↑k) 0 < v) : {i : Fin m | v ≤ WreathOrbits.rowSize T i}.card ≤ ↑k

Upper bound: ≤ k entries are ≥ v when sorted[k] < v.

theorem QuotientIsoLmn.sortedRowSizes_le_of_rowSize_le {m n : ℕ} (S T : Finset (Fin m × Fin n)) (h : ∀ (i : Fin m), WreathOrbits.rowSize S i ≤ WreathOrbits.rowSize T i) (k : Fin m) : (WreathOrbits.sortedRowSizes S).getD (↑k) 0 ≤ (WreathOrbits.sortedRowSizes T).getD (↑k) 0

The key sorted domination lemma.

theorem QuotientIsoLmn.canonicalYoung_subset_of_subset {m n : ℕ} {S T : Finset (Fin m × Fin n)} (h : S ⊆ T) : WreathOrbits.canonicalYoung S ⊆ WreathOrbits.canonicalYoung T

If S ⊆ T, then canonicalYoung S ⊆ canonicalYoung T.

theorem QuotientIsoLmn.canonicalYoung_eq_of_sameOrbit {m n : ℕ} {S T : Finset (Fin m × Fin n)} (h : WreathOrbits.SameOrbit S T) : WreathOrbits.canonicalYoung S = WreathOrbits.canonicalYoung T

theorem QuotientIsoLmn.canonicalYoung_sameOrbit {m n : ℕ} (S : Finset (Fin m × Fin n)) : WreathOrbits.SameOrbit S (WreathOrbits.canonicalYoung S)

The order isomorphism WreathQuotient ≃o GridYoungDiagram

noncomputable def QuotientIsoLmn.wreathQuotientToGridYoung {m n : ℕ} : WreathQuotient m n → GridYoungDiagram m n

@[simp]

theorem QuotientIsoLmn.wreathQuotientToGridYoung_mk {m n : ℕ} (S : Finset (Fin m × Fin n)) : wreathQuotientToGridYoung (wreathQuotientMk S) = ⟨WreathOrbits.canonicalYoung S, ⋯⟩

def QuotientIsoLmn.gridYoungToWreathQuotient {m n : ℕ} : GridYoungDiagram m n → WreathQuotient m n

theorem QuotientIsoLmn.gridYoungToWreathQuotient_wreathQuotientToGridYoung {m n : ℕ} (q : WreathQuotient m n) : gridYoungToWreathQuotient (wreathQuotientToGridYoung q) = q

theorem QuotientIsoLmn.wreathQuotientToGridYoung_gridYoungToWreathQuotient {m n : ℕ} (D : GridYoungDiagram m n) : wreathQuotientToGridYoung (gridYoungToWreathQuotient D) = D

theorem QuotientIsoLmn.wreathQuotientToGridYoung_le_iff {m n : ℕ} (a b : WreathQuotient m n) : wreathQuotientToGridYoung a ≤ wreathQuotientToGridYoung b ↔ a ≤ b

noncomputable def QuotientIsoLmn.wreathQuotientIsoGridYoung (m n : ℕ) : WreathQuotient m n ≃o GridYoungDiagram m n

Theorem 6.9 (first part). B_{R_{mn}}/G_{mn} ≃o GridYoungDiagram m n.

noncomputable def QuotientIsoLmn.wreathQuotientIsoLmn (m n : ℕ) : WreathQuotient m n ≃o YoungLattice.Lmn m n

Theorem 6.9. B_{R_{mn}}/G_{mn} ≅ L(m,n). (Theorem 6.9, Stanley's Algebraic Combinatorics)

theorem QuotientIsoLmn.wreathQuotient_iso_Lmn (m n : ℕ) : Nonempty (WreathQuotient m n ≃o YoungLattice.Lmn m n)