Developing Galois theory in set.mm

[Meta Kunt]

­Hey guys,

I'd like to develop a nice API of Galois theory and algebraic closures, in particular I want existence of primitive roots and some group theory to count the number of elements satisfying a condition.

Most of the definitions are in Mario's mathbox. However since I don't quite fully understand the intricacies of splitting field and direct limits, I'd need some handholding.#
These definitions would need to be moved out of Mario's mathbox.
HomLimB,HomLim,polyFld,splitFld1,splitFld1,polySplitLim,gf,gfoo­

Also I'd like to know what the API of the theorems is that I need to prove. I am certain that Mario's work is excellent, however based on any definition I would struggle to develop any api.
If we could discuss what theorems we need to formalise to develop a good API of the theory. But not only that, there will be lots of connective work linking definitions to powerful theorems that use it.

As a goal I'd like to construct the field GF(4) and explicitly calculate the elements of it. By Mario's definition this is the splitting field of (X^4-X)=(X^2+X+1)(X-1)(X) so there is already a big hurdle to overcome.
We could link the definition of GF(4) which would just be ( 2 GF 2 ) in set.mm
splitFld itself is another binary operation, this time substituted and in prosa would be similar to metamaths ( Z_2 splitFld (X^4-X) )
We now inside splitFld get an isomorphism predicate that says that we adjoin the roots in order, atleast that's what I think it does as (# ` p ) = 1 in our case. But the value is another more complicated map in what
appears to be adjoining either another more technical root or the identity function and sequentially repeating the process.
It appears even crazier that splitFld1 chooses a monic irreducible polynomial in a "canonical" way and then does a field extension with that polynomial. After that I didn't bother to much understand it since
this is several layers too deep already.


The first goal, as funnily as it is, is to likely develop the api bottom up, which means defining important lemmas for polyFld first.

I assume we shall be able to prove something like that.
Let K be a field let f in K[X] be monic and irreducible (note irreducible is likely enough). Then K[X]/(f) is a field.

I'd then like to be able to prove following results:
( Z_2 polyFld (X^2+X+1) ) is a field, contains 4 elements and give a description of how those 4 elements look.

Thank you.
metakunt

---

Your E-Mail. Your Cloud. Your Office. eclipso Mail Europe.

[Thierry Arnoux]

Hi metakunt,

Sorry I don't have much time this week for a long answer.

I think the best course of action would be to identify a good reference textbook, and follow along with the definitions and properties. I cannot help much with that choice as I'm not an expert in the domain. 

Milne's course notes are available online, so using them will help anyone who does not have access to a physical math library.

    https://www.jmilne.org/math/CourseNotes/FT.pdf

Then other options that come to mind is simply to look at the references listed in the Wikipedia page for Finite Fields... and ask the community, like in this question:

    https://mathoverflow.net/questions/126364/books-on-advanced-galois-theory

It's usually easier to go from the more general to the "numerical" application, so a general advice would be to not restrict yourself too much to a single application.

Pulling `polyFld` into main or your own mathbox and starting proving theorems like "a splitting field is a field", "a splitting field is a field extension", etc. sounds like a great start.

BR,
_
Thierry

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4315efc33341c08f6d04da88375a307f%40mail.eclipso.de.

[heiph...@wilsonb.com]

FWIW, Tom Leinster just shared a bunch of materials he organized from a Galois
Theory course: https://www.maths.ed.ac.uk/~tl/galois/ . In addition to a book,
there are quizzes, videos, and problem sets. At a first glance it looks quite
terrific.

[Steven Nguyen]

Galois theory seems to be very useful; I've heard about it many times, but unfortunately, I haven't learned any of it yet. I agree that moving the definitions and proving simple properties like Thierry said is the best option, since the definitions aren't used yet.

By the way, in Milne's notes (https://www.jmilne.org/math/CourseNotes/FT.pdf) page 7, it states a definition of Integral Domains that does not seem to match with any of the theorems around https://us.metamath.org/mpeuni/mmtheorems201.html#df-idom

