Field Extension of deg 2 isomorphic to square root adjoint

Stream: Is there code for X?

[Maik Fücks]

Hello,

Im trying to formalize a Galois-theoretic proof of the fundamental theorem of Algebra and i was looking for the result, that for a field (with characteristic other than 2) every quadratic Fieldextension is isomorphic to a adjoining a squareroot. Does anybody know if this is already in mathlib? I haven't found it so far.

Kind regards,
Maik

[Kevin Buzzard]

Have you formalised the statement?

[Maik Fücks]

This is what i thought of:

lemma quad_field_ext_iso_adj_sqrt (K L : Type) [Field L] [Field K] [Algebra K L] (hnchar2 : ¬CharP K 2) (h : finrank K L = 2) :
∃ α, α ∈ {u : K | ¬ ∃ w : K, w^2 = u } ∧ Nonempty (L ≃+* Algebra.adjoin K {α})

[Edward van de Meent]

please use #backticks

[Kevin Buzzard]

This isn't an accurate translation of the statement because the isomorphism you're asking for might not be K-equivariant. Maybe you just want that the adjoin is \top.

[Kevin Buzzard]

Wait this definitely isn't right because you never took the square root of alpha

[Maik Fücks]

Thats true, my bad. I will fix it.

[Maik Fücks]

So for the "root of alpha" problem, i came up with this possible solution:

lemma quad_field_ext_iso_adj_sqrt (K L : Type) [Field L] [Field K] [Algebra K L] (hnchar2 : ¬CharP K 2) (h : finrank K L = 2) :
  ∃ α, α ∈ {u : K | ¬ ∃ w : K, w^2 = u } ∧ Nonempty (L ≃+* AdjoinRoot (Polynomial.X^2 - Polynomial.C α)) := sorry

[Maik Fücks]

So for my purposes, i think i actually dont even need the isomorphism, but only the alpha as sort of a "certificate" of the existence of a quadratic extension, since i want to show that there are no quadratic extensions of the complex numbers by proving that there is no non-square in C. Something like

lemma quad_field_ext_iso_adj_sqrt_short (K L : Type) [Field L] [Field K] [Algebra K L] (hnchar2 : ¬CharP K 2) (h : finrank K L = 2)
 : ∃ α, α ∈ {u : K | ¬ ∃ w : K, w^2 = u }

[Kevin Buzzard]

Why don't you just prove there are no quadratic extensions of the complex numbers by proving that all quadratic equations have roots using the quadratic formula? Then you don't need to complete the square.

[Maik Fücks]

I was following along a proof on paper and thought if the result i asked for was actually in mathlib, it might not be the worst way to go along. But yeah, considering its not there (and im still quite new to lean) i might follow your advice and go along with the quadratic formula. Many thanks! (Also for your very good free "Formalizing Mathmatics 2024" course, which i just worked through to get into lean)

[Kevin Buzzard]

I was just raising the objection that "every complex number has a square root" is not really harder than "any monic quadratic equation has a complex root". There's no harm in following the paper proof, it's just that I am now very skeptical of paper proofs, because at least when I was writing them, I'd just write down a random thing which looked like it works rather than thinking hard about what was actually going on.

[Maik Fücks]

i got it all working now, thanks for your input!