Matching works

7 works

math.AC — Commutative Algebra

Prime-Generated Localization Descent for Unique Factorization in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

We give a source-grounded exposition of a Lean 4 formalization of prime-generated Nagata factoriality descent. A commutative noetherian integral domain is a unique factorization domain if a localization is a unique factorization domain and every denominator is exactly a finite product of prime elements belonging to the denominator submonoid. The formal statement works with an arbitrary algebra carrying Mathlib’s IsLocalization structure. We explain the two cases for an irreducible element, the multiset cancellation and splitting arguments, and the corollary for submonoids generated by arbitrary sets of primes. A registered polynomial corollary illustrates reuse of the descent package; its Laurent-polynomial premise is proved using Mathlib’s existing polynomial UFD instance, a dependency made explicit here. The exposition is tied to the registered source and dependency pins, distinguishes historical mechanical verification from manuscript review, and situates the development relative to an earlier Lean preprint and an Isabelle/HOL formalization. No new algebraic theorem or priority claim is asserted.

Primarily AI-generated textHuman understanding: some partsLean 4MathlibNagata factorialitycommutative algebralocalizationunique factorization domains

Oct 01, 2026PDF ↗View work →

hexagon:2609.00137v1

math.CO — Combinatorics

On a non-basis of the coinvariant algebra

Contributed by Darij Grinberg

A conjecture arising from a question of Procesi proposes a basis of the coinvariant algebra of $S_n$ consisting of column-antisymmetrized monomials indexed by pairs of standard Young tableaux. We show that the proposed family need not even span an $S_n$ -subrepresentation: for $n=8$ , a generator of degree $15$ is sent outside the span by the adjacent transposition $(4,5)$ . The proof is an exact finite computation with an explicit separating functional, requiring neither a rank computation nor Gr\"obner reduction. We also retain an explicit relation for $n=7$ , where the basis assertion first fails, although the span is still invariant.

A mix of human-written and AI-generated textHuman understanding: all partsSpecht modulesYoung tableauxcoinvariant algebrahigher Specht polynomialsrepresentations of the symmetric group

Sep 29, 2026PDF ↗View work →

hexagon:2609.00133v1

math.RA — Rings and Algebras

A Universal Noncommutative Splitting Algebra for Polynomials

Contributed by Darij Grinberg

Let $R$ be a commutative ring. We show that every homogeneous polynomial $f\in R[x_{1},\ldots,x_{m}]$ of degree $n$ splits into a product of $n$ homogeneous linear forms over a suitable noncommutative ring extension $S$ of $R$ (that is, over a noncommutative $R$ -algebra $S$ whose structure morphism $R\rightarrow S$ is injective). The algebra $S$ is universal for such factorizations and is free as an $R$ -module. The proof uses Bergman's Diamond Lemma: we define $S$ by generators and relations, and the relations form a terminating reduction system that has no ambiguities and thus is confluent. An analogous result is also shown for inhomogeneous polynomials (with inhomogeneous factors). This easily follows from the homogeneous case by homogenizing and then setting the homogenizing variable equal to $1$ .

A mix of human-written and AI-generated textHuman understanding: all partsBergman's diamond lemmaGröbner basescombinatorial algebranoncommutative polynomials

Sep 29, 2026PDF ↗View work →

hexagon:2609.00121v1

math.AC — Commutative Algebra

Polynomials over Symmetric Polynomials

Contributed by Darij Grinberg

Let $\mathbf{k}$ be a commutative ring, and let the symmetric group $\mathfrak{S}_{n}$ act on $P=\mathbf{k}\left[ x_{1} ,x_{2},\ldots,x_{n} \right] $ by permuting the variables. We prove four results that are known (at least in the case when $\mathbf{k}$ is a field) but not easily found in the literature. First, the coinvariant algebra (the quotient of $P$ by the ideal generated by the symmetric polynomials with constant term $0$ ) is a free $\mathbf{k}$ -module of rank $n!$ , with the residue classes of the Artin monomials as a basis. Second, $P$ is a free module of rank $n!$ over the ring $P^{\mathfrak{S}_{n}}$ of symmetric polynomials, again with the Artin monomials as a basis. Third, if $n!$ is invertible in $\mathbf{k}$ , the coinvariant algebra is the regular $\mathbf{k}\left[ \mathfrak{S}_{n} \right] $-module. Fourth, under the same hypothesis, $P$ is a free left $P^{\mathfrak{S}_{n}}\left[ \mathfrak{S}_{n} \right]$ -module of rank $1$ . The first result follows from an elementary normal-form lemma for monic polynomials with pairwise relatively prime leading monomials. The second is proved by lifting the Artin basis. For the third, we use orbit harmonics with a strongly discrete point orbit, and the fourth follows by equivariantly lifting a regular basis of the coinvariant algebra.

A mix of human-written and AI-generated textHuman understanding: all partsArtin basisGröbner basescoinvariant algebraorbit harmonicssymmetric polynomials

Sep 28, 2026PDF ↗View work →

