[EricSchmidt-119]

In this PR, we define finite fields! Well, sort of. What we actually do is use the Ackermann bijection to define a well ordering of HFStructs. Then we define the finite field of order q as the least HFStruct that is a field of order q. The catch is that to do anything useful with the definition, you first have to prove the existence of such a field.

Besides showing the existence of finite fields, it is also necessary to show that we can get one whose components are all hereditarily finite, analogously to theorem "fingrphf" proved in this PR. I did want to prove also the analogous result for monoids and use that to prove it for rings. But I discovered that we don't even have a definition of isomorphism of monoids. So I have contented myself with "fingrphf", which is enough to illustrate how these results are proved.

Changes:

imasgim: Moved from SO's mathbox to main
rnmposs: Moved from TA's mathbox to main

New statements in my mathbox:

relpropg
mpoexwd
grpxfr [removed]
imasgimw
grpgimcanon
cackbij
df-ackbij
ackbij3
grphfstruct [removed]
grpcanonhfstruct
fingrphf
clthfstruct
df-lthfstruct
hfstructwe
cfinfld
df-finfld

[tirix]

I have not yet reviewed the submission but I find the idea excellent!

Another way to define finite fields would have been the one mentioned in the "explicit construction" Wikipedia page of finite fields: by using quotient rings of polynomial rings by the Conway polynomials.

Is there any particular reason to use one rather than the other?

[EricSchmidt-119]

There are two steps in the definition of the Conway polynomials:

1. The definition of the compatibility condition.
2. Choosing a polynomial that satisfies it. There is, apparently, no natural choice, so the Conway polynomial is defined to be least according to a lexicographical ordering.

The purpose of the compatibility condition is unclear to me, but, based on the Wikipedia article, the motivation for defining Conway polynomials is to use them in computer algebra systems. Using the compatibility condition makes the definition of Conway polynomials recursive. I don't think we need this extra complexity. The remaining idea from this definition is picking an irreducible polynomial using the lexicographical order. This is one viable way of choosing a particular finite field.

So far as I am aware, no matter what method we use, we will have to make an essentially arbitrary choice, made definite using some ordering.

The minimal polynomial definition has the advantage of being more down-to-earth, not requiring the machinery needed to define HF, HFStructs, and a well ordering of HFStructs. It does require producing an ad hoc ordering.

The idea behind HFStructs is to set up the apparatus once and for all and use it whenever a problem of this type arises. One potential downside is that the development currently depends on ax-rep. It should be possible to eliminate this, but it might be a significant effort.

Either way, we shouldn't depend on the particular construction, just the fact that it produces a field of order q.

[tirix]

Thanks for taking the time to answer in length!

Yes, the choice is essentially arbitrary, so any construction is as good as another one.

The added condition for compatibility in the definition of Conway's polynomials seems to be to create a hierarchy of polynomials, which induces subfields : if $p|n$, then it guarantees by construction that $F_p$ is a subfield embedded in $F_n$. It will be the case for any other construction, but it might only be "modulo some isomorphism", and be harder to prove - thought this is just my intuition.

@digama0 explicitly defined a lexicographical order for polynomials so I was under the impression that he might be going for Conway's definition - but he stopped before, so this can only be a supposition. Actually its first use is for choosing a minimal irreducible polynomial factor for splitting fields.

As a note, there is already a definition for some finite fields in set.mm, namely df-gf for Galois fields. Here also, unfortunately this is only a definition, which has not been expanded yet with any use.

I will try to take more time to review this PR in detail, sorry I have not until now.

[EricSchmidt-119]

df-gf actually covers all finite fields up to isomorphism. It defines the finite field of order q = p^n as the splitting field of x^q - x over the field with p elements. In general, splitting fields are only defined up to isomorphism. Here, obtaining a specific splitting field uses a total ordering of the base field.

So we now have three different ways of proceeding.

[tirix]

There is a similar definition df-imas, and theorem imasgrpf1 which might have been applicable here, but would make use of ax-rep though.

[tirix]

I'd like to hear your thoughts about using "s (df-imas) for proving the existence of an isomorphic group, ring, field with hereditarily finite components, see for example imasring.

Otherwise nothing blocking from me!

[langgerard]

Would the base sets of the selected magma, semi-group; mooid, group, ring, field be identical, so that each would be a natural extension of the others ?

[EricSchmidt-119]

I'd like to hear your thoughts about using "s (df-imas) for proving the existence of an isomorphic group, ring, field with hereditarily finite components, see for example imasring.

Otherwise nothing blocking from me!

Ah, I was not previously aware of df-imas. I haven't studied it in detail, but I believe it would be usable for this. The requirement for ax-rep is undesirable, but it probably could be eliminated by added a hypothesis B e. _V throughout the development. This would be a natural thing to do since (I imagine) in almost all applications we would know directly that the codomain of F is a set.

[EricSchmidt-119]

Would the base sets of the selected magma, semi-group; mooid, group, ring, field be identical, so that each would be a natural extension of the others ?

Yes, the base set would be the same.

[EricSchmidt-119]

Taking a look at this some more:

df-imas is used only in imasval, which depends on ax-rep. This dependency can be removed by adding the hypothesis |- B e. _V. Removing it in other theorems will require propagating this hypothesis.

The theorem grphfstruct could not be generalized to one that concludes ( F "s R ) e. HFStruct for arbitrary structures. This is because the distance function takes values in RR. So the best we could do is restrict it to components it does work for, like ( ( F "s R ) |` { ( Base ` idx ) , ( +g ` idx ) } ).

[EricSchmidt-119]

It took a while, but finally I have updated this PR. The theorems grpxfr and grphfstruct have been removed. The theorem imasgim, the analogue of grpxfr for the structure image operation, has been moved to main. There are two new theorems: grpgimcanon and grpcanonhfstruct, the latter being the replacement for grphfstruct.

This represents all the changes I plan to make in this PR.