Formalization in Lean of faithfully flat descent of projectivity

Imagine you are trying to figure out if a massive, complex machine (a mathematical object called a "module") is built perfectly and efficiently (is "projective"). The machine is so big and complicated that you can't inspect every single gear and bolt at once.

This paper is about a brilliant shortcut: How to check if the whole machine is perfect by looking at a smaller, simpler version of it.

Here is the story of what the author, Liran Shaul, did, explained without the heavy math jargon.

The Big Problem: The "Mirror" Test

In the world of algebra, there is a rule called Faithfully Flat Descent. Think of it like a special mirror.

You have a machine $P$ in your workshop (Ring $R$ ).
You send it to a special factory $S$ (Ring $S$ ) that is "faithfully flat." This factory is like a perfect, high-resolution mirror that doesn't distort anything.
In the factory, the machine becomes $S \otimes P$ .

The Question: If the machine looks perfect in the factory mirror, does that mean the original machine in your workshop was perfect all along?
The Answer: Yes! But proving this wasn't easy.

The Historical Glitch

Back in the 1970s, two famous mathematicians (Raynaud and Gruson) wrote a paper claiming this "Mirror Test" worked. It became a cornerstone of modern algebra. However, decades later, another mathematician named Perry noticed a tiny crack in their proof—a missing step. It was like a bridge that looked solid but had a hidden gap in the middle.

For years, people used the bridge, hoping no one would fall through. Then, someone (Perry) fixed the gap. But in math, "someone said it's fixed" isn't enough. You need to be 100% sure.

The Solution: The Digital Architect (Lean)

This paper is about formalizing that fix. The author didn't just write a proof on paper; he translated the entire proof into a computer language called Lean.

Think of Lean as a super-strict robot architect. You can't tell the robot, "It's probably true." You have to give it every single logical brick. If there is even one missing brick, the robot refuses to build the tower.

The author built a tower over 10,000 lines of code long to prove that the "Mirror Test" is mathematically unbreakable.

The Toolkit: How They Built the Tower

To build this proof, the author had to invent several new tools because the robot's toolbox (the Mathlib library) was missing them. Here are the main tools, explained with analogies:

1. The "Peeling Onion" Strategy (Kaplansky Devissage)

The machine $P$ is too big to check all at once. The author used a strategy called Kaplansky Devissage.

Analogy: Imagine a giant onion. You can't eat the whole thing at once. Instead, you peel it layer by layer.
The Math: The author proved that any big machine can be broken down into a sequence of smaller, manageable layers (countably generated modules). If you can prove the "Mirror Test" works for these small layers, it works for the whole onion.

