Semialgebraic Sets

Stream: Is there code for X?

[Tomaz Mascarenhas]

Do we have anything on Semialgebraic sets?

[Kevin Buzzard]

Not even the definition, as far as I know.

[Kevin Buzzard]

Proving o-minimality would be a really cool project!

[Yaël Dillies]

It also is tangentially related to my research :smile:

[Tomaz Mascarenhas]

I see; is there any structure in mathlib that is constructed in a similar way? i.e. starting with a property (P(x) > 0 in this case) and then taking arbitrary conjunctions of these (forming basic semialgebraic sets) and then taking arbitrary disjunctions of these?

[Aaron Liu]

It seems to be only finite unions and intersections?

[Tomaz Mascarenhas]

Yes I think so

[Aaron Liu]

otherwise you could do anything as a union of singletons

[Aaron Liu]

Well docs#TopologicalSpace.generateFrom seems pretty similar

[Aaron Liu]

As well as the ones for filter and measure space and stuff

[Aaron Liu]

We also have docs#FreeRing, which is sums of products of elements

[Fabrizio Barroero]

I think @Johan Commelin once told me he had some project on this in lean 3. I can’t remember if it was about semi algebraic sets or o-minimality.

[Adam Topaz]

IMO the proper way to work with semialgebraic sets is to consider them as definable sets in the appropriate language w.r.t. appropriate kinds of first-order formulas.

[Adam Topaz]

(The theory of real closed fields has quantifier elimination)

[Tomaz Mascarenhas]

Adam Topaz said:

IMO the proper way to work with semialgebraic sets is to consider them as definable sets in the appropriate language w.r.t. appropriate kinds of first-order formulas.

You mean as defined here?

https://github.com/leanprover-community/mathlib4/blob/04c82c164d0b74dbfe3fcd0d7e174938d1112399/Mathlib/ModelTheory/Definability.lean

[Luigi Massacci]

You can look here for a purely geometric approach: https://github.com/rwbarton/lean-omin by @Reid Barton and @Johan Commelin

[Johan Commelin]

Just seeing this thread now. Thanks for posting that link Luigi!

@Niels Keukens @Lily <3 and @Joos Munneke are currently also working on a student project to formalize the basics of model-theoretic approach to o-minimality.