← All papers
Formalization in Lean of faithfully flat descent of projectivity
math.AC
Mar 4, 2026 · v1
TL;DR
Formalizes in Lean that faithfully flat descent preserves projectivity of an arbitrary module, verifying Perry's fix of a gap in Raynaud-Gruson.
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.
Problem
A foundational result in commutative algebra states that for a faithfully flat ring map R -> S, a module P is projective over R if and only if S tensor P is projective over S. Perry's fix of a subtle gap in the classical proof by Raynaud and Gruson had not been machine-verified.
Approach
The authors formalize this result in Lean, verifying Perry's corrected proof. The formalization covers faithfully flat descent of projectivity for arbitrary (not necessarily noetherian) commutative rings and arbitrary R-modules.
Results
The result is fully formalized in Lean. It serves as a key ingredient in the study of finitistic dimension of commutative noetherian rings.