Pipeline-generated

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.

✓ 12 results · all verified · 11 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Koszul Complexes and Regular Sequences — Examples

1 · Prerequisites

2 · Summary

A finite, ordered treatment of exterior constructions, Koszul homology, regular sequences, and their local finite consequences. All regularity claims retain their stated terminal-quotient and local hypotheses.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-09-06Open item page →

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∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Koszul Complex Polynomial Variables

Example

For $S = k [x_{1}, \dots, x_{n}]$ , the variables form a regular sequence and $K (x_{1}, \dots, x_{n}; S)$ is a finite free resolution of $k = S / (x_{1}, \dots, x_{n})$ .

Facts & Assumptions

Given: The polynomial ring and its variable sequence stated in the claim. The declared prerequisite used here is Koszul Complex Resolves A Regular Quotient.

Proof

technique · direct

1.1

Successive quotients by the variables are polynomial rings, so each next variable is injective.

givenalgebra

2.1

The regular-quotient resolution theorem gives a finite free resolution of $k$ .

step 1.1algebra∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06‡ rests on unproved material (inherited)Open item page →

Koszul Resolution Complete Intersection

Example

In $k [x, y]$ , the regular sequence $x^{2}, y^{3}$ gives $0 \to R \to R^{2} \to R \to R / (x^{2}, y^{3}) \to 0$ with ranks $1, 2, 1$ .

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Resolves A Regular Quotient, Complete Intersection Betti Numbers Binomial.

Proof

technique · direct

1.1

$x^{2}$ is regular in $k [x, y]$ , and $y^{3}$ is regular modulo $(x^{2})$ .

givenalgebra

2.1

The Koszul complex resolves the quotient with exterior ranks $1, 2, 1$ , whose alternating sum is zero.

step 1.1algebra∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Homology Zero Divisor

Example

For $R = k [t] / (t^{2})$ , $K (t; R)$ has $H_{0} ≅ k$ and $H_{1} = (t) ≅ k$ .

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are One Element Koszul Homology.

Proof

technique · direct

1.1

In $k [t] / (t^{2})$ , multiplication by $t$ has kernel and image $(t)$ .

givenalgebra

2.1

The one-element formula gives $H_{0} ≅ k$ and $H_{1} ≅ (t) ≅ k$ .

step 1.1algebra∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06‡ rests on unproved material (inherited)Open item page →

Nonpermutable Regular Sequence

Example

In $R = k [x, y, z] / ((x - 1) z)$ , $x, (x - 1) y$ is regular, whereas the reverse order is not: $(x - 1) y z = 0$ with $z \neq 0$ .

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Regular Sequence On A Module, Regularity Notions And Permutation Invariance Local.

Proof

technique · direct

1.1

Modulo $x$ , the relation becomes $z = 0$ , leaving $k [y]$ where $(x - 1) y$ becomes $- y$ ; also $x$ is a non-zero-divisor.

givenalgebra

2.1

In reverse order $z \neq 0$ is killed by $x - 1$ , so the first regularity condition fails; the ring is not local.

step 1.1algebra∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Homology After Localisation

Example

For $R = k [t]$ , $M = R / (t)$ , and sequence $(t)$ , localization at $S = {1, t, t^{2}, \dots}$ makes both the Koszul complex and its homology zero.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Homology Localises.

Proof

technique · direct

1.1

After inverting $t$ , the module $R / (t)$ is zero, so every term of the complex localizes to zero.

givenalgebra

2.1

Exact localization gives zero homology, agreeing with the localized Koszul complex.

step 1.1algebra∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Empty And Unit Koszul Boundaries

Example

For nonzero $M$ , compare $K (\emptyset; M)$ , $K (0; M)$ , and $K (1; M)$ ; the first is $M$ , the second has $H_{0} = H_{1} = M$ , and the third is acyclic.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Empty Koszul Complex Is The Coefficient Module, One Element Koszul Homology, Regular Sequence On A Module.

