Alphabeta Math
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.

45 results · all verified · 40 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 5 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Koszul Complexes and Regular Sequences

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

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Exterior Algebra Of A Finite Free Module

Definition

Let R be a commutative unital ring and let F be a finite free R-module with ordered basis e1,,en. Define F=TR(F)/(vv:vF), graded by tensor degree; write eI=ei1eip for I={i1<<ip}.

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

Exterior Algebra Basis Monomials

Statement

For every p, the wedges eI with I=p form an R-basis of pF; in particular it is zero for p>n.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Exterior Algebra Of A Finite Free Module.

Proof

technique · direct
1.1

Sort wedges using anticommutation and delete repetitions using eiei=0, so the increasing wedges span.

givenalgebra
2.1

The alternating determinant map to the free module on p-subsets kills the exterior relations and sends these wedges to distinct basis elements, proving independence.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Exterior Multiplication Koszul Sign Rule

Statement

If i is distinct from i1<<ip, then eieI=(1)#{ij<i}esort({i}I), while eieI=0 when iI.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Exterior Algebra Of A Finite Free Module, Exterior Algebra Basis Monomials.

Proof

technique · direct
1.1

Move ei across precisely the factors indexed below i; each adjacent swap contributes 1.

givenalgebra
2.1

If i already occurs, the wedge contains a square and is zero; this remains true in characteristic 2.

step 1.1algebra
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-06Open item page →

Koszul Complex Of A Sequence With Coefficients

Definition

Let R be a commutative unital ring, let x=(x1,,xn) be a finite ordered sequence in R, and let M be an R-module. On Rn, with standard basis e1,,en, let δ be the R-linear graded derivation of degree 1 with δ(ei)=xi and δ(R)=0; thus δ(ab)=δ(a)b+(1)paδ(b) for homogeneous a of degree p.

The Koszul complex with coefficients in M is K(x;M)=(RnRM,d), where d=δidM. Its degree-p term is pRnRM for 0pn, and zero otherwise. Explicitly,

d(ei1eipm)=j=1p(1)j1ei1eij^eipxijm.

The empty wedge is 1R. In particular d(eim)=1xim in K0=RRM, canonically identified with M by rmrm with inverse m1m. The differential out of degree zero is zero. The derivation respects the exterior relations and the two orders of deleting distinct factors cancel in d2, so these maps form a chain complex. For n=0 this is M in degree zero under the same identification.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-06Open item page →

Koszul Differential Coordinate Formula

Statement

For I=(i1<<ip), d(eIm)=j=1p(1)j1eIijxijm.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Of A Sequence With Coefficients, Exterior Algebra Basis Monomials.

Proof

technique · direct
1.1

Apply the graded Leibniz rule to the ordered wedge and use d(eij)=xij.

givenalgebra
2.1

Passing the differential through j1 degree-one factors gives (1)j1, yielding the formula.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Differential Square Pairwise Cancellation

Statement

The two terms of d2(eIm) obtained by deleting ia and ib in opposite orders have equal coefficient and opposite sign; hence d2=0.

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, Exterior Multiplication Koszul Sign Rule.

Proof

technique · direct
1.1

Fix two deleted positions a<b. Deleting a then b has sign (1)a1(1)b2, while the reverse order has sign (1)b1(1)a1; these differ by 1 and have the same scalar xiaxib.

givenalgebra
2.1

Every summand of d2 has a unique unordered pair of deleted indices, so the pairs cancel, including in characteristic 2 where 1=1 and the two equal terms add to 0.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-06Open item page →

Koszul Differential Is Well Defined And Squares To Zero

Statement

The derivation defining d annihilates the exterior relations, so it descends to RnM, and its square is zero. Thus K(x;M) is a chain complex.

Facts & Assumptions

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

Proof

technique · direct
1.1

The graded derivation sends eiei to xieieixi=0 and therefore respects the alternating quotient. Its coordinate action is the stated deletion formula.

givenalgebra
2.1

