Algebraic closedness of the complexification

finrank_eq_one_of_forall_isSquare proves that a finite extension of a finite square-closed extension of a real closed field is trivial. isAlgClosed_of_forall_isSquare then proves algebraic closedness of that square-closed field. In particular, isAlgClosed_quadraticAlgebra proves that R[i] = QuadraticAlgebra R (-1) 0 is algebraically closed. Polynomial.natDegree_le_two_of_irreducible bounds irreducible degrees by two; the polynomial IVT development uses this bound. Open scoped TauCeti.RealClosure to enable the algebraic-closedness instance on this quadratic algebra.

The proof puts finite extensions inside a finite normal closure. The 2-group argument then applies to the Galois group over a square-closed intermediate field.

The degree bound generalizes Mathlib's Irreducible.natDegree_le_two from Mathlib.Analysis.Complex.Polynomial.Basic, following its root, minimal polynomial, and finite-dimension proof over an arbitrary real closed field.

References

The algebraic argument uses a Sylow 2-subgroup of the Galois group; see Salma Kuhlmann, Real Algebraic Geometry, Lecture 5, Theorem 2.2.

theorem TauCeti.RealClosure.finrank_eq_one_of_forall_isSquare {R : Type u_1} {C : Type u_2} {L : Type u_3} [Field R] [IsRealClosed R] [Field C] [Algebra R C] [FiniteDimensional R C] [Field L] [Algebra R L] [Algebra C L] [IsScalarTower R C L] [FiniteDimensional C L] (hsq : ∀ (x : C), IsSquare x) : Module.finrank C L = 1

Every finite extension of a finite square-closed extension of a real closed field is trivial.

theorem TauCeti.RealClosure.isAlgClosed_of_forall_isSquare {R : Type u_1} {C : Type u_2} [Field R] [IsRealClosed R] [Field C] [Algebra R C] [FiniteDimensional R C] (hsq : ∀ (x : C), IsSquare x) : IsAlgClosed C

A finite square-closed extension of a real closed field is algebraically closed.

theorem TauCeti.RealClosure.isAlgClosed_quadraticAlgebra {R : Type u_1} [Field R] [IsRealClosed R] : IsAlgClosed (QuadraticAlgebra R (-1) 0)

The complexification R[i] of a real closed field is algebraically closed.

theorem Polynomial.natDegree_le_two_of_irreducible {R : Type u_1} [Field R] [IsRealClosed R] (p : Polynomial R) (hp : Irreducible p) : p.natDegree ≤ 2

Irreducible polynomials over a real closed field have degree at most two.