Ax-Grothendieck

Stream: maths

[Joseph Hua]

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]

@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]

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]

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]

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]

(deleted)

[Joseph Hua]

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]

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]

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]

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]

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

[Chris Hughes]

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 $\mathbb{F}_p$. The proof of this is that if $K$ is the algebraic closure of $F_p$ and $f$ is an injective polynomial map and $y \in K^n$ then we can find an $x$ such that $f(x) = y$ by restricting to the subfield $L$ generated by the coefficients of $f$ and the coordinates of $y$. $L$ is finitely generated and therefore finite, so $f$ is surjective when restricted to $L$ 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 $\mathbb{C}$ is isomorphic to $\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]

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]

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]

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

[Eric Rodriguez]

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

[Joseph Hua]

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]

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

[Damiano Testa]

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

[Adam Topaz]

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

[Chris Hughes]

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]

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]

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]

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]

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

[Yakov Pechersky]

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]

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

[Damiano Testa]

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]

Classification of algebraically closed fields part is now done #9370

[Kevin Buzzard]

Thanks a lot Chris!

[Joseph Hua]

Oh amazing! Thanks so much

[Aaron Anderson]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Eric Rodriguez]

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

[Eric Rodriguez]

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