The pairwise cancellation calculation proves d2=0, so the graded modules and this differential satisfy the chain-complex axioms.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Empty Koszul Complex Is The Coefficient Module

Statement

For the empty sequence, K(;M) is M in degree 0 and 0 in every other degree.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Of A Sequence With Coefficients.

Proof

technique · direct
1.1

For the zero free module, only 00=R is nonzero.

givenalgebra
2.1

Tensoring with M gives M in degree zero and zero elsewhere, with zero differential.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

One Element Koszul Complex

Statement

Let R be a commutative unital ring, let M be an R-module, and let xR. Then K(x;M) is 0MxM0, with the left copy in degree 1.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Of A Sequence With Coefficients.

Proof

technique · direct
1.1

For one basis element, the only exterior powers are Re and R.

givenalgebra
2.1

The defining differential sends em to xm, producing the displayed two-term complex.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

One Element Koszul Homology

Statement

For K(x;M), H0=M/xM, H1=(0:Mx), and Hi=0 for i{0,1}.

Facts & Assumptions

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

Proof

technique · direct
1.1

The sole differential is multiplication by x, whose cokernel is M/xM.

givenalgebra
2.1

Its kernel is (0:Mx) and no other chain groups occur.

step 1.1algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Basic Koszul Homology

Statement

For a finite sequence x, H0(K(x;M))=M/(x)M, Hi=0 for i>n, and Hn={mM:xim=0 for all i}.

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 Differential Coordinate Formula.

Proof

technique · direct
1.1

The image in degree zero is (x1M++xnM), so H0=M/(x)M.

givenalgebra
2.1

There are no degrees above n, and the top differential kills m exactly when every xi kills m.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Complex Concatenation Tensor Isomorphism

Statement

For finite sequences x,y, the graded tensor-product identification gives a signed chain isomorphism K(x,y;M)K(x;R)RK(y;M).

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Of A Sequence With Coefficients, Exterior Multiplication Koszul Sign Rule.

Proof

technique · direct
1.1

The exterior algebra of the direct sum of the two based free modules is the graded tensor product of their exterior algebras.

givenalgebra
2.1

Its total differential d1+(1)deg1d agrees termwise with the Koszul deletion differential.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Append One Element Mapping Cone Identification

Statement

If yR, then K(x,y;M) is chain-isomorphic to the mapping cone of multiplication by y on K(x;M).

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Concatenation Tensor Isomorphism, The mapping cone of a chain map.

Proof

technique · direct
1.1

Split p(RnRe) as pRnep1Rn. Send the second summand to the shifted cone summand.

givenalgebra
2.1

The coordinate formula gives d(ez)=yzedz, exactly the cone differential; hence the splitting is a chain isomorphism.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: 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 Mapping Cone Homology Exact Sequence

Statement

Appending y yields the exact sequence Hi(K(x;M))yHi(K(x;M))Hi(K(x,y;M))Hi1(K(x;M)).

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Append One Element Mapping Cone Identification, The cone long exact sequence.

Proof

technique · direct
1.1

The cone identification gives the degreewise split short exact sequence 0K(x;M)K(x,y;M)K(x;M)[1]0.

givenalgebra
2.1

Its connecting map is multiplication by y (check it on a cycle in the shifted summand), so the long exact homology sequence is the displayed one.

step 1.1algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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 Concatenation And Mapping Cone

Statement

The concatenation isomorphism and the append-one mapping-cone identification are natural in M and give the displayed cone long exact sequence.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Concatenation Tensor Isomorphism, Koszul Append One Element Mapping Cone Identification, Koszul Mapping Cone Homology Exact Sequence.

Proof

technique · direct
1.1

The direct-sum exterior identification supplies the signed concatenation chain isomorphism.

givenalgebra
2.1

Splitting off the final basis vector gives its multiplication cone, whose long exact sequence gives the stated package.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Generator Contraction Homotopy

Statement