2. The "Infinite Lego" Set (Lazard's Theorem)

To understand the layers, they needed to know how they are built.

Analogy: Imagine you have a complex Lego structure. Lazard's Theorem says that any "flat" structure is actually just a giant pile of simple, finite Lego bricks glued together in a specific way.
The Math: This allowed the author to treat complex, infinite modules as if they were built from simple, finite building blocks, making them easier to analyze.

3. The "Universal Glue" (Pushouts and Domination)

The proof required connecting different parts of the machine.

Analogy: Imagine you have two different blueprints for a room. You need to glue them together perfectly. The author invented a "Pushout" tool, which is like a universal glue that ensures two different maps fit together without creating a gap.
The Math: They used this to show that if a map is "universally injective" (it never loses information, no matter what you mix it with), it behaves very predictably.

4. The "Stabilizing Wave" (Mittag-Leffler Condition)

This is the most abstract part.

Analogy: Imagine a wave moving through a crowd. Sometimes the crowd is chaotic. But if the wave is "Mittag-Leffler," it means that as the wave moves forward, the people stop changing their minds. The pattern stabilizes.
The Math: This condition ensures that when you are looking at an infinite sequence of approximations of your machine, the approximations eventually stop changing in a chaotic way. This stability is the key to proving the machine is "projective."

The Grand Finale: Putting It All Together

The author combined all these tools to fix the gap in the old proof:

Break it down: Use the "Peeling Onion" strategy to turn the giant machine into small, countable pieces.
Check the pieces: Use the "Stabilizing Wave" and "Infinite Lego" rules to prove that if the pieces look perfect in the mirror, they are perfect.
Rebuild: Show that if all the small pieces are perfect, the whole machine is perfect.
Verify: Run the whole logic through the Lean robot. The robot checked every single step and said, "Verified."

Why Does This Matter?

This isn't just about fixing an old paper. It's about trust.

For Mathematicians: It proves that a fundamental rule of algebra is rock-solid. We can now use this rule to solve other hard problems (like understanding the "dimension" of rings) without worrying about hidden errors.
For Computer Science: It shows that we can use computers to verify the deepest, most abstract human thoughts. It's a step toward a future where mathematical knowledge is stored in a database that is 100% error-free.

In short, Liran Shaul took a shaky bridge, reinforced it with digital steel, and proved it can hold the weight of the entire mathematical world.

Based on the paper "Formalization in Lean of Faithfully Flat Descent of Projectivity" by Liran Shaul, here is a detailed technical summary covering the problem, methodology, key contributions, results, and significance.

1. Problem Statement

The paper addresses the formalization and verification of Theorem I, a foundational result in commutative algebra concerning the descent of projectivity along faithfully flat maps. The theorem states:

Let $R \to S$ be a faithfully flat map of commutative rings (not necessarily Noetherian), 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$ .

Context and Motivation:

Historical Gap: This theorem was central to the proof in the influential 1976 paper by Raynaud and Gruson regarding the finitistic dimension of commutative Noetherian rings. However, as noted by Gruson, the original proof contained a subtle gap.
Prior Work: A complete proof was later provided in [6] (Theorem 9.6) and incorporated into the Stacks Project, but these proofs had not been peer-reviewed in the traditional sense, nor had they been mechanically verified.
Goal: The author aims to provide a rigorous, machine-checked proof of this theorem and its prerequisites using the Lean 4 theorem prover and the Mathlib library.

2. Methodology

The formalization required the development of a substantial new infrastructure within Lean 4, as many necessary concepts were missing from Mathlib. The approach involved:

Transfinite Induction and Devissage: The proof relies on reducing arbitrary modules to countably generated ones. This required implementing a Kaplansky devissage framework using ordinals to construct filtrations of modules where successive quotients are countably generated.
Category Theory and Limits: The formalization involved defining and working with inverse systems (specifically Mittag-Leffler systems) and direct limits (colimits). The author had to define a concrete inverse limit suitable for their needs, as the standard Mathlib definition was insufficient for their specific application.
Algebraic Constructions:
- Pushouts: A concrete construction of pushouts in the category of modules was implemented to handle domination criteria.
- Universal Injectivity: The concept of universally injective maps (maps that remain injective after tensoring with any module) was formalized, along with their lifting properties.
- Domination: The notion of one linear map "dominating" another (via kernel containment after tensoring) was formalized and linked to factorization through pushouts.
Code Volume: The project resulted in over 10,000 lines of code, developed from scratch, covering modules, ordinals, and specific algebraic theorems.

3. Key Contributions and Formalized Results

The paper details the formalization of several intermediate theorems that serve as the building blocks for the main result:

A. Kaplansky Devissage (Section 1)

Theorem: If a module $M$ is a direct sum of countably generated modules, then any direct summand of $M$ is also a direct sum of countably generated modules.
Contribution: Formalized the equivalence between a module being a direct sum of countably generated modules and the existence of a Kaplansky devissage (a transfinite filtration with specific properties). This allows the reduction of general projectivity problems to the countably generated case.

B. Lazard's Theorem and Direct Limits (Section 2)

Theorem: A module is flat if and only if it is a direct limit of finitely presented free modules.
Contribution: Formalized Lazard's theorem and the more basic fact that any module is a direct limit of finitely presented modules. This is crucial for characterizing flatness and projectivity.

C. Pushouts and Universal Injectivity (Sections 3 & 4)

Pushouts: Implemented the pushout of modules as a quotient of a direct sum, proving its universal property and its compatibility with base change (tensor products).
Universal Injectivity: Defined universally injective maps and proved that this property descends along faithfully flat maps. This is a critical tool for transferring properties from $S \otimes_R P$ back to $P$ .

D. Mittag-Leffler Conditions (Sections 5, 6, & 7)

Mittag-Leffler Inverse Systems: Formalized the condition that images of transition maps in an inverse system stabilize. Proved that such systems over countable directed sets have non-empty limits.
Mittag-Leffler Modules: Formalized the definition of a Mittag-Leffler module (Raynaud-Gruson). Established the equivalence between the module-theoretic definition and conditions involving direct limits and inverse systems of Hom-functors.
Key Lemma: Proved that a countably generated, flat, Mittag-Leffler module is projective. This is the core of Theorem II.

E. The Main Theorems (Section 8)

Theorem II (Characterization of Projectivity):
An $R$ -module $P$ is projective if and only if:
1. $P$ is flat.
2. $P$ is Mittag-Leffler.
3. $P$ is a direct sum of countably generated modules.
- Note: This holds even for non-commutative rings.
Theorem I (Faithfully Flat Descent of Projectivity):

$P$ is projective over $R$ $\iff$ $S \otimes_R P$ is projective over $S$ (given $R \to S$ is faithfully flat).
- Proof Strategy: The proof combines the descent of the Mittag-Leffler property and countable generation (via faithful flatness) with Theorem II. For the general case, it uses a transfinite induction argument (Kaplansky devissage) to reduce the problem to the countably generated case.

4. Results

Verification: The paper successfully compiles and verifies the entire logical chain in Lean 4.
Gap Closure: The formalization provides a peer-reviewed, machine-checked verification of the corrected proof of Theorem I, resolving the historical gap in the Raynaud-Gruson work.
Library Expansion: The work significantly expands the Mathlib library with new definitions and theorems regarding:
- Ordinal-based filtrations (devissage).
- Mittag-Leffler conditions for modules and inverse systems.
- Universal injectivity and domination of linear maps.
- Pushouts in the module category.

5. Significance

Mathematical Rigor: By formalizing this result, the paper eliminates any doubt regarding the correctness of the proof of faithfully flat descent of projectivity, a cornerstone of modern commutative algebra.
Foundation for Future Work: The developed infrastructure (Mittag-Leffler modules, transfinite devissage, universal injectivity) is reusable for other problems in commutative algebra, particularly those involving finitistic dimensions and non-Noetherian rings.
Methodological Benchmark: The paper demonstrates the feasibility of formalizing highly non-trivial, transfinite arguments in commutative algebra, serving as a model for future large-scale formalization projects in mathematics.
AI-Assisted Development: The author acknowledges the use of Large Language Models (Claude Opus) in generating parts of the Lean code, highlighting the emerging role of AI in assisting with formal proof development.

In summary, this paper is a landmark in the formalization of commutative algebra, providing a verified proof of a critical theorem that underpins the study of finitistic dimensions and establishing a robust framework for handling infinite generation and transfinite induction in the Lean ecosystem.