Documentation

RealClosedField.RealClosedField

class IsRealClosed (R : Type u_1) [Field R] extends IsSemireal R :

A field R is real closed if

R is real
for all x ∈ R, either x or -x is a square
every odd-degree polynomial has a root.

one_add_ne_zero {s : R} (hs : IsSumSq s) : 1 + s ≠ 0
isSquare_or_isSquare_neg (x : R) : IsSquare x ∨ IsSquare (-x)
exists_isRoot_of_odd_natDegree {f : Polynomial R} (hf : Odd f.natDegree) : ∃ (x : R), f.IsRoot x

Instances

class IsRealClosure (K : Type u_1) (R : Type u_2) [Field K] [Field R] [LinearOrder K] [LinearOrder R] [Algebra K R] [IsStrictOrderedRing R] [IsStrictOrderedRing K] extends IsRealClosed R, IsOrderedModule K R, Algebra.IsAlgebraic K R :

A real closure of an ordered field is a real closed ordered algebraic extension.

one_add_ne_zero {s : R} (hs : IsSumSq s) : 1 + s ≠ 0
isSquare_or_isSquare_neg (x : R) : IsSquare x ∨ IsSquare (-x)
exists_isRoot_of_odd_natDegree {f : Polynomial R} (hf : Odd f.natDegree) : ∃ (x : R), f.IsRoot x
smul_le_smul_of_nonneg_left ⦃a : K⦄ (ha : 0 ≤ a) ⦃b₁ b₂ : R⦄ (hb : b₁ ≤ b₂) : a • b₁ ≤ a • b₂
smul_le_smul_of_nonneg_right ⦃b : R⦄ (hb : 0 ≤ b) ⦃a₁ a₂ : K⦄ (ha : a₁ ≤ a₂) : a₁ • b ≤ a₂ • b
isAlgebraic (x : R) : IsAlgebraic K x

Instances

Sufficient conditions to be real closed #

theorem IsRealClosed.mk' {R : Type u} [Field R] [IsSemireal R] (h₁ : ∀ {x : R}, ¬IsSquare x → IsSquare (-x)) (h₂ : ∀ {f : Polynomial R}, f.Monic → Odd f.natDegree → f.natDegree ≠ 1 → ¬Irreducible f) :

theorem IsRealClosed.of_isAdjoinRoot_i_or_finrank_eq_one {R : Type u} [Field R] (hR : ¬IsSquare (-1)) (h : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra R K] [FiniteDimensional R K], IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1) ∨ Module.finrank R K = 1) :

theorem IsRealClosed.of_isAdjoinRoot_i_isAlgClosure {R : Type u} [Field R] {K : Type u_1} [Field K] [Algebra R K] [IsAlgClosure R K] (h : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)) :

theorem IsRealClosed.of_linearOrderedField {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x) (exists_isRoot_of_odd_natDegree : ∀ {f : Polynomial R}, Odd f.natDegree → ∃ (x : R), f.IsRoot x) :

theorem IsRealClosed.of_linearOrderedField' {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (h₁ : ∀ {x : R}, 0 ≤ x → IsSquare x) (h₂ : ∀ {f : Polynomial R}, f.Monic → Odd f.natDegree → f.natDegree ≠ 1 → ¬Irreducible f) :