For each i, exterior multiplication by ei is a degree-1 homotopy satisfying d(ei)+(ei)d=xiid on K(x;M).

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Of A Sequence With Coefficients, Exterior Multiplication Koszul Sign Rule, A chain homotopy.

Proof

technique · direct
1.1

Let hi(z)=eiz. The graded Leibniz rule gives dhi(z)+hid(z)=d(ei)z=xiz.

givenalgebra
2.1

Thus hi is a chain homotopy from multiplication by xi to zero, with no division or characteristic assumption.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Sequence Ideal Annihilates Koszul Homology

Statement

Every xi, hence the ideal (x), annihilates every Hq(K(x;M)).

Facts & Assumptions

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

Proof

technique · direct
1.1

For each generator, the contraction identity is dhi+hid=xiid.

givenalgebra
2.1

Thus each xi acts trivially on homology, hence so does every element of (x).

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Generators Act Null Homotopically

Statement

Multiplication by each generator xi on K(x;M) is chain-homotopic to zero, and consequently acts as zero on homology.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Generator Contraction Homotopy, Sequence Ideal Annihilates Koszul Homology.

Proof

technique · direct
1.1

Exterior multiplication by ei satisfies d(ei)+(ei)d=xiid.

givenalgebra
2.1

This is a chain homotopy from multiplication by xi to zero, so its homology action vanishes.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Homology Supported On Sequence Vanishing Set

Statement

For every q, SuppHq(K(x;M))V((x)).

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Sequence Ideal Annihilates Koszul Homology, Support of a module, A prime lies in the support exactly when some element has annihilator inside it.

Proof

technique · direct
1.1

The sequence ideal annihilates each homology module.

givenalgebra
2.1

A prime in its support contains an annihilator of a nonzero element and therefore contains (x).

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Complex Localises Termwise

Statement

For a multiplicative subset S, localization gives a natural chain isomorphism S1K(x;M)K(x/1;S1M).

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Of A Sequence With Coefficients, Localisation of a module at a multiplicative subset.

Proof

technique · direct
1.1

Localization commutes with finite direct sums and with the finite free exterior bases, sending eIm/s to eI(m/s).

givenalgebra
2.1

The coordinate formula is preserved term by term because (xim)/s=(xi/1)(m/s), so this degreewise isomorphism is a chain isomorphism.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Homology Localises

Statement

Let R be a commutative unital ring, let M be an R-module, let x be a finite sequence in R, and let SR be a multiplicative subset. For every q, S1Hq(K(x;M))Hq(K(x/1;S1M)).

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Localises Termwise, Localisation of modules is exact.

Proof

technique · direct
1.1

Exact localization commutes with the kernel/image quotient defining homology.

givenalgebra
2.1

The termwise localization chain isomorphism identifies the result with the claimed localized Koszul homology.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Complex Flat Base Change

Statement

For a flat map RA, there is a natural chain isomorphism KR(x;M)RAKA(xA;MRA).

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Of A Sequence With Coefficients, Flat and faithfully flat modules and ring homomorphisms.

Proof

technique · direct
1.1

In degree p, base change sends (eIm)a to eI(ma); the exterior basis makes this an isomorphism.

givenalgebra
2.1

The two differentials agree on every basis wedge by xi(m)a=(xia)(m1), which proves the chain claim.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-06Open item page →

Koszul Homology Flat Base Change

Statement

For flat RA, Hq(KR(x;M))RAHq(KA(xA;MRA)) for every q.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Flat Base Change, Flat and faithfully flat modules and ring homomorphisms.

Proof

technique · direct
1.1

Flat tensoring is exact and therefore commutes with homology quotients.

givenalgebra
2.1

The base-changed complex is the Koszul complex on xA with coefficient MRA.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Generator Matrix Chain Map

Statement

If yi=jaijxj, the transpose matrix defines an exterior map inducing a chain map K(y;M)K(x;M).

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Complex Of A Sequence With Coefficients, Koszul Differential Coordinate Formula, Chain map.

Proof

technique · direct
1.1

Let EyEx send the ith basis vector to jaijej. The assumed identity yi=jaijxj makes the degree-one squares commute.

