FAGiL (Foundations of Algebraic Geometry in Lean4)

FAGiL consists of proof of theorems (proposition, lemmas, exercises ...) in Foundations of Algebraic Geometry (currently, we use September 2024 version) by Ravi Vakil implemented in Lean4.

Usage

The FAGiL is a standard lake package. So you can simply clone the repository and run

lake exe cache get
lake build

Guidelines

We adopt the same guideline as mathlib4, with following exceptions

• Naming convetion: we prefer to have an alias consistent with the book.
• Documentation style: Omit header comment unless you implement some theorem in a different way in the book Foundations of Algebraic Geometry.

Dependencies

• mathlib4