Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalization in Lean of faithfully flat descent of projectivity

Liran Shaul

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.

Formalization in Lean of faithfully flat descent of projectivity

Abstract

We formalize in Lean the following foundational result in commutative algebra: Let be a faithfully flat map of (not necessarily noetherian) commutative rings, and let be an arbitrary -module. Then is projective over if and only if is projective over . 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.
Paper Structure (9 sections, 16 theorems, 10 equations)

This paper contains 9 sections, 16 theorems, 10 equations.

Table of Contents

  1. Introduction
  2. Kaplansky Devissage
  3. Lazard theorem
  4. Pushout of modules
  5. Universally injective maps
  6. Mittag-Leffler Inverse Systems
  7. Domination
  8. Mittag-Leffler modules
  9. Projective modules and faithfully flat maps

Key Result

Theorem 1

Let $R \to S$ be a faithfully flat map of commutative rings, and let $P$ be an $R$-module. Then $P$ is projective over $R$ if and only if the $S$-module $S\otimes_R P$ is projective over $S$.

Theorems & Definitions (16)

  • Theorem 1
  • Theorem 2
  • Theorem 1.1
  • Theorem 2.1
  • Lemma 2.1
  • Theorem 3.1
  • Theorem 4.1
  • Theorem 4.2
  • Theorem 5.1
  • Theorem 5.2
  • ...and 6 more