givenalgebra
2.1

Extending by exterior powers respects wedge products, and the derivation rule then makes the resulting map commute with the differentials in every degree.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Complex Invariant Under Invertible Generator Change

Statement

If yi=jaijxj and the matrix (aij) is invertible, the induced generator-matrix chain map is an isomorphism K(y;M)K(x;M).

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.

Proof

technique · direct
1.1

The matrix chain map is defined by exterior powers of the generator map.

givenalgebra
2.1

The inverse matrix induces its inverse in every exterior degree, so the complexes are isomorphic.

step 1.1algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Functoriality Base Change And Generator Change For Koszul Complexes

Statement

Koszul complexes commute with localization and flat base change, and an invertible change of finite generators gives a signed chain isomorphism; the corresponding homology conclusions hold.

Facts & Assumptions

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

Proof

technique · direct
1.1

Termwise localization and flat-base-change maps are chain isomorphisms and exactness supplies their homology conclusions.

givenalgebra
2.1

An invertible generator matrix has an inverse exterior chain map; all maps commute with coefficient-module maps by construction.

step 1.1algebra
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Regular Sequence On A Module

Definition

Let R be a commutative unital ring, let M be an R-module, and let x=(x1,,xn) be a finite ordered sequence in R. The sequence is M-regular when M/(x1,,xi1)M0 and multiplication by xi is injective on it for every i, and M/(x)M0.

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

Regular Sequence First Element Boundary

Statement

A nonempty M-regular sequence has M0, has first element a non-zero-divisor on M, and has nonzero terminal quotient; thus neither a unit nor a zero module satisfies the adopted nonempty convention.

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.

Proof

technique · direct
1.1

At the first stage the definition requires injectivity of x1 on M.

givenalgebra
2.1

It also requires all stage quotients, especially M and the terminal quotient, to be nonzero; units and M=0 therefore fail.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Regular Sequence Tail On Quotient

Statement

A nonempty sequence (x1,,xn) is M-regular if and only if x1 is injective on M and (x2,,xn) is regular on M/x1M.

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.

Proof

technique · direct
1.1

Separate the first condition: x1 must be injective on M.

givenalgebra
2.1

Every remaining condition is precisely the regularity condition for the tail on M/x1M, including the nonzero terminal quotient.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Initial Subsequences Of A Regular Sequence Are Regular

Statement

Every initial subsequence of an M-regular sequence is regular on M.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Regular Sequence Tail On Quotient.

Proof

technique · direct
1.1

Each injectivity requirement for an initial segment occurs among those of the full sequence.

givenalgebra
2.1

Its terminal quotient is an already-required nonzero intermediate quotient.

step 1.1algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Localisation And Faithfully Flat Base Change Of Regular Sequences

Statement

An M-regular sequence remains regular after localization whenever the localized terminal quotient is nonzero, and remains regular after faithfully flat base change.

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, Localisation of modules is exact, Flat and faithfully flat modules and ring homomorphisms.

Proof

technique · direct
1.1

Localization preserves injectivity, so each regularity condition survives; the stated nonzero localized terminal quotient prevents the convention from failing at the end.

givenalgebra
2.1

Faithfully flat tensoring preserves and reflects injectivity and nonzero modules. Apply this successively to the quotient stages to obtain the base-change assertion.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Regular One Element Koszul Acyclicity

Statement

If multiplication by x is injective on nonzero M and M/xM0, then K(x;M) has zero positive homology and resolves M/xM.

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, Regular Sequence On A Module.

Proof

technique · direct
1.1

The one-element computation identifies positive homology with the kernel of multiplication by x.

givenalgebra
2.1

Injectivity makes that kernel zero and degree zero is the stated quotient.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: 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.

Regular Sequence Koszul Acyclicity Induction

Statement

If Hi(K(x;M))=0 for every i>0 and multiplication by y is injective on M/(x)M, then all positive homology of K(x,y;M) vanishes.

Facts & Assumptions

