Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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.

koszul euler characteristic annihilator correction

Example

Assume AC. Let R be a discrete valuation ring with uniformizer t and residue field k=R/(t). Take M=R⊕k and the one-element sequence (t). Then H0(K(t;M))≅k⊕k, H1(K(t;M))≅k, and all other homology vanishes. Moreover P(t),M(T)=T+2, so e1((t),M)=χ(K(t;M))=1. Omitting the annihilator correction from first-element reduction would give the incorrect value 2.

Facts & Assumptions

Given: AC, a DVR R with uniformizer t and residue field k=R/(t), M=R⊕k, and the sequence (t).

[A1]

We assume The Axiom of Choice for the two comparison results.

[F1]

The Koszul/multiplicity bridge holds for finite modules with finite-colength sequence ideals: degree-r Hilbert–Samuel coefficient as Koszul Euler characteristic.

[F2]

First-element reduction subtracts the Euler characteristic with annihilator coefficients: koszul euler characteristic first element reduction.

[F3]

In a DVR, ℓR(R/(ta))=a for every integer a≥0: Length and valuation in a DVR.

[F4]

The one-element Koszul differential is multiplication by that element: Koszul Complex Of A Sequence With Coefficients.

[F5]

Euler characteristic and degree-indexed coefficients use ℓR(M/In+1M): koszul euler characteristic and degree indexed multiplicity.

[F6]

Length adds in a short exact sequence: Module length is additive in short exact sequences.

Verification

technique · direct
1.1F4given

The complex is 0→R⊕k→tR⊕k→0, in degrees 1,0, and the map is (a,b)↦(ta,0). Since a DVR is a domain and t≠0, its kernel is 0⊕k and its image is tR⊕0. Thus H1≅k, H0≅(R/tR)⊕k=k⊕k, and all remaining homology is zero.

2.1F3F5F6step 1.1

The DVR length formula at a=1 gives ℓR(k)=1, and the split sequence 0→k→k⊕k→k→0 gives length 2. Therefore M/tM has finite length and χ(K)=2−1=1.

3.1A1F1F3F5F6step 2.1

For every n≥0, tn+1M=tn+1R⊕0. Hence M/tn+1M≅R/(tn+1)⊕k has length (n+1)+1=n+2. Thus P(T)=T+2 and e1=1![T]P=1. The DVR is Noetherian local, M is finite, and the finite-colength hypothesis was verified above, so the bridge theorem under AC gives the same value 1.

4.1A1F2F5step 1.1step 2.1step 3.1∎

Removing t leaves the empty sequence with coefficients C=M/tM=k⊕k and T=0:Mt=0⊕k. For an empty sequence its Euler characteristic is the coefficient module's length. Thus the first-element identity reads χ(K(t;M))=ℓR(C)−ℓR(T)=2−1=1. Both lengths are finite, so all its hypotheses hold. The nonzero annihilator term is exactly the discrepancy with ℓR(C)=2.

Remarks

Locally calculated design example. The general correction formula is supported by Hochster printed p.165; Stacks 43.15.5 supplies the comparison context. The actual instance uses the published DVR length interface and explicit multiplication maps, with no formal power-series construction assumed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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