Zulip Chat Archive

Stream: maths

Topic: Ax-Grothendieck


Joseph Hua (Jul 05 2021 at 18:44):

I am starting a project in model theory working towards a proof of Ax-Grothendieck in lean. So far I have defined languages, structures, morphisms, terms, and interpretation of terms in structures. I have my current work uploaded here https://github.com/Jlh18/ModelTheoryInLean/tree/branch/src

Some of the things I will be needing/doing in this project are

  • Compactness theorem, Vaught completeness test,
  • algebraic closure
  • Transcendence degree
  • A load of cardinality lemmas (some specific to rings)
  • A good way of moving between models of the theory of rings and rings themselves
  • transcendence degree + cardinality determine ACF_p up to isomorphism
  • Ax-Grothendieck for locally finite fields (no model theory here)

Especially with regards to algebraic closure, transcendence degree and cardinality I would be interested in what is already available. If you have any suggestions please let me know.

FYI here is how I defined terms and interpretation of terms:

  def Demult {A : Type u} [decidable_eq A] : list A  list A
  | []       := []
  | (a :: l) := if a  l then Demult l else a :: Demult l


  /- For each term we keep track of the (index of)-/
  /- variables appearing in it as a list in ℕ without repetitions (Demult applied to the list)-/
  /- Term.Var only has itself as the variable-/
  /- Term.Comp combines all the variables appearing in the terms used in the composition-/
  def VarList : Term L  list 
  | (Var x) := [x]
  | (Comp n f t_) := Demult (list.join (@Fin.List (list ) n (λ x, VarList (t_ x))))


  /- We interpret each term with variables [x₁,⋯,xₙ] as a map Mⁿ → M-/
  def TermMap (M : Type u) [L.Structure M] :
    Π (t : L.Term), Prod (list.length (Term.VarList t)) M  M
  | (Var x)         α := α ()
  | (Comp n f t_)   α :=
    FuncMap f (
      λ i, TermMap (t_ i) (Proj (t_ i).VarList (Comp n f t_).VarList (TermVarSubCompVar _ _ _) α)
      )

Adam Topaz (Jul 05 2021 at 18:52):

@Joseph Hua Sounds like a great project! One thing to note: we recently got first-order structures in mathlib thanks to the work of @Aaron Anderson based on Flypitch, see e.g. docs#first_order.language

Joseph Hua (Jul 05 2021 at 18:54):

Yes i have had a look at that and decided to make some adjustments - but it should be pretty much the same on overlaps

Aaron Anderson (Jul 05 2021 at 19:04):

I would definitely recommend staying at least somewhat close to Flypitch, because they have proven some big results like compactness, and to be honest just finding a practical inductive definition of formulas is tricky enough

Aaron Anderson (Jul 05 2021 at 19:05):

I have a long-term goal of working on model theory in Lean, but will probably not be active much this summer. I would still be happy to review any model-theory related PRs, or take a look at pre-PR work.

Aaron Anderson (Jul 05 2021 at 19:06):

(deleted)

Joseph Hua (Jul 05 2021 at 19:10):

Aaron Anderson said:

I would definitely recommend staying at least somewhat close to Flypitch, because they have proven some big results like compactness, and to be honest just finding a practical inductive definition of formulas is tricky enough

Oh amazing - I only saw basic docs#first_order.language so i couldnt see any results outside the basics. I have now found the rest of it https://github.com/flypitch/flypitch/releases/tag/2.0

Joseph Hua (Jul 05 2021 at 19:12):

Aaron Anderson said:

I have a long-term goal of working on model theory in Lean, but will probably not be active much this summer. I would still be happy to review any model-theory related PRs, or take a look at pre-PR work.

whats a PR? Im doing this as part of my 4th year project, so starting now and ending summer next year

Johan Commelin (Jul 05 2021 at 19:13):

PR = pull request. So that's the process of proposing a new addition to mathlib, getting reviews, and finally getting the stuff merged into mathlib.

Joseph Hua (Jul 07 2021 at 18:01):