Given: The ring, finite sequence, module, and element stated in the claim. The declared prerequisites used here are Basic Koszul Homology and Koszul Mapping Cone Homology Exact Sequence.

Proof

technique · direct
1.1

Put C=K(x;M). By hypothesis Hi(C)=0 for i>0, while H0(C)=M/(x)M by the basic Koszul-homology calculation.

givenalgebra
2.1

The mapping-cone exact sequence for K(x,y;M) identifies its H1 with the kernel of multiplication by y on H0(C), because H1(C)=0; this kernel is zero by hypothesis. For i>1, the adjacent groups Hi(C) and Hi1(C) both vanish, so exactness gives Hi(K(x,y;M))=0.

step 1.1algebra
TheoremStatement: Literature-sourcedProof: 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.

Regular Sequences Give Acyclic Koszul Complexes

Statement

Every finite M-regular sequence is M-Koszul-regular: Hi(K(x;M))=0 for i>0.

Facts & Assumptions

Given: The ring, finite sequence, and module stated in the claim. The declared prerequisites used here are Regular Sequence Koszul Acyclicity Induction, Regular One Element Koszul Acyclicity, Empty Koszul Complex Is The Coefficient Module, and Regular Sequence On A Module.

Proof

technique · direct
1.1

For the empty sequence the Koszul complex is M in degree zero, so the conclusion is immediate. For length one it is the one-element calculation.

givenalgebra
2.1

Suppose the result holds for an initial segment x. Regularity says that the next element y acts injectively on M/(x)M. The induction lemma applied to the already acyclic K(x;M) therefore makes K(x,y;M) acyclic in positive degrees. Induction on the length proves the claim.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: 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 Resolves A Regular Quotient

Statement

If M is finite free and x is M-regular, then K(x;M) is a finite free resolution of M/(x)M.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Regular Sequences Give Acyclic Koszul Complexes, Basic Koszul Homology, RmRRnRmn with the product basis, and dimF(VFW)=dimFVdimFW.

Proof

technique · direct
1.1

Regularity gives zero positive homology and the degree-zero calculation gives M/(x)M.

givenalgebra
2.1

Each term pRnRM is finite free because both factors are finite free, so this is a finite free resolution.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: 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.

Local Koszul H One Detects First Regularity Failure

Statement

Let (R,m) be Noetherian local, M finite nonzero, and xm. If the first failure of regularity occurs at xj, then H1(K(x;M))0.

Proof

technique · direct
1.1

Let x=(x1,,xj1) and N=M/(x)M. The preceding prefix is regular, so K(x;M) has zero positive homology and H0=N. The failure at xj gives 0AnnN(xj). The cone exact sequence therefore identifies H1(K(x,xj;M)) with this nonzero annihilator.

givenalgebra
2.1

Append the remaining entries one at a time. If L is the current nonzero first homology and the next entry is ym, the cone exact sequence injects L/yL into the new first homology. The module L is finite because it is homology of a bounded complex of finite modules over a Noetherian ring, and Nakayama gives L/yL0. Thus first homology remains nonzero through every later entry, proving H1(K(x;M))0.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

Local Koszul Acyclicity Inductive Converse

Statement

Let (R,m) be Noetherian local, M finite, and x=(x1,,xn)m be nonempty, with M/(x)M0. If K(x;M) has no positive homology, then the shorter complex is acyclic and the last element is injective on its preceding quotient.

Proof

technique · direct
1.1

Put C=K(x1,,xn1;M) and y=xn. For every j>0, the cone exact sequence and Hj+1(K(x;M))=0 show that multiplication by y on Hj(C) is surjective. Each Hj(C) is finite because C is a bounded complex of finite modules over the Noetherian ring R.

givenalgebra
2.1

Since ym, Nakayama applied to the surjections in step 1.1 gives Hj(C)=0 for every j>0. The segment of the same exact sequence ending in H1(K(x;M))=0 then shows that multiplication by y on H0(C)=M/(x1,,xn1)M is injective. These are the two asserted conclusions.

