Algebraic closure definition and existence axiom. #4554

metakunt · 2025-01-11T02:44:02Z

Define the algebraic closure of as the class of all fields that satisfy the following three properties:

Any polynomial of L[X] with positive degree has a root.
There exists an injective ring homomorphism embedding K into L.
Any element of L is algebraic over L.

Also postulate the axiom that the algebraic closure exists. This is needed to eventually discharge the hypotheses of the form

|- ( ph -> L e. ( AlgClosure ` K ) )

The definition fails for unknown reasons to me. Maybe one of you can help me.

Definition in lean:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/IsAlgClosed/Basic.html#IsAlgClosure
and its existence
https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.html#AlgebraicClosure.instField

icecream17 · 2025-01-11T03:42:49Z

I think the third part is that any element of K is algebraic over L, based on https://en.wikipedia.org/wiki/Algebraic_closure --> https://en.wikipedia.org/wiki/Algebraic_extension

(elements of L being algebraic over L is trivial because for any number N, we have the polynomial N - x = 0)

metakunt · 2025-01-11T05:17:55Z

Yeah you are right. This definition currently is bollocks.
I need the canonical map mapping the polynomial in K[X] to the polynomial in L[X]
so the second condition should be

$$\forall l \in L \exists q \in K[X] \mathrm{~such~that~} q(l)=0 \mathrm{~in~}L$$

I need the map that maps the polynomial with coefficients in K to the map with coefficients in L. In lean, this map is called Polynomial.aeval, I don't know what the metamath analogue is.

icecream17 · 2025-01-11T06:14:28Z

Lean's aeval looks like it assigns a single variable a value (evaluates a single variable). This probably isn't what your comment was talking about though... ((It takes the variable and value, and returns a function taking a polynomial to another polynomial with the variable removed, ie a homomorphism))

For single variable polynomials, df-evl1 in metamath is enough

For multivariable polynomials, this could be done by using df-selv and df-evl: df-selv basically let's us assign only some of the variables instead of all of them upon evaluation (see below), so it's perfect... but df-selv is not developed, with only selvval and selvcl basically.

Missing theorem:

(select some variables, evaluate those variables, then evaluate the rest) = evaluate all variables

icecream17 · 2025-01-11T06:35:01Z

To map K[X] to L[X] (there isn't a preexisting definition for this):

polynomials are represented as functions
(variables -> exponents) -> K coefficients

so function composition

( k_p in K[X] |-> ( k_p o. (the K hom L) ) )

metakunt · 2025-01-11T07:02:46Z

Yeah, you are right, I meant https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Polynomial/Eval/Defs.html#Polynomial.map

Also I think you've meant that every element of L is algebraic over K. In any way I have reflected that in the definition.

The definition should now be correct, if I didn't miss anything.

avekens · 2025-01-11T09:04:58Z

To verify that the definition is correct (i.e., it defines what was intended to be defined), some basic theorems should be proven, especially for the three postulated properties, starting with the following two defining theorems:

 ( K e. Field -> ( AlgClosure ` K ) = { l e. Field |
      ( A. p e. ( Base ` ( Poly1 ` l ) ) ( ( deg1 ` p ) e. NN ->
      E. z e. ( Base ` l ) ( ( ( eval1 ` l ) ` p ) ` z ) = ( 0g ` l ) ) /\
      E. f e. ( K RingHom l ) A. x e. l E. q e. ( Base ` ( Poly1 ` K ) )
      ( ( q o. f ) =/= ( 0g ` ( Poly1 ` l ) ) /\
      ( ( ( eval1 ` l ) ` q ) ` ( f ` x ) ) = ( 0g ` l ) ) ) } )
	  
 ( K e. Field -> ( L e. ( AlgClosure ` K ) <-> ( L e. Field /\
      ( A. p e. ( Base ` ( Poly1 ` L ) ) ( ( deg1 ` p ) e. NN ->
      E. z e. ( Base ` L ) ( ( ( eval1 ` L ) ` p ) ` z ) = ( 0g ` L ) ) /\
      E. f e. ( K RingHom L ) A. x e. L E. q e. ( Base ` ( Poly1 ` K ) )
      ( ( q o. f ) =/= ( 0g ` ( Poly1 ` L ) ) /\
      ( ( ( eval1 ` L ) ` q ) ` ( f ` x ) ) = ( 0g ` L ) ) ) ) ) )

set.mm

avekens · 2025-01-11T09:17:21Z

The two defining theorems should be named as

algclfval $p |- ( K e. Field -> ( AlgClosure ` K ) = { l e. Field |
      ( A. p e. ( Base ` ( Poly1 ` l ) ) ( ( deg1 ` p ) e. NN ->
      E. z e. ( Base ` l ) ( ( ( eval1 ` l ) ` p ) ` z ) = ( 0g ` l ) ) /\
      E. f e. ( K RingHom l ) A. x e. l E. q e. ( Base ` ( Poly1 ` K ) )
      ( ( q o. f ) =/= ( 0g ` ( Poly1 ` l ) ) /\
      ( ( ( eval1 ` l ) ` q ) ` ( f ` x ) ) = ( 0g ` l ) ) ) } )
	  
 isalgcl $p |- ( K e. Field -> ( L e. ( AlgClosure ` K ) <-> ( L e. Field /\
      ( A. p e. ( Base ` ( Poly1 ` L ) ) ( ( deg1 ` p ) e. NN ->
      E. z e. ( Base ` L ) ( ( ( eval1 ` L ) ` p ) ` z ) = ( 0g ` L ) ) /\
      E. f e. ( K RingHom L ) A. x e. L E. q e. ( Base ` ( Poly1 ` K ) )
      ( ( q o. f ) =/= ( 0g ` ( Poly1 ` L ) ) /\
      ( ( ( eval1 ` L ) ` q ) ` ( f ` x ) ) = ( 0g ` L ) ) ) ) ) )

metakunt · 2025-01-11T12:11:49Z

The two defining theorems should be named as

algclfval $p |- ( K e. Field -> ( AlgClosure ` K ) = { l e. Field |
      ( A. p e. ( Base ` ( Poly1 ` l ) ) ( ( deg1 ` p ) e. NN ->
      E. z e. ( Base ` l ) ( ( ( eval1 ` l ) ` p ) ` z ) = ( 0g ` l ) ) /\
      E. f e. ( K RingHom l ) A. x e. l E. q e. ( Base ` ( Poly1 ` K ) )
      ( ( q o. f ) =/= ( 0g ` ( Poly1 ` l ) ) /\
      ( ( ( eval1 ` l ) ` q ) ` ( f ` x ) ) = ( 0g ` l ) ) ) } )
	  
 isalgcl $p |- ( K e. Field -> ( L e. ( AlgClosure ` K ) <-> ( L e. Field /\
      ( A. p e. ( Base ` ( Poly1 ` L ) ) ( ( deg1 ` p ) e. NN ->
      E. z e. ( Base ` L ) ( ( ( eval1 ` L ) ` p ) ` z ) = ( 0g ` L ) ) /\
      E. f e. ( K RingHom L ) A. x e. L E. q e. ( Base ` ( Poly1 ` K ) )
      ( ( q o. f ) =/= ( 0g ` ( Poly1 ` L ) ) /\
      ( ( ( eval1 ` L ) ` q ) ` ( f ` x ) ) = ( 0g ` L ) ) ) ) ) )

Hah, that's worrying. The definition (likely) resolves to the empty set. I can't apply fvmptd as I can't prove sethood hypothesis of the function value.

How should I resolve this?

avekens · 2025-01-11T13:54:41Z

Maybe an ordered-pair class abstraction should be used instead of a maps-to notation (like for subgraphs, see ~df-subgr:

df-algcl $a |- isAlgCl = { <. l , k >. | ( l e. Field /\ k e. Field /\
      ( A. p e. ( Base ` ( Poly1 ` l ) ) ( ( deg1 ` p ) e. NN ->
      E. z e. ( Base ` l ) ( ( ( eval1 ` l ) ` p ) ` z ) = ( 0g ` l ) ) /\
      E. f e. ( k RingHom l ) A. x e. l E. q e. ( Base ` ( Poly1 ` k ) )
      ( ( q o. f ) =/= ( 0g ` ( Poly1 ` l ) ) /\
      ( ( ( eval1 ` l ) ` q ) ` ( f ` x ) ) = ( 0g ` l ) ) ) ) }

Then we have:

 isalgcl $p |- ( ( L e. Field /\ K e. Field ) -> ( L isAlgCl K <->
      ( A. p e. ( Base ` ( Poly1 ` L ) ) ( ( deg1 ` p ) e. NN ->
      E. z e. ( Base ` L ) ( ( ( eval1 ` L ) ` p ) ` z ) = ( 0g ` L ) ) /\
      E. f e. ( K RingHom L ) A. x e. L E. q e. ( Base ` ( Poly1 ` K ) )
      ( ( q o. f ) =/= ( 0g ` ( Poly1 ` L ) ) /\
      ( ( ( eval1 ` L ) ` q ) ` ( f ` x ) ) = ( 0g ` L ) ) ) ) )

avekens · 2025-01-11T14:19:31Z

Alternatively, an operation can be defined, as done for fldGen in #4553 (df-fldgen).

metakunt · 2025-01-11T15:01:54Z

I have used the definition you've provided and proved isalgcl. Thanks for the help.

tirix · 2025-01-11T15:03:59Z

I think it might be interesting, as an intermediate step, to define the class of algebraically closed fields.
There are already many properties to be proved with that object, and it even has its own Wikipedia page (that's a definitive criterion!).

metakunt · 2025-01-11T15:26:33Z

Can I get reverse closure. Given L isAlgCl K can I get that L and K are fields?
I've tried the following:


h1::algclelim.1    |- ( ( ph /\ L isAlgCl K ) -> ch )

h2::algclelim.2           |- ( ph -> K e. Field )
d1::nfv            |- F/ l ph
d2::nfv            |- F/ l ch
d6::ax-algclex     |- ( K e. Field -> E. l l isAlgCl K )
d3:d5,d6:syl       |- ( ph -> E. l l isAlgCl K )
!d4::              |- ( ( ph /\ l isAlgCl K ) -> ch )
qed:d1,2,d3,d4:exlimdd   |- ( ph -> ch )

yet I fail to show d4 from h1. I'd like to use something like this https://us.metamath.org/mpeuni/vtocld.html

set.mm

metakunt · 2025-01-12T15:29:48Z

Exactly, I want to state L as a class and not as a set. The final step will substitute l for L to eliminate it.

metakunt · 2025-01-12T15:39:17Z

How do I split a long link?

avekens · 2025-01-12T15:59:50Z

I think it might be interesting, as an intermediate step, to define the class of algebraically closed fields. There are already many properties to be proved with that object, and it even has its own Wikipedia page (that's a definitive criterion!).

So maybe:

df-aclfld $a |- AlgClField = { f e. Field | A. p e. ( Base ` ( Poly1 ` f ) )
                 ( ( deg1 ` p ) e. NN ->E. z e. ( Base ` f ) ( ( ( eval1 ` f ) ` p ) ` z ) = ( 0g ` f ) ) }

with

isaclfld $p |- ( F e. AlgClField <-> ( F e. Field /\ A. p e. ( Base ` ( Poly1 ` F ) )
        ( ( deg1 ` p ) e. NN ->E. z e. ( Base ` F ) ( ( ( eval1 ` F ) ` p ) ` z ) = ( 0g ` F ) ) ) )

and then:

df-algcl $a |- isAlgCl = { <. l , k >. | ( k e. Field /\ l e. AlgClField
     /\ E. f e. ( k RingHom l ) A. x e. l E. q e. ( Base ` ( Poly1 ` k ) )
      ( ( q o. f ) =/= ( 0g ` ( Poly1 ` l ) ) /\ ( ( ( eval1 ` l ) ` q ) ` ( f ` x ) ) = ( 0g ` l ) ) }

with

 isalgcl $p |- ( ( L e. Field /\ K e. Field ) -> ( L isAlgCl K <->( L e. AlgClField 
        /\ E. f e. ( K RingHom L ) A. x e. L E. q e. ( Base ` ( Poly1 ` K ) )
            ( ( q o. f ) =/= ( 0g ` ( Poly1 ` L ) ) /\ ( ( ( eval1 ` L ) ` q ) ` ( f ` x ) ) = ( 0g ` L ) ) ) )

metakunt · 2025-01-12T16:07:32Z

So in lean it's defined as Algebraically closed and Algebraic, we can have that definition.

avekens · 2025-01-12T16:23:17Z

To be more general, we can omit the e. Field in the definition, so that we get a concept of algebraically closed classes/structures (to be meaningful, there should be at least a base set and a zero element):

df-acl $a |- AlgCl = { f | A. p e. ( Base ` ( Poly1 ` f ) )
                 ( ( deg1 ` p ) e. NN ->E. z e. ( Base ` f ) ( ( ( eval1 ` f ) ` p ) ` z ) = ( 0g ` f ) ) }

langgerard · 2025-01-12T18:16:50Z

In the comment for isalgcl, the polynom p should be a positive degree

icecream17

For now with the long link use a url shortener

Edit: Yeah, metamath.exe rewrap does not split the url, so it's not supported.

icecream17 · 2025-01-11T15:04:50Z

set.mm

-  latexdef "AlgCl" as "\mathrm{AlgCl}";
+htmldef "isAlgCl" as ' isAlgCl ';
+  althtmldef "isAlgCl" as ' isAlgCl ';
+  latexdef "isAlgCl" as "\mathrm{isAlgClc}";


Suggested change

latexdef "isAlgCl" as "\mathrm{isAlgClc}";

latexdef "isAlgCl" as "\mathrm{isAlgCl}";

typo

I tried to commit your suggestion. it sadly didn't work. I've manually commited it.

metakunt · 2025-01-20T10:11:09Z

So what do I do with the link then?

icecream17 · 2025-02-11T23:48:49Z

An alternative to a url shortener as stated above is to create a file on github for maybe not only just the single link but more links and commentary.

(I was thinking about making a place for links since I keep finding random ones like https://www.c82.net/euclid/ that might be lost because of disorganization and that I'm not working on it right now)

If such a page is on github it is likely that the resulting link will fit, even with a #section-heading at the end

avekens · 2025-02-16T10:49:31Z

What is the status of this old PR? The only open issue seems to be the link which is too long. So either (my preference in the given order):

find a shorter link (maybe by an url shortener,as proposed above)
follow the approach proposed by @icecream17 4 days ago
split the link (then it cannot be clicked in the html page)
remove the link

metakunt · 2025-02-17T21:46:51Z

Oh, sorry I am currently a little bit on the busier side. I will clean the PR up when I find time.

metakunt · 2025-04-03T18:48:32Z

I have fixed up the definitions and added @avekens comments. I'll do a refactor once I have again some more time in the future.

I am unsure whether this axiomatic approach is good. I see @tirix progress and I am debating whether I should wait or help him prove key lemmas. After all it would be nicer if it didn't rely on some hypotheses which I just postulate, even though they have been proven.

tirix · 2025-04-04T07:07:39Z

I'm progressing, but at a very slow pace! :-)

One interesting tool would be to use E IntgRing F : the elements of a field E algebraic over a subfield F.

Then to write "F is algebraically closed (in E)", one could simply write ( E IntgRing F ) = F, i.e. all elements of F are algebraic.

As for the algebraic closure, one tool we use often is the intersection. The algebraic closure of F in E could be written as

|^| { a e. ( SubDRing ` E ) | ( F C_ a /\ ( E IntgRing a ) = a ) }

I.e. the algebraic closure of F is the intersection of all subfields of E containing F and algebraically closed - that is, the smallest algebraically closed subfield of E containing F.

Its existence would be trivial as soon as E itself is algebraically closed.

The advantage to reuse IntgRing would be that you have access to the theorems I've proved about it - and conversely, you would enrich the database with any new theorems about it.

tirix · 2025-04-04T07:48:11Z

PS. This approach has the drawback that a "bigger field" E is necessary. For Galois fields $GF(p)$, you'd first have to check out $GF_\infty(p)$. @digama0 has formalized its definition in ~ df-gfoo.

I think my recently defined minPoly might be used to shorten some of the definitions involved in splitFld (specifically splitFld1).

metakunt · 2025-04-04T10:31:08Z

Ok I'll think I'll go with your approach. To build it from the ground up.
Sadly I am not aware of the technical details regarding the construction, maybe because the literature is a little bit unformal or maybe if you omit certain details and accept several things that you just move at a faster pace.

I wouldn't know where to start currently anyways. Maybe we should just try to find out which lemmas/concepts we need to progress and where we can cut corners. For example we might not need the full construction with arbitrary fields, which involve Zorn's lemma but instead do it with @digama0's definition.

I currently have more of a problem is I miss the forest because of the trees. I'll gladly work on the lower level technical details to get the formalisation moving, but I don't feel comfortable to start because I am missing the general idea of the proof. Currently I have proven everything that is not construction dependent, Theorem 6.1 seemed to depend on much of the construction of the algebraic closure. Maybe we can modularise that better and extract data so that we have three tasks.

Define data needed to finish the proof
Prove the existence of the data by constructing the algebraic closure with the properties
Prove Th 6.1 dependent on this data.

I don't know what data we need. I'd assume, existence of primitive roots, algebraic closure property for arbitrary elements (for the inverse of the Frobenius, although here it's likely that any finite field that contains primitive roots would suffice) and several facts about primitive roots in general.

What do you think about it? Would this be something that interests you?

tirix · 2025-04-04T13:05:44Z

I think maybe the only API you need is:

$GF_\infty(p)$ has characteristic $p$ - so that Fermat's little theorem for polynomials applies,
$GF_\infty(p)$ is an algebraically closed field - so that it's perfect, and the Frobenius endomorphism is surjective (an automorphism).
$GF_\infty(p)$ contains some $r$-th primitive root of the unity $\mu$ as in the hypotheses in 6.1 (actually it contains all $r$-th primitive root of the unity for $r$ coprime with $p$)

So you can either:

aim at proving those properties or $GF_\infty(p)$, from its definition up,
or you postulate the existence of a field with those properties until we can prove that $GF_\infty(p)$ has them.

We might still have to introduce a definition and some properties for perfect fields for the second bullet point.

metakunt · 2025-04-04T17:56:35Z

Thank you for your feedback.

Alright, that sounds good. I'll go with that approach and close this PR as it won't be used.

I'll open a PR in the blueprints repo outlining how I would do it, I'll try to bundle the data and see if it works.
Let's see if with those definitions we can make some progress. In lean with the api defined I could do some transformations. The proofs itself were mechanical by nature and I hope that I can port them easily.

Algebraic closure definition and existence axiom.

c52421d

metakunt added 7 commits January 11, 2025 05:41

fix def algebraic

b65fbc8

fix definition algebraic

2e2dc0b

Add degree condition on existential

d8fe7a2

fmt

3df3370

typo

3b105fa

replace deg condition with nonzero condition

427e9a9

defs

6a2b398

wlammen added the mathbox only label Jan 11, 2025

Hopefully fix the def

2865cd4

avekens reviewed Jan 11, 2025

View reviewed changes

set.mm Show resolved Hide resolved

avekens reviewed Jan 11, 2025

View reviewed changes

set.mm Show resolved Hide resolved

avekens reviewed Jan 11, 2025

View reviewed changes

set.mm Show resolved Hide resolved

small things

fc000a0

metakunt added 2 commits January 11, 2025 13:13

missed renames

3404b4c

rewrap

45a0bbd

refactor algebraic closure as a class

170118a

avekens reviewed Jan 12, 2025

View reviewed changes

set.mm Show resolved Hide resolved

Add comments

d1805d1

icecream17 reviewed Jan 15, 2025

View reviewed changes

tirix mentioned this pull request Jan 26, 2025

Constructible numbers - initial idea #4578

Merged

metakunt marked this pull request as draft February 17, 2025 21:47

shorten url

97148b7

metakunt marked this pull request as ready for review April 3, 2025 17:45

metakunt added 5 commits April 3, 2025 19:47

typo

0228797

av changes

185dab1

latex labels

bfdfaf2

fix proof

20363d3

formatting

a32e34d

metakunt closed this Apr 4, 2025

metakunt deleted the alg-closure branch April 4, 2025 17:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Algebraic closure definition and existence axiom. #4554

Algebraic closure definition and existence axiom. #4554

metakunt commented Jan 11, 2025

icecream17 commented Jan 11, 2025

metakunt commented Jan 11, 2025 •

edited

Loading

icecream17 commented Jan 11, 2025 •

edited

Loading

icecream17 commented Jan 11, 2025 •

edited

Loading

metakunt commented Jan 11, 2025 •

edited

Loading

avekens commented Jan 11, 2025

avekens commented Jan 11, 2025

metakunt commented Jan 11, 2025 •

edited

Loading

avekens commented Jan 11, 2025

avekens commented Jan 11, 2025

metakunt commented Jan 11, 2025

tirix commented Jan 11, 2025

metakunt commented Jan 11, 2025 •

edited

Loading

metakunt commented Jan 12, 2025

metakunt commented Jan 12, 2025

avekens commented Jan 12, 2025 •

edited

Loading

metakunt commented Jan 12, 2025

avekens commented Jan 12, 2025 •

edited by tirix

Loading

langgerard commented Jan 12, 2025

icecream17 left a comment •

edited

Loading

icecream17 Jan 11, 2025

metakunt Apr 3, 2025

metakunt commented Jan 20, 2025

icecream17 commented Feb 11, 2025 •

edited

Loading

avekens commented Feb 16, 2025

metakunt commented Feb 17, 2025

metakunt commented Apr 3, 2025

tirix commented Apr 4, 2025

tirix commented Apr 4, 2025 •

edited

Loading

metakunt commented Apr 4, 2025

tirix commented Apr 4, 2025 •

edited

Loading

metakunt commented Apr 4, 2025

	latexdef "isAlgCl" as "\mathrm{isAlgClc}";
	latexdef "isAlgCl" as "\mathrm{isAlgCl}";

Algebraic closure definition and existence axiom. #4554

Algebraic closure definition and existence axiom. #4554

Conversation

metakunt commented Jan 11, 2025

icecream17 commented Jan 11, 2025

metakunt commented Jan 11, 2025 • edited Loading

icecream17 commented Jan 11, 2025 • edited Loading

icecream17 commented Jan 11, 2025 • edited Loading

metakunt commented Jan 11, 2025 • edited Loading

avekens commented Jan 11, 2025

avekens commented Jan 11, 2025

metakunt commented Jan 11, 2025 • edited Loading

avekens commented Jan 11, 2025

avekens commented Jan 11, 2025

metakunt commented Jan 11, 2025

tirix commented Jan 11, 2025

metakunt commented Jan 11, 2025 • edited Loading

metakunt commented Jan 12, 2025

metakunt commented Jan 12, 2025

avekens commented Jan 12, 2025 • edited Loading

metakunt commented Jan 12, 2025

avekens commented Jan 12, 2025 • edited by tirix Loading

langgerard commented Jan 12, 2025

icecream17 left a comment • edited Loading

Choose a reason for hiding this comment

icecream17 Jan 11, 2025

Choose a reason for hiding this comment

metakunt Apr 3, 2025

Choose a reason for hiding this comment

metakunt commented Jan 20, 2025

icecream17 commented Feb 11, 2025 • edited Loading

avekens commented Feb 16, 2025

metakunt commented Feb 17, 2025

metakunt commented Apr 3, 2025

tirix commented Apr 4, 2025

tirix commented Apr 4, 2025 • edited Loading

metakunt commented Apr 4, 2025

tirix commented Apr 4, 2025 • edited Loading

metakunt commented Apr 4, 2025

metakunt commented Jan 11, 2025 •

edited

Loading

icecream17 commented Jan 11, 2025 •

edited

Loading

icecream17 commented Jan 11, 2025 •

edited

Loading

metakunt commented Jan 11, 2025 •

edited

Loading

metakunt commented Jan 11, 2025 •

edited

Loading

metakunt commented Jan 11, 2025 •

edited

Loading

avekens commented Jan 12, 2025 •

edited

Loading

avekens commented Jan 12, 2025 •

edited by tirix

Loading

icecream17 left a comment •

edited

Loading

icecream17 commented Feb 11, 2025 •

edited

Loading

tirix commented Apr 4, 2025 •

edited

Loading

tirix commented Apr 4, 2025 •

edited

Loading