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.
minimal free resolution differentials land in maximal ideal
Statement
For an augmented degreewise finite free resolution over a nonzero Noetherian local ring , minimality means that every positive differential matrix has entries in . Equivalently no positive differential admits a unit pivot, or a nonzero two-term identity direct summand. A unit pivot can be cancelled without changing the resolved module.
Facts & Assumptions
Given: The objects and hypotheses in the statement. We work with the Axiom of Choice; cited dependent-choice and resolution-existence hypotheses are retained.
finite local modules admit minimal free resolutions: Every finite module over a nonzero Noetherian local ring has an augmented resolution by finite-rank free modules, with for . Such a resolution is called minimal; it need not be bounded. This extends the bounded terminology without changing it.
Proof
The condition that an image lie in is exactly that all matrix entries lie in , and is basis-independent. Since the complement of consists of units, failure supplies a unit entry. This is the minimality convention of the existence lemma.
Move that entry to the first position, scale it to , and clear its row and column by elementary basis changes. The matrix becomes . The identities force adjacent maps to vanish on or into the isolated coordinates; for the augmentation also vanishes there. Hence these coordinates form the direct summand . Deleting it preserves exactness. Conversely an identity summand cannot have zero residue differential, while every matrix with entries in does.
Depends on
Used by
Dependency tree · two levels
5 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
- Definition 1.49 and discussion after Lemma 1.50, pp.23–24 (standard reference, not scraped)