ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-06

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 Complex One And Two Elements

Example

Let $k$ be a field and $R = k [u, v]$ . With coefficients $M = R$ , the one-element complex is $K (u; R) = [0 \to R \overset{u}{\to} R \to 0]$ , with the displayed copies in degrees $1, 0$ . It has $H_{0} ≅ k [v]$ and zero homology in every other degree.

The two-element complex is $K (u, v; R) = [0 \to R \overset{d_{2}}{\to} R^{2} \overset{d_{1}}{\to} R \to 0]$ , in degrees $2, 1, 0$ , where degree-two $1$ corresponds to $e_{1} \land e_{2}$ , and

$d_{2} (c) = - v c e_{1} + u c e_{2}, d_{1} (a e_{1} + b e_{2}) = a u + b v .$

Its degree-zero homology is $k$ , and all other homology vanishes.

Facts & Assumptions

Given: A field $k$ , the polynomial ring $R = k [u, v]$ , coefficients $R$ , and the ordered standard exterior bases. The prerequisites are Basic Koszul Homology, One Element Koszul Complex, and Koszul Differential Coordinate Formula.

Proof

technique · direct

1.1

The one-element lemma gives the displayed complex. Multiplication by $u$ on $k [u, v]$ is injective by comparison of polynomial coefficients, so $H_{1} = 0$ and $H_{0} = R / u R ≅ k [v]$ ; all other terms vanish.

givenalgebra

1.2

For two elements the coordinate formula gives $d_{2} (c) = (- v c, u c)$ and $d_{1} (a, b) = u a + v b$ , with $d_{1} d_{2} (c) = - u v c + v u c = 0$ .

givenalgebra

2.1

If $u a + v b = 0$ , reduction modulo $u$ gives $v \overline{b} = 0$ in $k [v]$ . Multiplication by $v$ is injective, so $b = u c$ for some $c \in R$ . Substitution gives $u (a + v c) = 0$ , hence $a = - v c$ . Thus every degree-one cycle is $d_{2} (c)$ , proving $H_{1} = 0$ .

step 1.1step 1.2algebra

3.1

If $d_{2} (c) = 0$ , then $u c = 0$ , so $c = 0$ and $H_{2} = 0$ . Finally $H_{0} = R / (u, v) ≅ k$ , and there are no terms outside degrees $0, 1, 2$ . This proves both computations.

step 1.1step 1.2step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

The Stacks Project, Koszul complexes and regular sequences (standard reference, not scraped)