The Galois-theoretic reduction for real closed fields #
A finite Galois extension of a real closed field has a 2-group of automorphisms.
Over a square-closed intermediate extension it is trivial. These degree reductions
are used to prove algebraic closedness in AlgebraicClosed.lean.
References #
The Sylow 2-subgroup and index-two subgroup steps of the Artin–Schreier argument; see Salma Kuhlmann, Real Algebraic Geometry, Lecture 5, Theorem 2.2.
theorem
TauCeti.RealClosure.isPGroup_two_algEquiv
{R : Type u_1}
{E : Type u_2}
[Field R]
[IsRealClosed R]
[Field E]
[Algebra R E]
[FiniteDimensional R E]
[IsGalois R E]
:
IsPGroup 2 Gal(E/R)
A finite Galois extension of a real closed field has a 2-group as Galois group.
theorem
TauCeti.RealClosure.finrank_eq_one_of_isPGroup
{K : Type u_3}
{L : Type u_4}
[Field K]
[NeZero 2]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[IsGalois K L]
(hsq : ∀ (x : K), IsSquare x)
(hG : IsPGroup 2 Gal(L/K))
:
A square-closed field of characteristic different from two has no nontrivial finite Galois extension whose Galois group is a 2-group.
theorem
TauCeti.RealClosure.finrank_eq_one_of_isGalois_of_forall_isSquare
{R : Type u_1}
{E : Type u_2}
[Field R]
[IsRealClosed R]
[Field E]
[Algebra R E]
[FiniteDimensional R E]
[IsGalois R E]
{C : Type u_3}
[Field C]
[Algebra R C]
[Algebra C E]
[IsScalarTower R C E]
(hsq : ∀ (x : C), IsSquare x)
:
Over a square-closed intermediate extension of a real closed field, every finite Galois extension of the base becomes trivial.