Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedaudited 2026-09-06
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Koszul Complex 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)=(⋀Rn⊗RM,d), where d=δ⊗id⁡M. Its degree-p term is ⋀pRn⊗RM for 0≤p≤n, and zero otherwise. Explicitly,

d(ei1∧⋯∧eip⊗m)=∑j=1p(−1)j−1ei1∧⋯eij^⋯∧eip⊗xijm.

The empty wedge is 1∈R. In particular d(ei⊗m)=1⊗xim in K0=R⊗RM, canonically identified with M by r⊗m↦rm with inverse m↦1⊗m. 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.

Depends on

Used by

Dependency tree · two levels

9 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