Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passverified 2026-09-23 (gpt-6-sol)
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.

projective dimension from last nonzero betti number

Statement

Assume the Axiom of Choice. For a nonzero finite module M over a nonzero Noetherian local ring, pd⁡RM=sup⁡{i≥0:βiR(M)≠0}, allowing infinity. For each integer q≥0, pd⁡RM≤q if and only if Tor⁡q+1R(k,M)=0.

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]

betti number is rank in minimal resolution: For every minimal degreewise finite free resolution F∙→M of a finite module over a nonzero Noetherian local ring, βiR(M)=rank⁡RFi for all i≥0.

[F2]

Projective dimension of an object: Assume projective resolutions are supplied or exist in the relevant class. The projective dimension of M is pd⁡(M)=inf⁡{d≥0:M has a projective resolution of length d}, with value ∞ if this set is empty. A length-zero projective resolution exists exactly when M is projective.

[F3]

Projective dimension at most n iff the nth syzygy is projective: Let A be an abelian category with enough projectives, fix a projective resolution P∙→M, and let n≥1. Then pd⁡(M)≤n⟺ΩPn(M) is projective. In particular, the condition is independent of the chosen projective resolution.

[F4]

A finite flat module over a local ring is free: The standard theorem holds over arbitrary local rings; the proof written here is the Noetherian local case. Let (R,m) be a Noetherian local ring and let M be a finite flat R-module. Then M is free.

[F5]

Projective left and right modules are flat over an arbitrary ring: Every projective left or right module over an arbitrary ring is flat on its appropriate side.

[F6]

Assuming the Axiom of Choice, Nakayama's lemma: Assume the Axiom of Choice. Let R be a commutative ring, let I⊴R satisfy I⊆J(R), and let M be a finitely generated left R-module. If IM=M, then M=0.

[F7]

The balanced Tor bifunctor: For a right R-module N, a left R-module M, and i≥0, define Tor⁡iR(N,M) to be either Hi(N⊗RP∙) for a projective resolution of M or Hi(Q∙⊗RM) for a projective resolution of N, identified by the preceding natural balance isomorphism. On maps it uses the homology maps induced by comparison maps; coherence makes this a well-defined covariant bifunctor.

[F8]

minimal free resolution reduces to zero differential: Reducing a minimal degreewise finite free resolution modulo m gives the zero differential, so Tor⁡iR(k,M)≅k⊗RFi.

[F9]

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.1givenF2F6F7F8F9algebra

Under AC, [F9] supplies a minimal degreewise finite free resolution F∙→M; AC also meets the premise of Nakayama in [F6]. By [F7], the zero differential in [F8] identifies Tor⁡q+1R(k,M) with Fq+1/mFq+1. Its vanishing and Nakayama give Fq+1=0. Exactness then gives ker⁡(Fq→Fq−1)=0 (using the augmentation when q=0), so the truncated complex is a length-q free resolution. Also Fq+2=ker⁡dq+2=im⁡dq+3⊆mFq+2, so Nakayama prevents a restart, and the same argument applies successively in every subsequent degree.

1.2F3F5F4F2F7

Conversely, if pd⁡M≤q, a projective resolution of length at most q computes Tor and gives zero in every degree above q. The syzygy criterion also gives a finite free terminating resolution: for q≥1 its finite projective syzygy is flat and hence free; for q=0 apply the same freeness result directly to M.

2.1F1F6step 1.1step 1.2∎

Since M≠0, Nakayama gives β0(M)>0. The two implications show that the last nonzero degree equals projective dimension when finite; if there is no finite bound, nonzero Betti degrees are unbounded and both sides are infinite.

Depends on

Used by

Dependency tree · two levels

34 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