Adjunction forula WIP blueprint

Stream: maths

[Jack J Garzella]

Hi all, @Calvin Lee and I have been working on a WIP blueprint for proving the Adjunction Formula in Lean.

The proof has two main components, one (section two) which is mainly uses algebraic geometry machinery and some commutative algebra that is well within reach. Much of it piggy-backs off of work that is already being done in mathlib, e.g. Kahler differentials, Nakayama's lemma. The other component (section one) is entirely commutative algebra, dedicated to proving the following claim: A localization of a regular ring at a prime ideal is regular. This requires the Auslander-Buchsbaum-Serre theorem, which is a homological statement that will be a consumer of the homological machinery from LTE in one way or another.

As far as I can see, there are two reasonable choices for trying to prove Auslander-Buchsbaum-Serre: one can follow Bruns-Herzog and prove a bunch of facts about Ext, depth, and define Cohen-Macaulay rings, going through much of Bruns-Herzog chapter 1. Or, one can try to avoid this and develop the theory of Koszul homology, define DG-algebras, and prove a statement due to Serre using this machinery--though I'm not 100% sure this alternate proof is free of the notion of depth.

I'd be interested to hear feedback about which proof might be a better option to do.

The blueprint can be found here, notice that many proofs and statements are missing but the dependency graph is mostly there, with one major exception--the choice of proof of Auslander-Buchsbaum-Serre.

We're hoping to do a bunch of work on the side of things that doesn't need homological algebra, and then work on the homological bits later after having though through it a bit more.