Syzygies and free resolutions

Free resolutions of modules over polynomial rings, Hilbert's syzygy theorem, and graded Betti numbers and Poincaré series of multigraded modules.

TheoremHilbert's syzygy theorem#✓fully proved

Let \(k\) be a field, let \(n\) be a natural number, and let \(M\) be a finitely generated module over the polynomial ring \(k[X_1, \dots, X_n]\) in \(n\) variables. Then \(M\) has projective dimension at most \(n\) in the category of \(k[X_1, \dots, X_n]\)-modules.

theorem hilbert_syzygy
    {k : Type*} [Field k]
    {n : ℕ}
    {M : Type*} [AddCommGroup M] [Module (MvPolynomial (Fin n) k) M]
    [Module.Finite (MvPolynomial (Fin n) k) M] :
    CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of (MvPolynomial (Fin n) k) M) n

Sources

• D. Hilbert, Math. Ann. 36 (1890) 473–534 finite free resolution length ≤n; Lang, Algebra; Lean states field case k[X₁, …, Xₙ] with HasProjectiveDimensionLE n and n=0 field case.

Used by 1

Used byExistence of finite multigraded free resolutions

• Multigraded Betti numbers and Poincaré series

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.