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 Complexes and Regular Sequences
1 · Prerequisites
- Abelian Categories
- Binary Operations, Monoids, Groups and Subgroups
- Cardinal Arithmetic, Cofinality and the Alephs
- Categories, Functors and Natural Transformations
- Chain Complexes and Homology
- Chain Conditions, Semisimple Modules and the Wedderburn–Artin Theorem
- Chain Homotopy and the Homotopy Category
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Determinants of Matrices over a Commutative Ring
- Exactness and the Member Calculus
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Free Modules, Exact Sequences, Projective and Injective Modules
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Limits and Colimits
- Linear Independence, Bases and Dimension
- Localisation of Modules and Support
- Long Exact Sequences in Homology
- Mapping Cones Cylinders and Chain Triangles
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinal Arithmetic and the First Uncountable Ordinal
- Ordinals, Cardinals, and Transfinite Recursion
- Preadditive and Additive Categories and Biproducts
- Reflective Subcategories and the Adjoint Functor Theorems
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Roots, Rational Powers, and Classical Inequalities
- Set Theory Beyond Choice: Recorded, Not Proved Here
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tensor Products of Modules
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Diagram Lemmas in an Abelian Category
- The Field of Fractions and Localisation
- The ZFC Axioms and the Basic Set Constructions
- Universal Properties, Representables and the Yoneda Lemma
- Vector Spaces, Linear Subspaces, Span and Direct Sums
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
Exterior Algebra Of A Finite Free Module
Definition
Let be a commutative unital ring and let be a finite free -module with ordered basis . Define , graded by tensor degree; write for .
Exterior Algebra Basis Monomials
Statement
For every , the wedges with form an -basis of ; in particular it is zero for .
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
Sort wedges using anticommutation and delete repetitions using , so the increasing wedges span.
The alternating determinant map to the free module on -subsets kills the exterior relations and sends these wedges to distinct basis elements, proving independence.
Exterior Multiplication Koszul Sign Rule
Statement
If is distinct from , then , while when .
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
Move across precisely the factors indexed below ; each adjacent swap contributes .
If already occurs, the wedge contains a square and is zero; this remains true in characteristic .
Koszul Complex Of A Sequence With Coefficients
Definition
Let be a commutative unital ring, let be a finite ordered sequence in , and let be an -module. On , with standard basis , let be the -linear graded derivation of degree with and ; thus for homogeneous of degree .
The Koszul complex with coefficients in is , where . Its degree- term is for , and zero otherwise. Explicitly,
The empty wedge is . In particular in , canonically identified with by with inverse . The differential out of degree zero is zero. The derivation respects the exterior relations and the two orders of deleting distinct factors cancel in , so these maps form a chain complex. For this is in degree zero under the same identification.
Koszul Differential Coordinate Formula
Statement
For , .
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
Apply the graded Leibniz rule to the ordered wedge and use .
Passing the differential through degree-one factors gives , yielding the formula.
Koszul Differential Square Pairwise Cancellation
Statement
The two terms of obtained by deleting and in opposite orders have equal coefficient and opposite sign; hence .
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
Fix two deleted positions . Deleting then has sign , while the reverse order has sign ; these differ by and have the same scalar .
Every summand of has a unique unordered pair of deleted indices, so the pairs cancel, including in characteristic where and the two equal terms add to .
Koszul Differential Is Well Defined And Squares To Zero
Statement
The derivation defining annihilates the exterior relations, so it descends to , and its square is zero. Thus 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
The graded derivation sends to and therefore respects the alternating quotient. Its coordinate action is the stated deletion formula.
The pairwise cancellation calculation proves , so the graded modules and this differential satisfy the chain-complex axioms.
Empty Koszul Complex Is The Coefficient Module
Statement
For the empty sequence, is in degree and 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
For the zero free module, only is nonzero.
Tensoring with gives in degree zero and zero elsewhere, with zero differential.
One Element Koszul Complex
Statement
Let be a commutative unital ring, let be an -module, and let . Then is , with the left copy in 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
For one basis element, the only exterior powers are and .
The defining differential sends to , producing the displayed two-term complex.
One Element Koszul Homology
Statement
For , , , and for .
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
The sole differential is multiplication by , whose cokernel is .
Its kernel is and no other chain groups occur.
Basic Koszul Homology
Statement
For a finite sequence , , for , and .
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
The image in degree zero is , so .
There are no degrees above , and the top differential kills exactly when every kills .
Koszul Complex Concatenation Tensor Isomorphism
Statement
For finite sequences , the graded tensor-product identification gives a signed chain isomorphism .
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
The exterior algebra of the direct sum of the two based free modules is the graded tensor product of their exterior algebras.
Its total differential agrees termwise with the Koszul deletion differential.
Koszul Append One Element Mapping Cone Identification
Statement
If , then is chain-isomorphic to the mapping cone of multiplication by on .
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
Split as . Send the second summand to the shifted cone summand.
The coordinate formula gives , exactly the cone differential; hence the splitting is a chain isomorphism.
Koszul Mapping Cone Homology Exact Sequence
Statement
Appending yields the exact sequence .
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
The cone identification gives the degreewise split short exact sequence .
Its connecting map is multiplication by (check it on a cycle in the shifted summand), so the long exact homology sequence is the displayed one.
Koszul Concatenation And Mapping Cone
Statement
The concatenation isomorphism and the append-one mapping-cone identification are natural in 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
The direct-sum exterior identification supplies the signed concatenation chain isomorphism.
Splitting off the final basis vector gives its multiplication cone, whose long exact sequence gives the stated package.
Koszul Generator Contraction Homotopy
Statement
For each , exterior multiplication by is a degree- homotopy satisfying on .
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
Let . The graded Leibniz rule gives .
Thus is a chain homotopy from multiplication by to zero, with no division or characteristic assumption.
Sequence Ideal Annihilates Koszul Homology
Statement
Every , hence the ideal , annihilates every .
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
For each generator, the contraction identity is .
Thus each acts trivially on homology, hence so does every element of .
Koszul Generators Act Null Homotopically
Statement
Multiplication by each generator on 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
Exterior multiplication by satisfies .
This is a chain homotopy from multiplication by to zero, so its homology action vanishes.
Koszul Homology Supported On Sequence Vanishing Set
Statement
For every , .
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
The sequence ideal annihilates each homology module.
A prime in its support contains an annihilator of a nonzero element and therefore contains .
Koszul Complex Localises Termwise
Statement
For a multiplicative subset , localization gives a natural chain isomorphism .
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
Localization commutes with finite direct sums and with the finite free exterior bases, sending to .
The coordinate formula is preserved term by term because , so this degreewise isomorphism is a chain isomorphism.
Koszul Homology Localises
Statement
Let be a commutative unital ring, let be an -module, let be a finite sequence in , and let be a multiplicative subset. For every , .
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
Exact localization commutes with the kernel/image quotient defining homology.
The termwise localization chain isomorphism identifies the result with the claimed localized Koszul homology.
Koszul Complex Flat Base Change
Statement
For a flat map , there is a natural chain isomorphism .
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
In degree , base change sends to ; the exterior basis makes this an isomorphism.
The two differentials agree on every basis wedge by , which proves the chain claim.
Koszul Homology Flat Base Change
Statement
For flat , for every .
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
Flat tensoring is exact and therefore commutes with homology quotients.
The base-changed complex is the Koszul complex on with coefficient .
Koszul Generator Matrix Chain Map
Statement
If , the transpose matrix defines an exterior map inducing a chain map .
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
Let send the th basis vector to . The assumed identity makes the degree-one squares commute.
Extending by exterior powers respects wedge products, and the derivation rule then makes the resulting map commute with the differentials in every degree.
Koszul Complex Invariant Under Invertible Generator Change
Statement
If and the matrix is invertible, the induced generator-matrix chain map is an isomorphism .
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
The matrix chain map is defined by exterior powers of the generator map.
The inverse matrix induces its inverse in every exterior degree, so the complexes are isomorphic.
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
Termwise localization and flat-base-change maps are chain isomorphisms and exactness supplies their homology conclusions.
An invertible generator matrix has an inverse exterior chain map; all maps commute with coefficient-module maps by construction.
Regular Sequence On A Module
Definition
Let be a commutative unital ring, let be an -module, and let be a finite ordered sequence in . The sequence is -regular when and multiplication by is injective on it for every , and .
Regular Sequence First Element Boundary
Statement
A nonempty -regular sequence has , has first element a non-zero-divisor on , 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
At the first stage the definition requires injectivity of on .
It also requires all stage quotients, especially and the terminal quotient, to be nonzero; units and therefore fail.
Regular Sequence Tail On Quotient
Statement
A nonempty sequence is -regular if and only if is injective on and is regular on .
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
Separate the first condition: must be injective on .
Every remaining condition is precisely the regularity condition for the tail on , including the nonzero terminal quotient.
Initial Subsequences Of A Regular Sequence Are Regular
Statement
Every initial subsequence of an -regular sequence is regular on .
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
Each injectivity requirement for an initial segment occurs among those of the full sequence.
Its terminal quotient is an already-required nonzero intermediate quotient.
Localisation And Faithfully Flat Base Change Of Regular Sequences
Statement
An -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
Localization preserves injectivity, so each regularity condition survives; the stated nonzero localized terminal quotient prevents the convention from failing at the end.
Faithfully flat tensoring preserves and reflects injectivity and nonzero modules. Apply this successively to the quotient stages to obtain the base-change assertion.
Regular One Element Koszul Acyclicity
Statement
If multiplication by is injective on nonzero and , then has zero positive homology and resolves .
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
The one-element computation identifies positive homology with the kernel of multiplication by .
Injectivity makes that kernel zero and degree zero is the stated quotient.
Regular Sequence Koszul Acyclicity Induction
Statement
If for every and multiplication by is injective on , then all positive homology of 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
Put . By hypothesis for , while by the basic Koszul-homology calculation.
The mapping-cone exact sequence for identifies its with the kernel of multiplication by on , because ; this kernel is zero by hypothesis. For , the adjacent groups and both vanish, so exactness gives .
Regular Sequences Give Acyclic Koszul Complexes
Statement
Every finite -regular sequence is -Koszul-regular: for .
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
For the empty sequence the Koszul complex is in degree zero, so the conclusion is immediate. For length one it is the one-element calculation.
Suppose the result holds for an initial segment . Regularity says that the next element acts injectively on . The induction lemma applied to the already acyclic therefore makes acyclic in positive degrees. Induction on the length proves the claim.
Koszul Complex Resolves A Regular Quotient
Statement
If is finite free and is -regular, then is a finite free resolution of .
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, with the product basis, and .
Proof
Regularity gives zero positive homology and the degree-zero calculation gives .
Each term is finite free because both factors are finite free, so this is a finite free resolution.
Local Koszul H One Detects First Regularity Failure
Statement
Let be Noetherian local, finite nonzero, and . If the first failure of regularity occurs at , then .
Facts & Assumptions
Given: The ring, module, sequence, and first failed index stated in the claim. The declared prerequisites used here are Koszul Mapping Cone Homology Exact Sequence, Regular Sequences Give Acyclic Koszul Complexes, Regular Sequence On A Module, A local ring is a nonzero commutative ring with a unique maximal ideal, Left and right Noetherian rings, Noetherian modules: every submodule is finitely generated, Generated submodule, cyclic and finitely generated modules, module basis and free module, and Assuming the Axiom of Choice, Nakayama's lemma.
Proof
Let and . The preceding prefix is regular, so has zero positive homology and . The failure at gives . The cone exact sequence therefore identifies with this nonzero annihilator.
Append the remaining entries one at a time. If is the current nonzero first homology and the next entry is , the cone exact sequence injects into the new first homology. The module is finite because it is homology of a bounded complex of finite modules over a Noetherian ring, and Nakayama gives . Thus first homology remains nonzero through every later entry, proving .
Local Koszul Acyclicity Inductive Converse
Statement
Let be Noetherian local, finite, and be nonempty, with . If has no positive homology, then the shorter complex is acyclic and the last element is injective on its preceding quotient.
Facts & Assumptions
Given: The rings, finite sequences, modules, and local hypotheses stated in the claim. The declared prerequisites used here are Koszul Mapping Cone Homology Exact Sequence, Regular Sequence On A Module, A local ring is a nonzero commutative ring with a unique maximal ideal, Left and right Noetherian rings, Noetherian modules: every submodule is finitely generated, Generated submodule, cyclic and finitely generated modules, module basis and free module, Assuming the Axiom of Choice, Nakayama's lemma.
Proof
Put and . For every , the cone exact sequence and show that multiplication by on is surjective. Each is finite because is a bounded complex of finite modules over the Noetherian ring .
Since , Nakayama applied to the surjections in step 1.1 gives for every . The segment of the same exact sequence ending in then shows that multiplication by on is injective. These are the two asserted conclusions.
Koszul Acyclicity Characterises Local Regular Sequences
Statement
For a finite module over a Noetherian local ring and with nonzero terminal quotient, is regular if and only if for all .
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
If 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 , regularity implies acyclicity by the forward theorem.
Conversely, suppose 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 . Iterating proves all ordered injectivity conditions, while the final nonzero quotient is assumed; hence is regular.
Local Koszul Acyclicity Iff Regular Sequence
Statement
For a finite module over a Noetherian local ring, with and , is -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
The forward direction is regular-sequence Koszul acyclicity.
The reverse direction is the local converse; together with the terminal quotient hypothesis it gives regularity.
Koszul Regular And H One Regular Sequences
Definition
Let be a commutative unital ring, let be an -module, and let be a finite ordered sequence in . Call -Koszul-regular when for every , and --regular when ; ordinary regularity is the preceding ordered definition.
Koszul Regular Implies H One Regular
Statement
Every -Koszul-regular sequence is --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
Koszul regularity says every positive homology group vanishes.
Taking degree one is exactly -regularity.
H One Regular Local Implies Koszul Regular
Statement
For finite over Noetherian local with , --regularity implies -Koszul-regularity.
Facts & Assumptions
Given: The ring, finite module, and sequence stated in the claim. The declared prerequisites used here are Koszul Regular And H One Regular Sequences, Local Koszul H One Detects First Regularity Failure, Local Koszul Acyclicity Iff Regular Sequence, and Assuming the Axiom of Choice, Nakayama's lemma.
Proof
If , every term of is zero and the conclusion is immediate. Suppose . Because , Nakayama shows that ; the same argument applies to every prefix quotient.
If were not regular, it would therefore have a first injectivity failure. The detection lemma would give , contradicting -regularity. Thus is regular, and the local regularity criterion gives vanishing of every positive Koszul homology group.
Regular Sequence Permutation Adjacent Swap
Statement
For finite over a Noetherian local ring and a regular sequence in , 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
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.
The swapped sequence still lies in 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.
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
Every permutation is a product of adjacent transpositions.
Apply the adjacent-swap result successively under the unchanged local finite hypotheses.
Positive Powers Of A Regular Sequence Remain Regular
Statement
Under the same local finite hypotheses, is regular whenever is regular and all .
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
For one non-zero-divisor , if , repeated injectivity of gives ; its quotient remains nonzero by the regularity convention.
Use adjacent swaps to place one entry at a time, replace it by its positive power, and induct through the quotient stages.
Regularity Notions Coincide Local Finite
Statement
For finite over Noetherian local and with nonzero terminal quotient, ordinary regularity, -Koszul-regularity, and --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
Regularity implies Koszul regularity, which implies -regularity.
The local implication and local acyclicity converse close the cycle.
Regularity Notions And Permutation Invariance Local
Statement
Let be a finite module over a Noetherian local ring , and let satisfy . Then ordinary, Koszul, and regularity coincide. Moreover, every permutation of an ordinary -regular sequence in is -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
The preceding corollary identifies the three notions in the stated local setting.
The permutation corollary applies to ordinary regularity and equivalence transfers the conclusion.
Minimal Free Resolution Over A Local Ring
Definition
A finite free resolution over local is minimal when for every .
Koszul Betti Numbers Over A Local Ring
Definition
When a Koszul resolution of over a local ring is minimal, define its th Koszul Betti number by .
Koszul Resolution Minimality Maximal Ideal Sequence
Statement
Let be a local ring and let be a finite free -module. If and resolves , then it is a minimal free resolution because every differential matrix has entries among the .
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
In the exterior bases, every matrix coefficient of is or , hence belongs to .
Since is finite free, every term 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.
Complete Intersection Betti Numbers Binomial
Statement
For a length- regular sequence in the maximal ideal of a local ring, the minimal Koszul resolution has for and 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
The minimality lemma identifies the Koszul ranks with the Koszul Betti numbers. In degree the free module has basis indexed by -subsets of an -set.
There are such subsets and none in degrees outside , giving the stated table.
5 · Examples, counterexamples and false statements
None yet.