step 1.1algebra
TheoremStatement: Literature-sourcedProof: 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 Acyclicity Characterises Local Regular Sequences

Statement

For a finite module over a Noetherian local ring and xm with nonzero terminal quotient, x is regular if and only if Hi(K(x;M))=0 for all i>0.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Regular Sequences Give Acyclic Koszul Complexes, Local Koszul Acyclicity Inductive Converse.

Proof

technique · direct
1.1

If x is empty, its Koszul complex is concentrated in degree zero and the assumed nonzero terminal quotient is exactly the nonzero-module condition in the definition of an empty regular sequence. Thus the equivalence holds in this case. For nonempty x, regularity implies acyclicity by the forward theorem.

givenalgebra
2.1

Conversely, suppose x is nonempty and the Koszul complex is acyclic in positive degrees. The local converse lemma makes the last element injective on the quotient by the preceding entries and makes the shorter Koszul complex acyclic. Its terminal quotient is nonzero because it surjects onto M/(x)M. Iterating proves all ordered injectivity conditions, while the final nonzero quotient is assumed; hence x is regular.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: 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.

Local Koszul Acyclicity Iff Regular Sequence

Statement

For a finite module M over a Noetherian local ring, with xm and M/(x)M0, x is M-regular if and only if its positive Koszul homology vanishes.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Acyclicity Characterises Local Regular Sequences.

Proof

technique · direct
1.1

The forward direction is regular-sequence Koszul acyclicity.

givenalgebra
2.1

The reverse direction is the local converse; together with the terminal quotient hypothesis it gives regularity.

step 1.1algebra
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-06Open item page →

Koszul Regular And H One Regular Sequences

Definition

Let R be a commutative unital ring, let M be an R-module, and let x be a finite ordered sequence in R. Call x M-Koszul-regular when Hi(K(x;M))=0 for every i>0, and M-H1-regular when H1(K(x;M))=0; ordinary regularity is the preceding ordered definition.

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

Koszul Regular Implies H One Regular

Statement

Every M-Koszul-regular sequence is M-H1-regular.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Regular And H One Regular Sequences.

Proof

technique · direct
1.1

Koszul regularity says every positive homology group vanishes.

givenalgebra
2.1

Taking degree one is exactly H1-regularity.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: 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.

H One Regular Local Implies Koszul Regular

Statement

For finite M over Noetherian local (R,m) with xm, M-H1-regularity implies M-Koszul-regularity.

Facts & Assumptions

Proof

technique · direct
1.1

If M=0, every term of K(x;M) is zero and the conclusion is immediate. Suppose M0. Because (x)m, Nakayama shows that M/(x)M0; the same argument applies to every prefix quotient.

givenalgebra
2.1

If x were not regular, it would therefore have a first injectivity failure. The detection lemma would give H1(K(x;M))0, contradicting H1-regularity. Thus x is regular, and the local regularity criterion gives vanishing of every positive Koszul homology group.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: 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.

Regular Sequence Permutation Adjacent Swap

Statement

For finite M over a Noetherian local ring and a regular sequence in m, interchanging two adjacent terms preserves regularity.

Facts & Assumptions

Given: The ring, finite module, and regular sequence stated in the claim. The declared prerequisites used here are Regular Sequence On A Module, Local Koszul Acyclicity Iff Regular Sequence, and Koszul Complex Invariant Under Invertible Generator Change.

Proof

technique · direct
1.1

The local criterion makes the original regular sequence Koszul-acyclic. Interchanging two adjacent generators is multiplication by an invertible permutation matrix, so invariance under invertible generator change gives an isomorphic Koszul complex for the swapped sequence.

givenalgebra
2.1

The swapped sequence still lies in m and generates the same ideal, so its terminal quotient is the same nonzero module. Applying the reverse direction of the local criterion to its acyclic Koszul complex proves that it is regular.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: 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.

Regular Sequences Permutable Local

Statement