hexagon:2609.00117v1

math.AC — Commutative Algebra

Splitting a Polynomial into Linear Factors after an Injective Ring Extension

Contributed by Darij Grinberg

We show that each univariate polynomial $P = p_0 + p_1 X + \cdots + p_m X^m \in R[X]$ over a commutative ring $R$ can be factored into linear factors over a suitable commutative ring extension $S$ of $R$ . The proof proceeds by universal construction: $S$ is defined as the tensor product $R \otimes_{C_m} B_m$ , where $B_m$ is the polynomial ring $\ZZ[a_1, b_1, a_2, b_2, \ldots, a_m, b_m]$, and where $C_m$ is its subring generated by its ``homogenized elementary symmetric polynomials'' $E_r=\sum_{\substack{I\subseteq [m];\\ |I|=r}} \prod_{i\in I}a_i\prod_{i\notin I}b_i$ for all $0 \leq r \leq m$ . The injectivity of the structure homomorphism $R \to S$ is deduced from a combinatorial study of the diagonal subring of $B_m$ . In the process, a homogeneous variant of the Garsia--Stanton basis is constructed, and some classical properties of symmetric polynomials are recovered.

A mix of human-written and AI-generated textHuman understanding: all parts

Sep 28, 2026PDF ↗View work →

hexagon:2609.00105v1

math.AC — Commutative Algebra

Graded absolute integral closures and Picard groups

Contributed by Akhil Mathew

We deduce from Bhatt's graded Cohen--Macaulay and vanishing results that an integer-graded absolute integral closure of a weighted polynomial ring over $\Z_p$ , modulo $p$ , is free with basis degrees smaller than the sum of the weights. A direct $p$ -adic expansion turns this degree bound into a uniform solution of the cusp relation modulo nilpotents. Consequently every ring $R$ admits a faithfully flat algebra with seminormal reduction, and every invertible $R[T]$ -module becomes free after a faithfully flat extension of $R$ , answering a question of Drinfeld.

Primarily AI-generated textHuman understanding: all partsPicard groupsabsolute integral closureseminormality

Sep 26, 2026PDF ↗View work →

hexagon:2609.00001v1

math.AG — Algebraic Geometry

Strict negativity and non-vanishing of Chen--Larson hypergeometric coefficients

Contributed by Johannes Schmitt

Chen and Larson study tautological classes on the strata of holomorphic abelian differentials, where they predict a vanishing result. Using known tautological relations on the moduli space of curves, they reduce this prediction to the non-vanishing of certain coefficients of a quotient of hypergeometric generating series, treating the residue classes $g\equiv0,2\pmod3$ and $g\equiv1\pmod3$ through two separate series; they verify the non-vanishing by computer for small genus. We prove it in general: in both cases the relevant coefficient is non-vanishing for every genus and every stratum, and in the first case it has, more strongly, a uniform strict sign. Along the way we correct an error in the Chen--Larson derivation of the $g\equiv1\pmod3$ series, where a constant of the underlying relation of Ionel had inadvertently been changed. The paper falls into two parts. Part~I gives the mathematical proofs; Part~II documents the Lean~4 and Mathlib formalization --- whose only non-standard trust assumption is the compiler invoked by \code{native\_decide} for the large finite computations --- together with the long-horizon, multi-model generative-AI process that produced the proofs, exposed false intermediate routes, and uncovered the error in the printed Proposition~5.2 relation noted above.

Primarily AI-generated textHuman understanding: not declaredpower seriestautological classes

Sep 01, 2026PDF ↗View work →

math.AC — Commutative Algebra
math.AG — Algebraic Geometry
math.AP — Analysis of PDEs
math.AT — Algebraic Topology
math.CA — Classical Analysis and ODEs
math.CO — Combinatorics
math.CT — Category Theory
math.CV — Complex Variables
math.DG — Differential Geometry
math.DS — Dynamical Systems
math.FA — Functional Analysis
math.GM — General Mathematics
math.GN — General Topology
math.GR — Group Theory
math.GT — Geometric Topology
math.HO — History and Overview
math.IT — Information Theory
math.KT — K-Theory and Homology
math.LO — Logic
math.MG — Metric Geometry
math.NA — Numerical Analysis
math.NT — Number Theory
math.OA — Operator Algebras
math.OC — Optimization and Control
math.PR — Probability
math.QA — Quantum Algebra
math.RA — Rings and Algebras
math.RT — Representation Theory
math.SG — Symplectic Geometry
math.SP — Spectral Theory
math.ST — Statistics Theory
cs.CC — Computational Complexity
cs.CG — Computational Geometry
cs.DM — Discrete Mathematics
cs.DS — Data Structures and Algorithms
cs.FL — Formal Languages and Automata Theory
cs.IT — Information Theory
cs.LO — Logic in Computer Science
cs.MS — Mathematical Software
cs.NA — Numerical Analysis
cs.SC — Symbolic Computation
math-ph — Mathematical Physics
quant-ph — Quantum Physics
stat.TH — Statistics Theory