Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalization of Auslander--Buchsbaum--Serre criterion in Lean4

Naillin Guan, Yongle Hu

TL;DR

This work presents a comprehensive Lean4 formalization of the Auslander--Buchsbaum--Serre criterion, anchoring regularity of Noetherian local rings to finite global dimension via a depth framework built on Ext vanishing. It develops depth, AB formula, Ischebeck, and Cohen--Macaulay theory (including unmixedness and universal catenarity), culminating in a weakened Ferrand--Vasconcelos route to deduce regularity from finite projective dimension of the maximal ideal. A key strategy is proving that maximal Cohen--Macaulay modules over regular local rings are free, which together with AB yields the equality gldim = dim for regular local rings and supports the AB--Serre criterion. The project also delivers substantial infrastructure for future formalizations in commutative algebra, including extensions to Cohen--Macaulay theory over arbitrary rings and related flatness/normality themes, with Hilbert's Syzygy Theorem as a notable corollary.

Abstract

We present a comprehensive formalization in the Lean4 theorem prover of the Auslander--Buchsbaum--Serre criterion, which characterizes regular local rings as those Noetherian local rings with finite global dimension. Rather than following the well-known proof that computes the projective dimension of the residue field via quotient by regular sequences and uses the Koszul complex to bound the cotangent space dimension by the global dimension, our approach is built systematically on the formalization of depth defined via the vanishing of Ext functors. We establish key homological results including Rees' theorem, the Auslander--Buchsbaum formula, and Ischebeck's theorem, and further develop the theories of Cohen--Macaulay modules and rings, including a complete formalization of the unmixedness theorem for Cohen--Macaulay rings. To prove the Auslander--Buchsbaum--Serre criterion, we show that maximal Cohen--Macaulay modules over regular local rings are free and establish a weakened form of the Ferrand--Vasconcelos theorem specific for the unique maximal ideal. As corollaries, we deduce that regularity can be checked at maximal ideals and formalize Hilbert's Syzygy Theorem. This work demonstrates how homological algebra can be effectively employed in the formalization of commutative algebra, providing extensive infrastructure for future developments in the field.

Formalization of Auslander--Buchsbaum--Serre criterion in Lean4

TL;DR

This work presents a comprehensive Lean4 formalization of the Auslander--Buchsbaum--Serre criterion, anchoring regularity of Noetherian local rings to finite global dimension via a depth framework built on Ext vanishing. It develops depth, AB formula, Ischebeck, and Cohen--Macaulay theory (including unmixedness and universal catenarity), culminating in a weakened Ferrand--Vasconcelos route to deduce regularity from finite projective dimension of the maximal ideal. A key strategy is proving that maximal Cohen--Macaulay modules over regular local rings are free, which together with AB yields the equality gldim = dim for regular local rings and supports the AB--Serre criterion. The project also delivers substantial infrastructure for future formalizations in commutative algebra, including extensions to Cohen--Macaulay theory over arbitrary rings and related flatness/normality themes, with Hilbert's Syzygy Theorem as a notable corollary.

Abstract

We present a comprehensive formalization in the Lean4 theorem prover of the Auslander--Buchsbaum--Serre criterion, which characterizes regular local rings as those Noetherian local rings with finite global dimension. Rather than following the well-known proof that computes the projective dimension of the residue field via quotient by regular sequences and uses the Koszul complex to bound the cotangent space dimension by the global dimension, our approach is built systematically on the formalization of depth defined via the vanishing of Ext functors. We establish key homological results including Rees' theorem, the Auslander--Buchsbaum formula, and Ischebeck's theorem, and further develop the theories of Cohen--Macaulay modules and rings, including a complete formalization of the unmixedness theorem for Cohen--Macaulay rings. To prove the Auslander--Buchsbaum--Serre criterion, we show that maximal Cohen--Macaulay modules over regular local rings are free and establish a weakened form of the Ferrand--Vasconcelos theorem specific for the unique maximal ideal. As corollaries, we deduce that regularity can be checked at maximal ideals and formalize Hilbert's Syzygy Theorem. This work demonstrates how homological algebra can be effectively employed in the formalization of commutative algebra, providing extensive infrastructure for future developments in the field.

Paper Structure

This paper contains 33 sections, 74 theorems, 11 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Associated Primes
  4. Krull Dimension of Module
  5. Dimension of Polynomial Rings
  6. Regular Sequence Under Flat Base Change
  7. Projective Dimension
  8. Global Dimension
  9. Definition of Depth and Related Results
  10. Definition of Depth
  11. The Auslander--Buchsbaum Theorem
  12. The Ischebeck Theorem
  13. Cohen--Macaulay Modules and Rings
  14. Unmixedness Theorem for Cohen--Macaulay Rings
  15. Universally Catenary
  16. ...and 18 more sections

Key Result

Theorem 1.1

Let $(R, \mathfrak{m})$ be a Noetherian local ring and let $M$ be a non-trivial finitely generated $R$-module. If projective dimension of $M$ is finite, then

Theorems & Definitions (120)

  • Theorem 1.1: Auslander--Buchsbaum
  • Theorem 1.2
  • Definition 1.3
  • Proposition 1.4
  • Theorem 1.5: stacks-project
  • Proposition 1.6
  • Theorem 1.7: Ferrand--Vasconcelos, CM_ring
  • Proposition 1.8
  • Theorem 1.9
  • Theorem 1.10: Hilbert's Syzygy
  • ...and 110 more