Copying df-plfl to my mathbox

31 views

Skip to first unread message

Meta Kunt

unread,

Nov 30, 2024, 9:59:30 AM11/30/24

to mm goog

Greetings,

I'd like to develop an API for finite fields and its algebraic closure. I've looked at how lean implements it (Non-constructive using Krull and Algebra isomorphisms), and I'd like to develop theory such that I can progress with the AKS formalisation.

It appears I need the following (at the minimum): A ring homomorphism from (Z/n)[X] --> F_p[X]/h(x) such that F_p[X]/h(X) contains a primitive r-th root of unity. See https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/RootsOfUnity/AlgebraicallyClosed.html#IsAlgClosed.hasEnoughRootsOfUnity which uses the algebraic closure to prove that if r,p are coprime that the algebraic closure of F_p has r-th primitive roots of unity.

Of course I think we could also take the splitting field of (X^r-1) to show that it has at most r roots of unity and by the embedding of (X^r-1) into a suitable (X^(p^a)-1) to show that all roots are different. And then by a combinatorial argument to show that not all roots of unity aren't primitive roots of unity. I think the necessary step is I'd like to have a hypothesis
|- ( ph -> M e. ( PrimitiveRoot ` F ) )
which I can eventually eliminate by proving
|- ( ph -> E. m e. ( PrimitiveRoot ` F ) )
However I'd need to show that a primitive root exist for a given field, here I'm unsure what field to take and what will formalise easier.

Also we need to have the concept of a perfect ring. I.e. the Frobenius is an automorphism.

Proving that the Frobenius is injective is found here, it works for any nilpotent ring (i.e any nilpotent element is 0). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/CharP/Reduced.html#frobenius_inj
Proving that the frobenius is surjective can be done two ways, either we take the splitting field approach, then we can argue that the frobenius is an endomorphism of finite fields, i.e. also bijective, or by a different argument that the Frobenius of its algebraic closure is surjective. Indeed x^p is a polynomial and x^p=c <-> x^p-c=0, by the algebraic closure property has a root. Proof here https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/IsAlgClosed/Basic.html#IsAlgClosed.perfectField

Other that that there is also the possibility of just defining the properties without actually constructing anything. We could use something like a collection of all algebraic closures of a field and prove just by those properties without showing that they exist. Then all theorems would contain hypotheses such as ( ph -> F e. ( AlgebraicClosure ` ( Z_p ) ) ) and we would develop an API just based on that

This is how lean does it https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/IsAlgClosed/Basic.html#IsAlgClosure is just the definition of the algebraic closure. An existence proof that allows to discharge above hypothesis is found https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.html#AlgebraicClosure.instIsAlgClosure

At the end once someone actually constructs ( GF_oo ` p ) and proves that ( GF_oo ` p ) e. AlgebraicClosure ( Z_p ) we could discharge those hypotheses.

Anyways I'd be happy if I could get some helpful points to develop a basic api for https://us.metamath.org/mpeuni/df-plfl.html

My goal is the following, show that (X^2+X+1) is irreducible over F_2[X], show that the polyFld construction is a field for irreducible monic polynomials,
show that [X] x. [X+1] = [1] therefore that X and X+1 are inverse to each other and show explicitly that {0,1,X,X+1} are the only possibilities of elements of that field, therefore it contains 4 elements.
( # ` F ) = 4.

What theorems should I formalise before starting with the next one, which is this auxiliary splitting field construction which is already beyond my comprehension https://us.metamath.org/mpeuni/df-sfl1.html

Also Mario, I'd be happy if you could explain the definitions and API's of the following definitions, as I sadly don't understand them. I'm not sure what theorems you have planned and what will be necessary/enough for me to prove.
https://us.metamath.org/mpeuni/df-homlimb.html
https://us.metamath.org/mpeuni/df-homlim.html
https://us.metamath.org/mpeuni/df-sfl1.html
https://us.metamath.org/mpeuni/df-sfl.html
https://us.metamath.org/mpeuni/df-psl.html

and then if needed for
https://us.metamath.org/mpeuni/df-gf.html
https://us.metamath.org/mpeuni/df-gfoo.html

I assume at the very minimum we need that they are all fields, that homlim inherits the structures (maybe an induction proof, but it seems very technical) and that gfoo is an algebraic closure. I'm not sure how easy it will be to calculate explicitly in even a small field like GF 2 2, as this would already be a splitting polynomial of ( X^4-X)=X*(X+1)*(X^2+X+1), here I have trouble understanding how sfl works and how I can make use of it in theorems.

I'd be happy for any help as I'm afraid I'd otherwise have not much of a progress.

Metakunt