theorem IsRealClosed.of_intermediateValueProperty {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (h : ∀ {f : Polynomial R} {x y : R}, x ≤ y → 0 ≤ Polynomial.eval x f → Polynomial.eval y f ≤ 0 → ∃ z ∈ Set.Icc x y, Polynomial.eval z f = 0) :

theorem IsRealClosed.of_maximal_isOrderedAlgebra {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (h : ∀ (K : Type u) [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : Algebra R K] [Algebra.IsAlgebraic R K] [IsOrderedModule R K], Module.finrank R K = 1) :

theorem IsRealClosed.of_maximal_isSemireal {R : Type u} [Field R] [IsSemireal R] (h : ∀ (K : Type u) [inst : Field K] [IsSemireal K] [inst_2 : Algebra R K] [Algebra.IsAlgebraic R K], Module.finrank R K = 1) :

theorem IsSquare.of_not_isSquare_neg {R : Type u} [Field R] [IsRealClosed R] {x : R} (hx : ¬IsSquare (-x)) :

theorem IsSquare.of_isSumSq {R : Type u} [Field R] [IsRealClosed R] {x : R} (hx : IsSumSq x) :

instance IsRealClosed.instFactIrreduciblePolynomialHAddHPowXOfNat {R : Type u} [Field R] [IsRealClosed R] :

Fact (Irreducible (Polynomial.X ^ 2 + 1))

theorem IsRealClosed.exists_eq_pow_of_odd {R : Type u} [Field R] [IsRealClosed R] (x : R) {n : ℕ} (hn : Odd n) :

∃ (r : R), x = r ^ n

theorem IsRealClosed.exists_eq_pow_of_isSquare {R : Type u} [Field R] [IsRealClosed R] {x : R} (hx : IsSquare x) {n : ℕ} (hn : n > 0) :

∃ (r : R), x = r ^ n

Classification of algebraic extensions of a real closed field #

theorem IsRealClosed.odd_finrank_extension (R : Type u) [Field R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] [FiniteDimensional R K] (hK : Odd (Module.finrank R K)) :

Module.finrank R K = 1

theorem IsRealClosed.isAdjoinRoot_i_of_isQuadraticExtension (R : Type u) [Field R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [Algebra.IsQuadraticExtension R K] :

IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)

theorem IsRealClosed.isSquare_algebraMap_of_isAdjoinRoot_i (R : Type u) [Field R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] (hK : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)) (x : R) :

IsSquare ((algebraMap R K) x)

theorem IsRealClosed.isSquare_of_isAdjoinRoot_i (R : Type u) [Field R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] (hK : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)) (x : K) :

theorem IsRealClosed.finrank_neq_two_of_isAdjoinRoot_i (R : Type u) [Field R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] (hK : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)) (L : Type u_2) [Field L] [Algebra K L] :

Module.finrank K L ≠ 2

theorem IsRealClosed.finite_extension_rank_le (R : Type u) [Field R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [FiniteDimensional R K] :

Module.finrank R K ≤ 2

theorem IsRealClosed.rank_eq_one_of_isAdjoinRoot_i (R : Type u) [Field R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] (hK : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)) (L : Type u_2) [Field L] [Algebra R L] [Algebra K L] [FiniteDimensional R L] [IsScalarTower R K L] :

Module.finrank K L = 1

theorem IsRealClosed.finite_extension_classify (R : Type u) [Field R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [FiniteDimensional R K] :

IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1) ∨ Module.finrank R K = 1

instance IsRealClosed.instFiniteDimensionalOfIsAlgebraic (R : Type u) [Field R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [Algebra.IsAlgebraic R K] :

FiniteDimensional R K

theorem IsRealClosed.maximal_isSemireal (R : Type u) [Field R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [IsSemireal K] [Algebra.IsAlgebraic R K] :

Module.finrank R K = 1

theorem IsRealClosed.isAdjoinRoot_i_of_isAlgClosure (R : Type u) [Field R] [IsRealClosed R] (K : Type u_1) [Field K] [Algebra R K] [IsAlgClosure R K] :

IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)

instance IsRealClosed.instIsQuadraticExtensionOfIsAlgClosure (R : Type u) [Field R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] [IsAlgClosure R K] :

Algebra.IsQuadraticExtension R K

theorem IsRealClosed.isAlgClosure_iff_isAdjoinRoot_i {R : Type u} [Field R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] :

IsAlgClosure R K ↔ IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)

