Zulip Chat Archive

Stream: maths

Topic: model completeness of algebraically closed fields


view this post on Zulip Damiano Testa (Aug 17 2020 at 11:55):

Is it possible to (a) prove that the first order theory of algebraically closed fields is complete (via quantifier elimination or otherwise) and (b) use such a statement/proof to actually deduce things about the complex numbers (or arbitrary algebraically closed fields)?

For instance, I am thinking that Hilbert's Nullstellensatz can be proved quite quickly using quantifier elimination.

view this post on Zulip Johan Commelin (Aug 17 2020 at 11:57):

Sure, but I don't think that (a) is very easy. It will require quite a bit of prior work.

view this post on Zulip Adam Topaz (Aug 17 2020 at 11:59):

I do think it would be nice to have some more model theory in mathlib, in general

view this post on Zulip Damiano Testa (Aug 17 2020 at 12:00):

What about focusing on quantifier elimination? For algebraically closed fields, quantifier elimination and elimination theory are very close and formalizing this might be more at hand?

view this post on Zulip Damiano Testa (Aug 17 2020 at 12:01):

For instance, is it in theory possible in Lean to prove quantifier elimination by some form of induction on propositions, to show that every proposition reduces to true or false constructively? Is there an "induction on proposition"?

view this post on Zulip Damiano Testa (Aug 17 2020 at 12:02):

Something along the lines of: a proposition either begins with a \exist or a \forall. in the first case, do something, in the second case, negate, push negations through and repeat

view this post on Zulip Adam Topaz (Aug 17 2020 at 12:03):

I think unfortunately one has model first order sentences as some kind of inductive type. The closest thing I know of is in the flypitch project

view this post on Zulip Damiano Testa (Aug 17 2020 at 12:04):

Would working with the first order theory of ACF, possibly make this any easier?

view this post on Zulip Damiano Testa (Aug 17 2020 at 12:05):

Even just proving something about nested sequences of \exists and \foralls might be a good testing ground

view this post on Zulip Adam Topaz (Aug 17 2020 at 12:06):

I think with the current stuff from mathlib it would be easier to try to prove the AG formulation a la Chevalley's theorem.

view this post on Zulip Johan Commelin (Aug 17 2020 at 12:07):

@Damiano Testa Sure this can be done. Flypitch probably did a lot of similar stuff. But right now, there is no definition in mathlib of what it means to be a first order formula in the language of "whatever"

view this post on Zulip Damiano Testa (Aug 17 2020 at 12:07):

Adam Topaz said:

I think with the current stuff from mathlib it would be easier to try to prove the AG formulation a la Chevalley's theorem.

I was actually trying to get a proof of Chevalley's theorem and this is how I got to this question...

view this post on Zulip Damiano Testa (Aug 17 2020 at 12:08):

Johan Commelin said:

Damiano Testa Sure this can be done. Flypitch probably did a lot of similar stuff. But right now, there is no definition in mathlib of what it means to be a first order formula in the language of "whatever"

Ok, I do not know what Flypitch is, but I get the idea that this is not a viable approach, at least for the moment!

view this post on Zulip Adam Topaz (Aug 17 2020 at 12:11):

I think Chevalley's theorem is approachable in lean without going through general stuff about quantifier elimination

view this post on Zulip Adam Topaz (Aug 17 2020 at 12:12):

The first step would be to formalize constructive sets in the Zariski topology

view this post on Zulip Adam Topaz (Aug 17 2020 at 12:12):

This would presumably be done as some inductive relation building on top of the Zariski topology.

view this post on Zulip Adam Topaz (Aug 17 2020 at 12:13):

And inducting on this definition is essentially equivalent to induction on the quantifiers in a given first order formula

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 12:15):

so you could make constructible sets as an inductive Prop, like the way Alex Best did topology generated by a collection of sets in LFTCM

view this post on Zulip Adam Topaz (Aug 17 2020 at 12:16):

Yeah that's approximately what I was thinking

view this post on Zulip Johan Commelin (Aug 17 2020 at 12:16):

@Damiano Testa https://github.com/flypitch/ is a formal verification of independence of the continuum hypothesis. Arguably the biggest milestone that Lean can brag about (-;

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 12:16):

oh in fact he even did constructible sets:
https://github.com/leanprover-community/lftcm2020/blob/1948bfaf58e3b340b39cd9b8366aa4f13e5ffa7d/src/exercises_sources/wednesday/afternoon/topological_spaces.lean#L117-L122

view this post on Zulip Adam Topaz (Aug 17 2020 at 12:17):

We need the Zariski topology too

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 12:17):

that might be there

view this post on Zulip Adam Topaz (Aug 17 2020 at 12:17):

In the sense of "classical" ag

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 12:20):

Zariski top on prime spectrum is in algebraic_geometry.prime_spectrum. I guess we might be talking at cross purposes here. I was envisaging that Chevalley's theorem was some statement about finitely presented morphisms of schemes

view this post on Zulip Adam Topaz (Aug 17 2020 at 12:22):

Oh sure, but the original question was about quantifier elimination in algebraically closed fields, so for that it's just Chevalley's theorem for varieties over the alg. cl field in question

view this post on Zulip Damiano Testa (Aug 17 2020 at 12:23):

But is the Zariski part of the topology needed much more than just to say this: let R be a ring and c an element of R. The set of all prime ideals containing c is closed and "essentially equal to" Spec R/c, the complement is open and "essentially equal to" Spec R_c?

view this post on Zulip Damiano Testa (Aug 17 2020 at 12:23):

To go from here to the general case of finite presentation, indeed it is mostly playing around with quasi-compact opens, retrocompactness and complements of finitely generated ideals

view this post on Zulip Damiano Testa (Aug 17 2020 at 12:26):

(I am thinking of the proof of Chevalley's theorem in the stacks project:
https://stacks.math.columbia.edu/tag/00F5
)

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 12:27):

yeah that should be fun to do in Lean, it will probably teach you a lot

view this post on Zulip Damiano Testa (Aug 17 2020 at 12:28):

I am trying to do it, in fact! Ahahaha (But you probably already knew this! ;)

view this post on Zulip Damiano Testa (Aug 17 2020 at 12:28):

(Anyway, now I am the one who has to go! Bye!)

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 12:31):

oh this uses the EGA version of constructible, with retrocompact in, so the link to constructible I sent is no good

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 12:31):

right, I guess it has to use this version because there are no Noetherian hypotheses

view this post on Zulip Aaron Anderson (Aug 17 2020 at 16:52):

I’m starting to adapt some flypitch to conventions that seem to match the rest of mathlib a little better at a branch, mathlib:fol_project.

view this post on Zulip Aaron Anderson (Aug 17 2020 at 16:56):

I’m still not particularly close, but I have a definition of definable sets that doesn’t require formulas.

view this post on Zulip Aaron Anderson (Aug 17 2020 at 16:57):

One thing I noticed is that I couldn’t find a super-suitable definition of the Boolean algebra generated by a particular subset. Perhaps I just need to look again, but I think that’d be useful for defining constructible


Last updated: May 19 2021 at 02:10 UTC