Papers With

← All papers
First page of The Minimum Number of Generators of Symmetric Ideals

The Minimum Number of Generators of Symmetric Ideals

Noah Walker

math.AC May 27, 2025 · v3
formalization mathlib algebra combinatorics
Read PDF arXiv abstract Code
TL;DR
The author formalized the complete proof of Proposition 4.4, a Kostka-number inequality, in Lean using Mathlib.
Abstract
We study equigenerated symmetric ideals in polynomial rings and the minimum number of polynomials required to generate them up to permutations of the variables. We give a representation-theoretic formula for this number and determine a sharp threshold on the number of variables needed for a general symmetric ideal to attain the largest possible dimension in its generating degree. The threshold is governed by partial sums of integer partition numbers, which appear in the OEIS as sequence A000070. We also construct explicit extremal symmetric ideals for every admissible number of generators. As an application, the principal case gives the sharp stable range for the theorem of Harada-Seceleanu-Şega on general principal symmetric ideals.
Problem

The paper studies the minimum number of polynomials needed to generate an equigenerated symmetric ideal up to permutations of the variables. It also asks how many variables are needed for a general symmetric ideal to attain the largest possible dimension in its generating degree.

Approach

The question is recast as finding the minimum number of kS_n-module generators of the generating-degree component, which gives a formula in terms of the canonical decomposition. Maximal r-generated submodules of R_d are described using Kostka numbers and Specht module dimensions. Inequalities between Kostka numbers and standard Young tableaux counts are proved by induction and case analysis. Proposition 4.4 from this analysis is formalized in Lean with Mathlib.

Results

A formula r = ceil(max n_i/dim V_i) is obtained, together with a sharp threshold on n governed by partial sums of partition numbers (OEIS A000070). Explicit extremal symmetric ideals are constructed, and the results give the sharp stable range for the Harada-Seceleanu-Şega theorem on general principal symmetric ideals.