theorem IsRealClosed.isAlgClosure_of_isAdjoinRoot_i (R : Type u) [Field R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] (hK : IsAdjoinRootMonic' K (Polynomial.X ^ 2 + 1)) :

IsAlgClosure R K

theorem IsRealClosed.isAlgClosure_of_finrank_ne_one (R : Type u) [Field R] [IsRealClosed R] {K : Type u_1} [Field K] [Algebra R K] [Algebra.IsAlgebraic R K] (hK : Module.finrank R K ≠ 1) :

IsAlgClosure R K

theorem IsRealClosed.irred_poly_classify {R : Type u} [Field R] [IsRealClosed R] {f : Polynomial R} (hf : f.Monic) :

Irreducible f ↔ f.natDegree = 1 ∨ ∃ (a : R) (b : R), b ≠ 0 ∧ f = (Polynomial.X - Polynomial.C a) ^ 2 + Polynomial.C b ^ 2

theorem IsRealClosed.irred_poly_natDegree {R : Type u} [Field R] [IsRealClosed R] {f : Polynomial R} (hf : Irreducible f) :

f.natDegree ≤ 2

noncomputable def IsRealClosed.unique_isStrictOrderedRing (R : Type u) [Field R] [IsRealClosed R] :

Unique { l : LinearOrder R // IsStrictOrderedRing R }

Equations

IsRealClosed.unique_isStrictOrderedRing R = IsSemireal.unique_isStrictOrderedRing ⋯

Instances For

theorem IsRealClosed.nonneg_iff_isSquare {R : Type u} [Field R] [IsRealClosed R] [LinearOrder R] [IsStrictOrderedRing R] {x : R} :

0 ≤ x ↔ IsSquare x

theorem IsRealClosed.isSquare_of_nonneg {R : Type u} [Field R] [IsRealClosed R] [LinearOrder R] [IsStrictOrderedRing R] {x : R} :

0 ≤ x → IsSquare x

Alias of the forward direction of IsRealClosed.nonneg_iff_isSquare.

theorem IsRealClosed.exists_eq_pow_of_nonneg {R : Type u} [Field R] [IsRealClosed R] [LinearOrder R] [IsStrictOrderedRing R] {x : R} (hx : 0 ≤ x) {n : ℕ} (hn : n > 0) :

∃ (r : R), x = r ^ n

theorem IsRealClosed.intermediate_value_property {R : Type u} [Field R] [IsRealClosed R] [LinearOrder R] [IsStrictOrderedRing R] {f : Polynomial R} {x y : R} (hle : x ≤ y) (hx : 0 ≤ Polynomial.eval x f) (hy : Polynomial.eval y f ≤ 0) :

∃ z ∈ Set.Icc x y, Polynomial.eval z f = 0

theorem IsRealClosed.TFAE (R : Type u) [Field R] :

[IsRealClosed R, IsAdjoinRootMonic' (AlgebraicClosure R) (Polynomial.X ^ 2 + 1), IsSemireal R ∧ ∀ (K : Type u) [inst : Field K] [IsSemireal K] [inst_2 : Algebra R K] [Algebra.IsAlgebraic R K], Module.finrank R K = 1].TFAE

theorem IsRealClosed.TFAE_linearOrderedField (R : Type u) [Field R] [LinearOrder R] [IsStrictOrderedRing R] :

[IsRealClosed R, ∀ (K : Type u) [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : Algebra R K] [Algebra.IsAlgebraic R K] [IsOrderedModule R K], Module.finrank R K = 1, ∀ {f : Polynomial R} {x y : R}, x ≤ y → 0 ≤ Polynomial.eval x f → Polynomial.eval y f ≤ 0 → ∃ z ∈ Set.Icc x y, Polynomial.eval z f = 0].TFAE

theorem weak_Artin_Schreier {R : Type u_1} [Field R] (hR_char : ringChar R ≠ 2) (hR : Module.finrank R (AlgebraicClosure R) = 2) :

theorem Artin_Schreier {R : Type u_1} [Field R] (hR : FiniteDimensional R (AlgebraicClosure R)) :