[heiph...@wilsonb.com]

> By the way, in Milne's notes (https://www.jmilne.org/math/CourseNotes/FT.pdf)
> page 7, it states a definition of Integral Domains that does not seem to
> match with any of the theorems around
> https://us.metamath.org/mpeuni/mmtheorems201.html#df-idom

The cancellation law condition is equivalent to the zero divisors one. The
proof is short and sweet, but I don't see it in set.mm. Maybe you want to make
dfdomn?

[Meta Kunt]

I am trying to prove the weak compositions of integers by giving an explicit
isomorphism. https://en.wikipedia.org/wiki/Composition_(combinatorics)
In particular I want to prove theorem 2 of https://en.wikipedia.org/wiki/Stars_and_bars_(combinatorics)


```

h1:: |- ( ph -> N e. NN )
h2:: |- ( ph -> K e. NN0 )
h3:: |- A = { a e. ~P ( 1 ... ( ( N - 1 ) + K ) ) | ( # ` a ) = N }


h4:: |- B = { f | ( f : ( 1 ... N ) --> NN0 /\ sum_ i e. ( 1 ... N ) (
f ` i ) = K ) }

h5:: |- F = ( x e. A |-> ( h e. ( 1 ... N ) |-> if ( h = N , ( ( (
N + K ) - 1 ) - sup ( x , RR , < ) ) , ( ( ( iota_ d e. x ( # ` { v e.
x | v <_ d } ) = ( h + 1 ) ) - ( iota_ e e. x ( # ` { w e. x | w <_
e } ) = h ) ) - 1 ) ) ) )
h6:: |- G = ( y e. B |-> { l e. ( 1 ... ( ( N - 1 ) + K ) ) | E. s e.
( 1 ... N ) l = ( sum_ t e. ( 1 ... s ) ( y ` t ) + ( s - 1 ) ) } )
qed:?: |- ( ( ph /\ X e. A ) -> ( F ` ( G ` X ) ) = X )

```

In particular I want to calculate the size of B. My idea was to use an explicit
isomorphism from A to B while there is a theorem that gives me the size of
A, namely https://us.metamath.org/mpeuni/hashbcval.html

I don't know if my definitions are the best or if there is a better way.


Alternatively I have tried to maybe use the isomorphism of the k-element subsets of 1 to n to the ordered functions
of ( 1 ... N ) to ( 1 ... K ) where for a < b f(a) < f(b) and use that to show that this is isomorphic to B.
There seems to be something that is likely nice to be used. https://us.metamath.org/mpeuni/fz1iso.html
But I have not figured out a proof blueprint. Some similar lemmas exist but I am not sure what the least painful way of doing things is.

My plan was to show that the strictly monotone increasing functions from ( 1 ... K ) to ( 1 ... N ) are bijective onto the k-element subsets of ( 1 ... N )
The mapping g taking a function f onto the power set of ( 1 ... N ) is defined by taking the range of f. I want to show that the function g is injective by
considering two f1, f2 and show that g(f1) is not equal to g(f2)
Surjectivity I want to show separately. Given a k-elemental subset x of ( 1 ... N ) generate the order isomorphism with fz1iso and put it in the range function.
therefore let y be the order isomorphism of x and show that it is a monotonely increasing function from ( 1 ... K ) to ( 1 ... N )

Is this plan sound? Because I seem to struggle with the existential quantor in fz1iso.





________________________________________________________
Your E-Mail. Your Cloud. Your Office. eclipso Mail Europe. https://www.eclipso.eu

[Jim Kingdon]

On 9/22/24 11:01, 'Meta Kunt' via Metamath wrote:
> Is this plan sound? Because I seem to struggle with the existential quantor in fz1iso.

I won't try to reply to everything you were trying to do but if you are
having the same struggle I used to have with existential quantifiers you
might be looking for https://us.metamath.org/mpeuni/exlimddv.html

Its usage in https://us.metamath.org/mpeuni/xpdom2.html is pretty typical.