Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The graded dual numbers have Cartan polynomial 1+v²

Statement

Let k be any field and let A=k[ε]/(ε2) with deg⁡ε=2. Put S=A/(ε) in degree zero and R=Z[v,v−1], with v[M]=[M{1}] and M{r}d=Md−r. Then K0gr(A)=R[A] and G0gr(A)=R[S], and the graded Cartan map sends [A] to (1+v2)[S].

Facts & Assumptions

Given: A field k, the quotient algebra A=k[ε]/(ε2), and the grading with deg⁡ε=2. The simple module S=A/(ε) is concentrated in degree zero.

[F1]

The polynomial ring k[x] consists of finitely supported coefficient sequences with coefficientwise addition and convolution multiplication (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

[F2]

For a field F, every f∈F[x] and nonzero g∈F[x] have unique q,r with f=qg+r and either r=0 or deg⁡r<deg⁡g (Division algorithm for polynomials over a field).

[F3]

The coefficientwise operations make k[x] a commutative ring with its constants embedded as a unital subring (Polynomial convolution makes R[x] a commutative ring containing R as its constant subring).

[F4]

A two-sided ideal is an additive subgroup closed under multiplication on both sides; in a commutative ring the left, right and two-sided ideal conditions agree (Left, right and two-sided ideals).

[F5]

The quotient ring k[x]/I is formed from additive cosets with multiplication (f+I)(g+I)=fg+I (The quotient ring R/I with (r+I)(s+I)=rs+I).

[F6]

This quotient multiplication is well defined if and only if I is a two-sided ideal (Multiplication of additive cosets is well defined if and only if the additive subgroup is a two-sided ideal).

[F7]

When I is a two-sided ideal, the cosets form a ring with identity 1+I (For a two-sided ideal I, the additive cosets form a ring R/I with identity 1+I).

[F8]

A k-algebra is a unital ring with a unital map from k whose image is central (Algebras over a commutative ring, central structure maps, and algebra homomorphisms).

[F9]

A graded k-algebra has a decomposition A=⨁iAi with AiAj⊆Ai+j and 1A∈A0 (Associative graded algebras, bimodules, and internal shifts).

[F10]

The internal shift is (M{r})d=Md−r and is invertible (Associative graded algebras, bimodules, and internal shifts).

[F11]

A finite direct sum of shifts of the regular graded module is projective in GrMod⁡0(A) (Finite graded projectives are finite shifted-free summands).

[F12]

A finite graded projective cover is a degree-zero epimorphism whose kernel is superfluous among graded submodules (Finite-dimensional graded algebras have graded projective covers).

[F13]

G0gr(A) uses short-exact-sequence relations, K0gr(A) uses split relations, and cAgr([P])=[P] (Graded Grothendieck groups, shift action, and Cartan map).

[F14]

A short exact sequence 0→X→Y→Z→0 imposes [Y]=[X]+[Z] in G0 (Grothendieck group of an essentially small abelian category).

[F15]

The Laurent action is vr[M]=[M{r}] and vr[P]=[P{r}] (Graded Grothendieck groups, shift action, and Cartan map).

[F16]

A graded-simple module is a nonzero finite-dimensional graded module with no proper nonzero graded submodule (Shift-orbit bases for graded simple and projective classes).

[F17]

Representatives of graded-simple shift orbits and their finite graded projective covers give Laurent bases for G0gr(A) and K0gr(A) (Shift-orbit bases for graded simple and projective classes).

Proof

technique · direct
1.1F1F2F3F4F5F6F7F8F9givenconstructalgebra

Let x denote the polynomial variable and I=(x2)=x2k[x]. It is an additive subgroup, and multiplication by any polynomial sends x2q to another multiple of x2 on either side; thus it is a two-sided ideal by [F3, F4]. The coefficient of x2 in x2 is 1≠0, so [F2] gives every f∈k[x] a unique division remainder a+bx modulo I. Hence each element of A=k[x]/I has a unique form a+bε, and {1,ε} is a k-basis with ε2=0. By [F5] and [F6] the coset multiplication is well defined, and [F7] makes A a unital ring. The composite k→k[x]→A is unital and multiplicative: the first map is the constant-polynomial homomorphism [F3], and the quotient map preserves sums, products, and identity by the coset operations in [F5] and [F7]. The quotient is commutative because k[x] is commutative, so this map has central image. Thus [F8] makes A a two-dimensional unital k-algebra. Define A0=k1, A2=kε, and Ad=0 for d∉{0,2}. The multiplication rules 1⋅1=1, 1⋅ε=ε⋅1=ε, and ε2=0 verify [F9]. The quotient S=A/(ε) is one-dimensional over k and concentrated in degree zero.

2.1F9F10F16step 1.1givenchoosealgebra

Let T be any nonzero finite-dimensional graded-simple left A-module, with graded-simple as in [F16]. The submodule εT is graded since ε is homogeneous. If εT≠0, simplicity gives εT=T, whence T=εT=ε2T=0, a contradiction; thus εT=0. The action factors through A/(ε)=k, so each homogeneous component Td is a graded submodule. Simplicity forces exactly one component to be nonzero. That component has dimension one over k, since if its dimension exceeded one, the span of any nonzero vector would be a proper nonzero graded submodule. Hence T≅S{r} for its unique nonzero degree r. This also proves S is graded-simple. Distinct r give distinct supports, so there is exactly one graded-simple shift orbit, represented by S.

2.2F11step 1.1given

The regular graded module A=A{0} is a finite direct sum of shifts of itself, so [F11] makes it projective in GrMod⁡0(A). It is finite-dimensional by step 1.1, hence is a finite graded projective.

3.1F9F12F16step 1.1step 2.1step 2.2givenalgebra

The quotient map π:A↠S is degree-zero and has kernel kε. If a graded submodule N≤A satisfies N+kε=A, then taking degree-zero components gives N0=A0=k1, since (kε)0=0. Thus 1∈N, so N=A. By [F12], π is a finite graded projective cover of S. To verify indecomposability directly, suppose A=U⊕V for nonzero graded submodules. Since π is nonzero, one restriction, say π∣U, is nonzero; its image is a nonzero graded submodule of the graded-simple S, hence is all of S. Therefore every element of A differs from an element of U by an element of ker⁡π, so U+ker⁡π=A. Superfluity forces U=A, contradicting V≠0. Thus A is graded-indecomposable.

4.1F13F17step 2.1step 3.1construct

Apply [F17] to the unique simple shift orbit from step 2.1 and its cover A↠S from step 3.1. It gives [S] as an R-basis of G0gr(A) and [A] as an R-basis of K0gr(A).

5.1F10F13F14F15step 1.1step 4.1givenconstructalgebra∎

Identify S with k via the quotient map. Define j:S{2}→A by j(λ)=λε. It is degree-zero because the degree-zero element of S lies in degree two after shifting, and ε has degree two. For a=α+βε∈A and λ∈k, the quotient action on S gives j(aλ)=αλε, while a j(λ)=(α+βε)λε=αλε because ε2=0; hence j is A-linear. It is injective since ε≠0 by the unique normal form, and its image is kε=ker⁡π. Thus 0→S{2}→jA→πS→0 is exact. By [F14], [A]=[S{2}]+[S] in G0gr(A). Now [F10] and [F15] give [S{2}]=v2[S], while [F13] says the graded Cartan map sends [A] to this same class in G0gr(A). Therefore cAgr([A])=(1+v2)[S], as claimed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources