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 On 23/08/2024 18:30, 'Meta Kunt' via Metamath wrote:
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 <https://www.eclipso.eu>*. -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4315efc33341c08f6d04da88375a307f%40mail.eclipso.de <https://groups.google.com/d/msgid/metamath/4315efc33341c08f6d04da88375a307f%40mail.eclipso.de?utm_medium=email&utm_source=footer>.
-- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/36df3e97-51ad-4aa5-a132-af645cb54b56%40gmx.net.