Every permutation of a regular sequence in the maximal ideal of a Noetherian local ring is regular on the finite module.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Regular Sequence Permutation Adjacent Swap.

Proof

technique · direct
1.1

Every permutation is a product of adjacent transpositions.

givenalgebra
2.1

Apply the adjacent-swap result successively under the unchanged local finite hypotheses.

step 1.1algebra
LemmaStatement: Literature-sourcedProof: 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.

Positive Powers Of A Regular Sequence Remain Regular

Statement

Under the same local finite hypotheses, x1a1,,xnan is regular whenever x1,,xn is regular and all ai>0.

Facts & Assumptions

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

Proof

technique · direct
1.1

For one non-zero-divisor x, if xam=0, repeated injectivity of x gives m=0; its quotient remains nonzero by the regularity convention.

givenalgebra
2.1

Use adjacent swaps to place one entry at a time, replace it by its positive power, and induct through the quotient stages.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: 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.

Regularity Notions Coincide Local Finite

Statement

For finite M over Noetherian local (R,m) and xm with nonzero terminal quotient, ordinary regularity, M-Koszul-regularity, and M-H1-regularity are equivalent.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Local Koszul Acyclicity Iff Regular Sequence, Koszul Regular Implies H One Regular, H One Regular Local Implies Koszul Regular.

Proof

technique · direct
1.1

Regularity implies Koszul regularity, which implies H1-regularity.

givenalgebra
2.1

The local H1 implication and local acyclicity converse close the cycle.

step 1.1algebra
TheoremStatement: Literature-sourcedProof: 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.

Regularity Notions And Permutation Invariance Local

Statement

Let M be a finite module over a Noetherian local ring (R,m), and let xm satisfy M/(x)M0. Then ordinary, Koszul, and H1 regularity coincide. Moreover, every permutation of an ordinary M-regular sequence in m is M-regular.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Regularity Notions Coincide Local Finite, Regular Sequences Permutable Local.

Proof

technique · direct
1.1

The preceding corollary identifies the three notions in the stated local setting.

givenalgebra
2.1

The permutation corollary applies to ordinary regularity and equivalence transfers the conclusion.

step 1.1algebra
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Minimal Free Resolution Over A Local Ring

Definition

A finite free resolution FN over local (R,m) is minimal when di(Fi)mFi1 for every i>0.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Koszul Betti Numbers Over A Local Ring

Definition

When a Koszul resolution of N over a local ring is minimal, define its ith Koszul Betti number by βiK(N)=rankRKi.

LemmaStatement: Literature-sourcedProof: 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 Resolution Minimality Maximal Ideal Sequence

Statement

Let (R,m) be a local ring and let M be a finite free R-module. If xm and K(x;M) resolves M/(x)M, then it is a minimal free resolution because every differential matrix has entries among the xi.

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, Minimal Free Resolution Over A Local Ring, Koszul Differential Coordinate Formula.

Proof

technique · direct
1.1

In the exterior bases, every matrix coefficient of d is 0 or ±xi, hence belongs to m.

givenalgebra
2.1

Since M is finite free, every term MRpRn is finite free. The assumed acyclicity and degree-zero quotient therefore make the Koszul complex a finite free resolution, and the containment from step 1.1 is precisely the local minimality criterion.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: 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.

Complete Intersection Betti Numbers Binomial

Statement

For a length-n regular sequence in the maximal ideal of a local ring, the minimal Koszul resolution has βiK=(ni) for 0in and 0 otherwise.

Facts & Assumptions

Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Resolution Minimality Maximal Ideal Sequence, Koszul Betti Numbers Over A Local Ring, Exterior Algebra Basis Monomials.

Proof

technique · direct
1.1

The minimality lemma identifies the Koszul ranks with the Koszul Betti numbers. In degree i the free module has basis indexed by i-subsets of an n-set.

givenalgebra
2.1

There are (ni) such subsets and none in degrees outside 0,,n, giving the stated table.

step 1.1algebra

5 · Examples, counterexamples and false statements

None yet.

Sources