I just understood the definition of formulas, I was super confused as to how to specify which term is bounded by ∀'. Am I understanding it correctly to be: it bounds the variable &0 and then shifts the index of every remaining free variable down by 1?

Joseph Hua (Aug 05 2021 at 15:07):

Why can i pattern match on t : bounded_preterm L n 0 but not do induction t in tactic mode?

Chris Hughes (Jan 27 2022 at 19:14):

So @Joseph Hua gave me an update today and says he has a proof of Ax-Grothendieck with a lot of sorries. The main sorry is a proof of the Łoś–Vaught test which is a model theoretic theorem, but I suggested that we could help him with the non-model theory parts.

There are two main things to prove

The first is to prove Ax-Grothendieck for the algebraic closure of Fp\mathbb{F}_p. The proof of this is that if KK is the algebraic closure of FpF_p and ff is an injective polynomial map and yKny \in K^n then we can find an xx such that f(x)=yf(x) = y by restricting to the subfield LL generated by the coefficients of ff and the coordinates of yy. LL is finitely generated and therefore finite, so ff is surjective when restricted to LL because an injective map from a finite set to itself is surjective.

The other thing to prove is that any algebraically closed field of characteristic with the same cardinality as C\mathbb{C} is isomorphic to C\mathbb{C}. I've made lots of progress on this in #9370 and #11703 . I think finishing this off will be easy once the sorries in #11703 are filled in which are that if R and S are integral domains and algebra R S with an injective algebra_map and S is algebraic over R then fraction_ring S is algebraic over fraction_ring R and algebra_map R (fraction_ring S) is injective. I'm sure this is a special case of something more general.

I think it would be super cool to have a proof of Ax-Grothendieck, it's a bit different from the rest of the stuff we have and really cool to see model theory being used to prove something outside of model theory.

Kevin Buzzard (Jan 27 2022 at 19:18):

The reason that I leapt upon Joseph's proposal for Ax-Grothendieck in Lean for his MSc project was precisely that I also thought it would be really interesting to see if model theory could prove something outside of model theory.

Kevin Buzzard (Jan 27 2022 at 19:19):

Let me make it clear that there will be no issues with people collaborating with Joseph even though the work is part of his degree. If some part of the argument is done by someone else then he can just state this in the write-up.

Eric Rodriguez (Jan 27 2022 at 19:21):

I think we already have algebra_map R (fraction_ring S) is injective; we use similar things in flt-regular

Eric Rodriguez (Jan 27 2022 at 20:01):

and maybe the algebraic result is docs#is_fraction_ring.comap_is_algebraic_iff?

Joseph Hua (Jan 27 2022 at 20:21):

Thanks Chris! To summarize:

  • The first sorry that remains is that the theories of algebraically closed fields of characteristic 0 / p are complete. To prove this I need
  1. Vaught's test (which I am working on)
  2. That any two algebraically closed fields of the same characteristic and cardinality are isomorphic (which Chris is close to fininishing)
  • The second sorry is Ax-Groth for the algebraic closure of F_p

My repo is here https://github.com/Jlh18/ModelTheoryInLean8

Damiano Testa (Jan 27 2022 at 20:31):

For item 2 you, don't you need to exclude countable models?

Damiano Testa (Jan 27 2022 at 20:33):

Just to be more explicit, Q\mathbb{Q} and Q(t)\mathbb{Q}(t) do not have isomorphic algebraic closure.

Adam Topaz (Jan 27 2022 at 20:33):

