Formalization of Auslander–Buchsbaum–Serre criterion in Lean4
Naillin Guan and Yongle Hu
我们在Lean4定理证明器中形式化了Auslander–Buchsbaum–Serre判据的完整证明。对于局部环，我们没有采用众所周知的证明方法——即考虑环模正则序列的商来计算投射维数，并使用Koszul复形来证明余切空间的维数不超过整体维数——而是通过极大Cohen–Macaulay模和Ferrand–Vasconcelos定理的弱化版本证明了该判据，这种方法更适用于形式化过程和mathlib的当前发展。我们的形式化包括了深度以及Cohen–Macaulay模和环的构造，这些在判据的证明中经常使用。我们还发展了相关结果，包括Cohen–Macaulay环的无混合性定理和Hilbert合冲定理。
We formalized a complete proof of the Auslander–Buchsbaum–Serre criterion in the Lean4 theorem prover. For a local ring, rather than following the well-known proof that considers the residue field as the quotient of the ring by a regular sequence to compute projective dimension and uses the Koszul complex to show the dimension of the cotangent space is at most the global dimension, we prove the criterion via maximal Cohen–Macaulay modules and a weakened version of the Ferrand–Vasconcelos theorem...
