The wreath product as a subgroup of Perm (Fin (m * n))

noncomputable def YoungLattice.Lmn.wreathElemToPerm {m n : ℕ} (g : WreathOrbits.WreathElem m n) : Equiv.Perm (Fin m × Fin n)

Convert a WreathElem m n to an Equiv.Perm (Fin m × Fin n).

noncomputable def YoungLattice.Lmn.wreathSubgroup (m n : ℕ) : Subgroup (Equiv.Perm (Fin (m * n)))

The wreath product S_n ≀ S_m embedded as a subgroup of Perm (Fin (m * n)). Each WreathElem m n acts on Fin m × Fin n by (i, j) ↦ (σ i, τ_i j). Via finProdFinEquiv : Fin m × Fin n ≃ Fin (m * n), this gives a permutation of Fin (m * n). The subgroup is the image of the wreath product.

Bridge: QuotientPoset (m*n) (wreathSubgroup m n) ≃o WreathQuotient m n

theorem YoungLattice.Lmn.wreathElemToPerm_apply {m n : ℕ} (g : WreathOrbits.WreathElem m n) (p : Fin m × Fin n) : (wreathElemToPerm g) p = g.actOn p

theorem YoungLattice.Lmn.sum_rowSize_eq_card {m n : ℕ} (S : Finset (Fin m × Fin n)) : ∑ i : Fin m, WreathOrbits.rowSize S i = S.card

The sum of row sizes equals the cardinality of a finset on a product type.

theorem YoungLattice.Lmn.image_finProdFinEquiv_actOnSet {m n : ℕ} (g : WreathOrbits.WreathElem m n) (S : Finset (Fin m × Fin n)) : Finset.image (⇑finProdFinEquiv) (g.actOnSet S) = finProdFinEquiv.permCongr (wreathElemToPerm g) • Finset.image (⇑finProdFinEquiv) S

Image of actOnSet through finProdFinEquiv equals smul.

theorem YoungLattice.Lmn.smul_image_symm_eq_actOnSet {m n : ℕ} (g : WreathOrbits.WreathElem m n) (A : Finset (Fin (m * n))) : Finset.image (⇑finProdFinEquiv.symm) (finProdFinEquiv.permCongr (wreathElemToPerm g) • A) = g.actOnSet (Finset.image (⇑finProdFinEquiv.symm) A)

smul action pulled back by finProdFinEquiv.symm = actOnSet.

theorem YoungLattice.Lmn.wreathSubgroup_orbit_of_sameOrbit {m n : ℕ} (S T : Finset (Fin m × Fin n)) (h : WreathOrbits.SameOrbit S T) : ∃ (g : ↥(wreathSubgroup m n)), g • Finset.image (⇑finProdFinEquiv) S = Finset.image (⇑finProdFinEquiv) T

Forward: Wreath orbit → wreathSubgroup-orbit.

theorem YoungLattice.Lmn.sameOrbit_of_wreathSubgroup_orbit {m n : ℕ} (A : Finset (Fin (m * n))) (g : ↥(wreathSubgroup m n)) : WreathOrbits.SameOrbit (Finset.image (⇑finProdFinEquiv.symm) A) (Finset.image (⇑finProdFinEquiv.symm) (g • A))

Backward: wreathSubgroup-orbit → wreath orbit (closure induction).

noncomputable def YoungLattice.Lmn.quotientPosetEquivWreathQuotient (m n : ℕ) : SpernerProperty.QuotientPoset (m * n) (wreathSubgroup m n) ≃ QuotientIsoLmn.WreathQuotient m n

The bridge equivalence between QuotientPoset and WreathQuotient.

noncomputable def YoungLattice.Lmn.quotientPosetIsoWreathQuotient (m n : ℕ) : SpernerProperty.QuotientPoset (m * n) (wreathSubgroup m n) ≃o QuotientIsoLmn.WreathQuotient m n

The bridge is an order isomorphism.

theorem YoungLattice.Lmn.sumParts_gridYoungToLmn {m n : ℕ} (S : QuotientIsoLmn.GridYoungDiagram m n) : (QuotientIsoLmn.gridYoungToLmn S).sumParts = (↑S).card

sumParts (gridYoungToLmn S) = S.val.card.

theorem YoungLattice.Lmn.grade_composed_iso {m n : ℕ} (A : Finset (Fin (m * n))) : grade ℕ ((QuotientIsoLmn.wreathQuotientIsoLmn m n) (QuotientIsoLmn.wreathQuotientMk (Finset.image (⇑finProdFinEquiv.symm) A))) = A.card

The composed isomorphism preserves grades.

Grade-preserving order isomorphism: QuotientPoset ≃o Lmn

noncomputable def YoungLattice.Lmn.quotientPosetIsoLmn (m n : ℕ) : { e : SpernerProperty.QuotientPoset (m * n) (wreathSubgroup m n) ≃o Lmn m n // ∀ (p : SpernerProperty.QuotientPoset (m * n) (wreathSubgroup m n)), grade ℕ (e p) = grade ℕ p }

Grade-preserving order isomorphism from QuotientPoset (m*n) (wreathSubgroup m n) to Lmn m n. Composed from the bridge quotientPosetIsoWreathQuotient and wreathQuotientIsoLmn (Theorem 6.9).

theorem YoungLattice.Lmn.hasSpernerProperty (m n : ℕ) : SpernerProperty.HasSpernerProperty

Corollary 6.10 (Sperner). L(m,n) has the Sperner property.

theorem YoungLattice.Lmn.Lmn_isRankUnimodal (m n : ℕ) : SpernerProperty.IsRankUnimodal

Corollary 6.10 (Unimodal). L(m,n) is rank-unimodal.

theorem YoungLattice.Lmn.isRankSymmetric_and_isRankUnimodal_and_hasSpernerProperty (m n : ℕ) : SpernerProperty.IsRankSymmetric ∧ SpernerProperty.IsRankUnimodal ∧ SpernerProperty.HasSpernerProperty

Corollary 6.10. The posets L(m,n) are rank-symmetric, rank-unimodal, and Sperner.