Alphabeta MathHow 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.
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.
Depends on
Used by
- Koszul Complex Resolves A Regular Quotient Corollary
- Dense relative-dimension strata in flat finitely presented fibres Lemma
- Depth from first nonzero Koszul cohomology Lemma
- Koszul resolutions and restriction to flat fibres Lemma
- Koszul sheaf Ext of a smooth regular immersion is concentrated in codimension Lemma
- Local flatness criterion by regular parameters Lemma
- Local Koszul H One Detects First Regularity Failure Lemma
- Poincare cohomology at the identity Lemma
- Smooth closed immersion is regular with exact conormal sequence Lemma
- Smooth immersions, their conormal sequence, deformation charts and smooth sections Lemma
- The first-layer relations of a closed MOY resolution form a regular sequence Lemma
- Chevalley–Eilenberg cohomology computes Ext of the trivial module Proposition
- Koszul Acyclicity Characterises Local Regular Sequences Theorem
- The diagonal Koszul complex is a finite free resolution of R Theorem
Dependency tree · two levels
10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- The Stacks Project, Koszul complexes and regular sequences (standard reference, not scraped)