we-solve (beta)

Math-2521 · mathematics · Algebra

Finiteness of the little finitistic dimension

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every Artin algebra $A$, is \[ \sup\{\operatorname{pd}_A(M): M\text{ is finitely generated and }\operatorname{pd}_A(M)<\infty\} \] finite?

Short English statement

For every Artin algebra $A$, are the finite projective dimensions $\operatorname{pd}_A(M)$ of its finitely generated modules $M$ bounded above?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2521-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2521

One finite complex algebra supports modules with finite projective dimension at least $2m-2$ for arbitrarily large integers $m$. Consequently its little finitistic dimension is infinite, giving the requested counterexample within Artin algebras. This is presented as a claimed negative answer.

Finiteness of the little finitistic dimension

OpenAI's claim

OpenAI presents a counterexample in the selected manuscript. A single finite-dimensional complex algebra is claimed to have finite modules whose finite projective dimensions are unbounded.

Mathematical statement of the claimed result

Result 1.
A finite-dimensional unital complex algebra $A$ is claimed to admit, for every $m\ge1$, a left module $N_m$, finite-dimensional over $\mathbb C$, satisfying \[ 2m-2\le\operatorname{pd}_AN_m<\infty. \] Thus its little finitistic dimension, the supremum of finite projective dimensions of finite-dimensional modules, is infinite. A second complex algebra $\Lambda$ satisfies \[ \operatorname{findim}\Lambda=\operatorname{Findim}\Lambda=\infty, \qquad \operatorname{findim}(\Lambda^{\mathrm{op}}) =\operatorname{Findim}(\Lambda^{\mathrm{op}})=0, \] where each displayed dimension is for left modules and the capitalized version allows all modules. The corollary also distinguishes generation of the unbounded derived categories by injectives on the two sides.

Outline of the argument

One fixed finitely presented algebra encodes arbitrarily long terminating processes through a twisted derived tensor functor. The subsequent finite-dimensional realization converts these tensor histories into ordinary projective resolutions, retaining unbounded termination lengths without changing the final algebra.

Formal verification

For family 198, the Lean scope includes unbounded finite projective dimensions over one complex algebra and a separate extreme left/right finitistic and injective-generation asymmetry. The listed Comparator files are FinitisticAsymmetry.lean, LittleFinitistic.lean. Named declarations include OAI.LittleFinitistic.Main.exists_counterexample, OAI.LittleFinitistic.extreme_left_right_asymmetry. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

Go to contribution →