Proof

technique · direct

1.1

The empty complex is $M$ ; for $0$ the two-term differential is zero, and for $1$ it is an isomorphism.

givenalgebra

2.1

Thus $H_{0} = H_{1} = M$ in the zero case and the unit case is acyclic; the unit fails the proper-quotient regularity convention.

step 1.1algebra∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul D Square Sign Check Three Elements

Example

For $e_{1} \land e_{2} \land e_{3}$ , expand $d^{2}$ and pair the two appearances of each $x_{i} x_{j} e_{k}$ with opposite signs.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Differential Coordinate Formula, Koszul Differential Square Pairwise Cancellation.

Proof

technique · direct

1.1

After one differential the three terms are $x_{1} e_{2} \land e_{3} - x_{2} e_{1} \land e_{3} + x_{3} e_{1} \land e_{2}$ .

givenalgebra

2.1

The second differential produces each $x_{i} x_{j} e_{k}$ twice with opposite signs, so the total is zero.

step 1.1algebra∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Homology Of A Zero Divisor

Example

For $R = k [s, t] / (s t)$ and $x = s$ , $H_{0} = R / (s)$ , $H_{1} = (t)$ , and both are supported on $V (s)$ .

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are One Element Koszul Homology, Koszul Homology Supported On Sequence Vanishing Set.

Proof

technique · direct

1.1

The annihilator of $s$ in $k [s, t] / (s t)$ is $(t)$ .

givenalgebra

2.1

Thus $H_{0} = R / (s)$ and $H_{1} = (t)$ ; both are killed by $s$ and supported on $V (s)$ .

step 1.1algebra∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Generator Change Koszul Isomorphism

Example

For $(x, y)$ and $(x + y, y)$ , the matrix $(\begin{array}{cc} 1 & 1 \\ 0 & 1 \end{array})$ induces the chain isomorphism sending the new first basis vector to $e_{1} + e_{2}$ and the second to $e_{2}$ .

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Generator Matrix Chain Map, Koszul Complex Invariant Under Invertible Generator Change.

Proof

technique · direct

1.1

The displayed upper-triangular matrix is invertible and expresses $(x + y, y)$ in terms of $(x, y)$ .

givenalgebra

2.1

Its exterior action intertwines differentials, and the inverse matrix supplies the inverse chain map.

step 1.1algebra∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06‡ rests on unproved material (inherited)Open item page →

Regular Sequence Powers And Permutation

Example

In $k [x, y]_{(x, y)}$ , $(x, y)$ , $(x^{2}, y^{3})$ , and $(y^{3}, x^{2})$ are regular sequences.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Positive Powers Of A Regular Sequence Remain Regular, Regular Sequences Permutable Local.

Proof

technique · direct

1.1

$x, y$ are regular in the local polynomial ring because the successive quotients are domains.

givenalgebra

2.1

Positive powers and adjacent swaps preserve regularity under these Noetherian local hypotheses.

step 1.1algebra∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06‡ rests on unproved material (inherited)Open item page →

Koszul Resolution Betti Table Complete Intersection

Example

For $R = k [x, y, z]_{(x, y, z)}$ and $(x^{2}, y^{2}, z^{2})$ , the minimal Koszul resolution of the quotient has Betti table $1, 3, 3, 1$ .

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Complete Intersection Betti Numbers Binomial, Koszul Resolution Minimality Maximal Ideal Sequence.

Proof

technique · direct

1.1

The squared variables are a regular sequence in the local polynomial ring and lie in its maximal ideal.

givenalgebra

2.1

The minimal Koszul ranks are $(\binom{3}{0}), (\binom{3}{1}), (\binom{3}{2}), (\binom{3}{3}) = 1, 3, 3, 1$ .

step 1.1algebra∎

Sources

The Stacks Project, Koszul complexes and regular sequences