Lean 中 faithfully flat descent 关于 projectivity 的形式化

我们在 Lean 中形式化化以下交换代数中的基础结果：设 $R \to S$ 为一般交换环间的faithfully flat映射，$P$ 为任意 $R$-模。若 $P$ 在 $R$ 上为自由模，则 $S\otimes_r P$ 在 $S$ 上为自由模。此结果形式化并验证了 Perry 对 Raynaud-Gruson 经典著作中细微缺口的修正，这一结果是研究交换非诺伊尔纳环的 finitistic 维数关键要素。