[Metamath] Developing Galois theory in set.mm

['Meta Kunt' via Metamath]

­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.

--
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4315efc33341c08f6d04da88375a307f%40mail.eclipso.de.