Formalization in Lean of faithfully flat descent of projectivity

TL;DR

This paper formalizes a fundamental result in commutative algebra about projectivity descent along faithfully flat ring maps using the Lean proof assistant, verifying a correction to classical proofs.

Contribution

It provides a formal proof of faithfully flat descent of projectivity in Lean, including Perry's correction to Raynaud and Gruson's classical result.

Findings

Formal proof of faithfully flat descent of projectivity in Lean

Verification of Perry's correction to classical algebraic results

Contribution to formal methods in commutative algebra

Abstract

We formalize in Lean the following foundational result in commutative algebra: Let $R \to S$ be a faithfully flat map of (not necessarily noetherian) commutative rings, and let $P$ be an arbitrary $R$-module. Then $P$ is projective over $R$ if and only if $S\otimes_R P$ is projective over $S$. This formalizes and verifies Perry's fix of a subtle gap in the classical work of Raynaud and Gruson, a result which is a key ingredient in the study of finitistic dimension of commutative noetherian rings.