(it's okay with uncountable cardinality) I suspect Joseph meant to say cardinality of a transcendence base (over the prime subfield)?

Chris Hughes (Jan 27 2022 at 20:56):

Eric Rodriguez said:

and maybe the algebraic result is docs#is_fraction_ring.comap_is_algebraic_iff?

I don't think it is this. That would prove algebraic (fraction_ring R) (fraction_ring S) is equivalent to algebraic R (fraction_ring S) but we don't know algebraic R (fraction_ring S). There's some content to this, you have to prove that if x is a root of P, then x^-1 is a root of P with the coefficients in reverse order.

Johan Commelin (Jan 28 2022 at 03:25):

I think Damiano build an API for "P with coefficients in reverse order". So the content you are looking for might already be in mathlib.

Johan Commelin (Jan 28 2022 at 03:29):

Hmm, I can't find that exact result. But there is docs#polynomial.reverse and docs#polynomial.mirror which both might be relevant.

Johan Commelin (Jan 28 2022 at 03:30):

For example, we know reverse (f * g) = reverse f * reverse g, and from there it shouldn't be too hard to get your result about x⁻¹.

Yakov Pechersky (Jan 28 2022 at 03:58):

I think I used these algebra instances recently for ratfunc on top of polynomial, just not in the generality of localizations

Yakov Pechersky (Jan 28 2022 at 04:02):

And built the lift of alg_hom that you need to construct your [algebra (fraction_ring R) (fraction_ring S)], just generalize this https://github.com/leanprover-community/mathlib/pull/11276/files#diff-fd31dd5424b8516373b9afed90f52999a75af83f88d655e59e310598a784e137R625

Yakov Pechersky (Jan 28 2022 at 04:05):

Unless I misunderstood something and what I said is irrelevant, then ignore it

Damiano Testa (Jan 28 2022 at 05:25):

I used reverse to transport some results about leading_coeffs to similar results about trailing_coeffs. What you want about roots of reversed polynomials may be close, but I am not sure.

To go into slightly technical issues, mirror reflects the interval [0, nat_degree + trailing_nat_degree]. Thus, reverse and mirror only differ by multiplication by a power of x, and this only when 0 is a root of your polynomial. Nevertheless, mirror might avoid having to worry about the case when 0 really is a root of your polynomial, in which case it will not be a zero of reverse (if the polynomial is non-zero).

Chris Hughes (Jan 29 2022 at 22:14):

Classification of algebraically closed fields part is now done #9370

Kevin Buzzard (Jan 29 2022 at 23:59):

Thanks a lot Chris!

Joseph Hua (Jan 31 2022 at 09:50):

Oh amazing! Thanks so much

Aaron Anderson (Jan 31 2022 at 17:29):

I should also note that I've started to get some more model theory into actual mathlib. It does look a bit different than flypitch, although it follows most of the same principles.

Aaron Anderson (Jan 31 2022 at 17:31):

This probably shouldn't change this project at all, at least not yet. Once I have the compactness theorem, I think it'd be possible to adapt the project to modern mathlib, but I don't know if it'd be worth it.

Joseph Hua (Jan 31 2022 at 21:52):

Aaron Anderson said:

I should also note that I've started to get some more model theory into actual mathlib. It does look a bit different than flypitch, although it follows most of the same principles.

I have seen. In order to work with morphisms of structures (which wasn't mentioned in the flypitch project as far as I could see) I ported some of your work to my copy of the flypitch project. Of course it would be nice to go the other way round and make the flypitch work more suitable for mathlib, but that's a much larger project than I have time for.

Joseph Hua (Apr 07 2022 at 15:10):

It's done! https://github.com/Jlh18/ModelTheoryInLean8

Kevin Buzzard (Apr 07 2022 at 15:23):

It's here: https://github.com/Jlh18/ModelTheoryInLean8/blob/94823f02a543e8c7ef230925ecc497926c905ea3/src/Rings/AxGroth.lean#L1577 . This is nice because it uses model theory to prove a result which doesn't mention model theory.

Ruben Van de Velde (Apr 07 2022 at 15:25):

Lean 8? Way to be ahead of the rest of us on lean 3 or 4!

Eric Rodriguez (Apr 07 2022 at 15:49):

those seem like custom types - is there glue to the standard docs#polynomial etc?

Eric Rodriguez (Apr 07 2022 at 15:51):

oh, I see, they're not, poly_map really is required


Last updated: Dec 20 2023 at 11:08 UTC