Concrete field extensions

Stream: Is there code for X?

[Artie Khovanov]

I'm having a bit of trouble finding some material on field extensions, and I'm not sure if it's because my searching skills are bad or because it's not there. I've found stuff on Kummer theory and the Galois correspondence which looks good to me!

• Quadratic extensions: I found the definition IsQuadraticExtension, but do we have the result classifying separable quadratic extensions of a field $K$ via $K^*/(K^2)*$?
• Artin-Schreier extensions: I can't find anything on these at all.

[Kenny Lau]

@Artie Khovanov the canonical way to write field extension is [Field K] [Field L] [Algebra K L].

[Artie Khovanov]

Yes, I'm aware. I also know how to write down $K(\alpha)$ with $\alpha$ a root of an irreducible $f\in K[X]$. I'm not asking how to make definitions - I'm asking if the theories of quadratic and Artin-Schreier extensions that I described have been formalised anywhere.

[Kenny Lau]

@Artie Khovanov Well, if you look at the file for Kummer theory, it does say that it is a TODO to relate that file to Algebra.IsQuadraticExtension, so please feel free to do it! :slight_smile:

[Artie Khovanov]

Ah OK - looks like the answer to my first question is "no", then!
Do you know about the Artin-Schreier extensions?

[Kenny Lau]

It doesn't seem to exist from my searching