Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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 (R,m), minimality means that every positive differential matrix has entries in m. 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.

[F1]

finite local modules admit minimal free resolutions: Every finite module M over a nonzero Noetherian local ring (R,m,k) has an augmented resolution ⋯→F1→F0→M→0 by finite-rank free modules, with di(Fi)⊆mFi−1 for i>0. Such a resolution is called minimal; it need not be bounded. This extends the bounded terminology without changing it.

Proof

1.1F1given

The condition that an image lie in mFi−1 is exactly that all matrix entries lie in m, and is basis-independent. Since the complement of m consists of units, failure supplies a unit entry. This is the minimality convention of the existence lemma.

2.1step 1.1algebra∎

Move that entry to the first position, scale it to 1, and clear its row and column by elementary basis changes. The matrix becomes diag⁡(1,D). The identities di−1di=didi+1=0 force adjacent maps to vanish on or into the isolated coordinates; for i=1 the augmentation also vanishes there. Hence these coordinates form the direct summand 0→R→1R→0. Deleting it preserves exactness. Conversely an identity summand cannot have zero residue differential, while every matrix with entries in m does.

Depends on

Used by

Dependency tree · two levels

8 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