Facts on sheaves and schemes via constructive logic

Stream: maths

[Thomas Eckl]

Some days ago, I saw Ingo Blechschmidt's thesis from 2017 on the arXiv. As far as I understood it, it explains how properties of and facts on sheaves and schemes local over a base scheme, like Grothendieck's generic freeness, translate to statements of an internal language in the Zariski topoi of sheaves and schemes over a base scheme where they become statements on sets, rings and modules and are therefore easier to prove. The proofs somehow make exact hand-waving arguments that properties hold respectively construction work on affine schemes and are natural enough to glue.

I find two points particularly interesting:

• The internal language is intuitionistic/constructive, so proofs about sets, rings and modules cannot use the Law of Excluded Middles or the Axiom of Choice. There is a very mathematical reason why this must be the case: The Axiom of Choice is equivalent to the freeness of every vector space, and this translates to the statement that every sheaf of modules on a reduced scheme is locally free! So this is an example where constructive logic is forced on us by facts of a classical theory, but where at the same time we gain significant simplifications of proofs. Such features contradict common assumptions of classically working mathematicians (like me) on constructive logic.

• Second, the translation process relies on a metatheorem: If the translation of the statement A to the internal language implies the translation of the statement B inside the internal language, then the original statement A implies the original statement B. Can such a metatheorem be (effectively) implemented in a proof assistant like LEAN?

[Johan Commelin]

@Thomas Eckl I think such a metatheorem can be implemented as a tactic. In principle. But what I understood from the experts is that it will be quite challenging to do this in a way that is actually usable.

[Johan Commelin]

But I know that @Alex J. Best was thinking about this recently. Such a tactic is certainly on my wishlist!

[Alex J. Best]

Yes, I've been thinking a quite a bit about this recently, but only thinking so far! Its a fascinating idea, and Ingo's thesis especially makes it seem like it might be actually useful, which is what I'd really hope for out of such meta work. I also liked some of the examples in https://math.jhu.edu/~eriehl/ct/DJM-LectureNotes.pdf . I'm very interesed in working out what an automated internalization of a mathlib statement and could look like, would it be unrecognizably general and require further post processing? And/or rewriting into external properties to obtain a "useful" result?

[Thomas Eckl]

So, how should such a tactic work? Take the statement on sheaves/schemes, translate it to the internal language of the relevant topos, ask the user for a proof of the translated statement, check that it does only use constructive arguments (probably using another tactic), translate this proof back to a classical proof on sheaves or schemes? That would mean that the Lean kernel only sees the classical arguments, and the metatheorem is never scrutinized by a proof checker - maybe not only a little bit unsatisfactory when producing such a complex tool in the context of a proof checking.

[David Wärn]

I imagine you would first define some sort of basic language for the type of statements you are interested in (together with rules for proofs and/or constructions in this language). Then you specify a way to interpret this language in, say, sheaves on X (so for example a formula in the language might get interpreted as an open set of X, and a proof in your language interprets as a proof that this open set is all of X). All of this you can do formally in Lean with no metaprogramming (but maybe you'd want to use some tactics to post-process the interpretations of formulas). A third step would be a sort of reflection tactic which takes an ordinary Lean proof and gives you a corresponding proof in your language. This part might feel unsatisfactory, but you can't get around it. There's no way to internalize in Lean the idea that every (constructive) Lean proof can be reflected into your language, so the tactic has to actually inspect each proof it is fed.

[Kevin Buzzard]

@Joseph Hua is this tactic discussed above something you would need for your Ax-Grothendieck proof?

[David Wärn]

The story for Ax-Grothendieck should be similar but simpler since you'd only need to reflect / reify formulas (not proofs). So you would show that Ax-Grothendieck holds for each $\overline{\mathbb F_p}$, prove that if some first-order sentence holds at almost every $\overline{\mathbb F_p}$ then it holds for $\mathbb C$, and then deduce that Ax-Grothendieck holds for $\mathbb C$ since it is a first-order sentence. This last step is the one of interest here; it's where you need to relate ordinary Lean formulas with formulas in the formal language of first-order logic. So this story is simpler since it doesn't matter how you prove the theorem for $\overline{\mathbb F_p}$ (in particular you don't have to work in FOL!).

[Kevin Buzzard]

Oh nice. I'm supervising Joseph basically so he can teach me by example what such a proof looks like in Lean. Did I recently read that you can just "run the outer proof internally" or something, using the Nullstellensatz (which we have), to get a model-theory-free proof of A-G?

[David Wärn]

I wonder if we can do this simple special case of internalising proofs in a sheaf topos: write a tactic which given an ordinary Lean proof like example {p : Prop} : ¬¬(p ∨ ¬p) := λ a, a (or.inr (λ b, a (or.inl b))), outputs a proof that for a Heyting algebra H and p : H, ¬¬(p ∨ ¬p) = ⊤.

[David Wärn]

Did I recently read that you can just "run the outer proof internally" or something, using the Nullstellensatz (which we have), to get a model-theory-free proof of A-G?

I don't know but it sounds plausible, there's surely many ways to prove A-G

[Antoine Chambert-Loir]

David Wärn said:

Did I recently read that you can just "run the outer proof internally" or something, using the Nullstellensatz (which we have), to get a model-theory-free proof of A-G?

I don't know but it sounds plausible, there's surely many ways to prove A-G

That's definitely possible and has been done in many ways, many times. See that paper of Serre, How to use finite fields for problems concerning infinite fields, for references and a sketch of a proof, or Wikipedia, Ax-Grothendieck theorem.

On the other hand, the model theory proof, the Nullstellensatz proof, and Grothendieck's proof by spreading-out basically rely on the same arguments.

[Alex J. Best]

Thomas Eckl said:

So, how should such a tactic work? Take the statement on sheaves/schemes, translate it to the internal language of the relevant topos, ask the user for a proof of the translated statement, check that it does only use constructive arguments (probably using another tactic), translate this proof back to a classical proof on sheaves or schemes? That would mean that the Lean kernel only sees the classical arguments, and the metatheorem is never scrutinized by a proof checker - maybe not only a little bit unsatisfactory when producing such a complex tool in the context of a proof checking.

Personally I'm more interested in "getting theorems for free" and taking existing proofs and translating them into an arbitrary topos, and then massaging the statements into a nice form. So, rather than prompting the user for proofs, just rely on the user to prove in the logic of lean the theorem they want translated.
The mathematics behind why this works (e.g. soundness theorems) is of course very interesting too, but seeing as you can't verify this for such a meta-tool I'm not too worried as long as it works in practice, my main goal is to reduce repetition and make formalization efforts faster and more efficient.