Model Theory - fields are field structures and vice versa

Stream: maths

[Chris Hughes]

I've started (slowly) trying to get the Ax-Grothendieck theorem into mathlib on the axgroth branch. I think the Model Theory library is currently well set up for doing general model theory, but without applying it to concrete examples yet.

One of the things I have to do for this is prove that a model for the theory of Algebraically Closed Fields of char p is an algebraically closed field of char p and vice versa. This is clearly going to be kind of messy, and the decision I made was to make the fact that fields are models of field an instance, and then any theorem that required both model theory and field theory should be stated over fields. This seems to copy what is already there for graphs. The other direction is there, but not as an instance, and is to be used sparingly. However, I will still sometimes need the other direction, and you end up needing to know that going from Language.field.Structure + Theory.field.Model => Field => Language.field.Structure + Theory.field.Model is the identity. Ideally this should be by definition. The lack of commutavity is basically because for f : (fin 2 -> M) - M, f = fun x => f ![x 0, x1] is not by definition.

One solution is to put up with the pain, and hope that these issues will only come up a couple of times, and that the important theorems about AlgClosedFields, namely completeness of the theory of alg closed fields of a particular characteristic and also the lefschetz principle will be usable without these issues coming up in usage.

Another solution is to redefine the notion of a Structure for a language to either return an ArityNFunction where an ArityNFunction is defined as

def ArityNFunction : ℕ → Type _
  | 0 => M
  | n+1 => M → ArityNFunction n

The final solution is to use some sort of iterated binary product instead of Fin n -> M and then for concrete n, the equality mentioned above that failed will be by definition. I think this is my prefered solution, because it's the least radical change from the current implementation. Do @Joseph Hua, @Floris van Doorn or @Jesse Michael Han or @Aaron Anderson have any comments on this?

[Notification Bot]

This topic was moved here from #mathlib4 > Model Theory - fields are field structures and vice versa by Chris Hughes.

[Chris Hughes]

I guess the other option is to state all theorems with both [Theory.field.Structure K] and [Field K] as well as a compatibility assumption between the two structures.

[Aaron Anderson]

I've always struggled with good instance design, and this doesn't change the mathematical meaning, so I'll ultimately defer to any changes on that design, if you can make the existing code work with it.

[Aaron Anderson]

Also, I think that ultimately, it would be good to be able to define things like, say, definability, on a broad array of such types. Explicitly, I think that it should be possible to define definability of functions M -> M -> M, as well as functions M x M -> M and (fin 2 -> M) -> M. @Reid Barton and @Johan Commelin probably have some thoughts on how to design this well.

[Aaron Anderson]

Also also, I've had some conversations recently with @Ramon Fernández Mir about improving the model theory library, so I'll add a tag.

[Chris Hughes]

Chris Hughes said:

I guess the other option is to state all theorems with both [Theory.field.Structure K] and [Field K] as well as a compatibility assumption between the two structures.

This is what I did in the end. I defined a CompatibleField type class which extends Field and Language.field.Structure along with compatibility hypotheses. It means I need to use let a fair amount to add instances by hand, but it seems to work okay. It's worth noting that the diagram Field => FieldStructure => Field won't ever commute by definition unless things like nsmul are added to the language of fields, which would be a controversial addition, and would mean that the theory of fields would require infinitely many axioms, which is a mathematically significant change.

[Kevin Buzzard]

Could you make a variant of FieldStructure which contained the nsmul fields, write down the bijection between field and this modified structure, and then just write down the dodgier bijection between FieldStructure and the modified field structure separately?

[Chris Hughes]

Yes. But I don't see why I would do that. ACtually there's no way to make FieldStructure => Field => FieldStructure commute ever I've just realized, because a field structure is a map ∀ n, FieldFunc n → (Fin n → K), where FieldFunc n is

inductive FieldFunc : ℕ → Type
  | add : FieldFunc 2
  | mul : FieldFunc 2
  | neg : FieldFunc 1
  | inv : FieldFunc 1
  | zero : FieldFunc 0
  | one : FieldFunc 0

But to commute by definition would require two functions ∀ n, FieldFunc n → (Fin n → K) to be defeq iff they are defeq on all constructors and this is not the case. So there's not much hope of trying to make these things commute.

[Chris Hughes]

Field => FieldStructure => Field could commute with a lot of effort, but I think this is more trouble than it's worth. The occasional let is not that bad, especially since it's not like people will be applying the model theory of fields all the time. There are maybe just a few theorems that can be proved that way and people won't be that annoyed by the letI.