noncomputable def Field.isOrderingOrderedAlgebraEquiv (F : Type u_1) (K : Type u_2) [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Field K] [Algebra F K] : { O : Subsemiring K // O.IsOrdering ∧ Subsemiring.map (algebraMap F K) (Subsemiring.nonneg F) ≤ O } ≃ { _l : LinearOrder K // IsStrictOrderedRing K ∧ IsOrderedModule F K }

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Field.isOrderingOrderedAlgebraEquiv_apply_coe {F : Type u_1} {K : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Field K] [Algebra F K] (O : Subsemiring K) (hO : O.IsOrdering) (hO₂ : Subsemiring.map (algebraMap F K) (Subsemiring.nonneg F) ≤ O) : ↑((isOrderingOrderedAlgebraEquiv F K) ⟨O, ⋯⟩) = ↑((isOrderingLinearOrderEquiv K) ⟨O, hO⟩)

@[simp]

theorem Field.isOrderingOrderedAlgebraEquiv_symm_apply_coe {F : Type u_1} {K : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Field K] [Algebra F K] (l : LinearOrder K) (hl : IsStrictOrderedRing K) (hl₂ : IsOrderedModule F K) : ↑((isOrderingOrderedAlgebraEquiv F K).symm ⟨l, ⋯⟩) = ↑((isOrderingLinearOrderEquiv K).symm ⟨l, hl⟩)

theorem Field.exists_isOrderedAlgebra_iff_neg_one_notMem_sup {F : Type u_1} {K : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Field K] [Algebra F K] : (∃ (x : LinearOrder K), IsStrictOrderedRing K ∧ IsOrderedModule F K) ↔ -1 ∉ Subsemiring.map (algebraMap F K) (Subsemiring.nonneg F) ⊔ Subsemiring.sumSq K

theorem sup_map_nonneg_sumSq_eq_addSubmonoid_closure_set_mul {F : Type u_1} {K : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Field K] [Algebra F K] : ↑(Subsemiring.map (algebraMap F K) (Subsemiring.nonneg F) ⊔ Subsemiring.sumSq K) = ↑(Submodule.span ↥(Subsemiring.nonneg F) {x : K | IsSquare x})

theorem Field.exists_isOrderedAlgebra_iff_neg_one_notMem_span_nonneg_isSquare {F : Type u_1} {K : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Field K] [Algebra F K] : (∃ (x : LinearOrder K), IsStrictOrderedRing K ∧ IsOrderedModule F K) ↔ -1 ∉ Submodule.span ↥(Subsemiring.nonneg F) {x : K | IsSquare x}

theorem Field.exists_isOrderedAlgebra_of_projection {F : Type u_1} {K : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Field K] [Algebra F K] (π : K →ₗ[F] F) (hπ : ∀ (x : K), x ≠ 0 → 0 < π (x * x)) : ∃ (x : LinearOrder K), IsStrictOrderedRing K ∧ IsOrderedModule F K

theorem adj_sqrt_ordered {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {a : F} (ha : 0 ≤ a) (ha₂ : ¬IsSquare a) : ∃ (x : LinearOrder (AdjoinRoot (Polynomial.X ^ 2 - Polynomial.C a))), IsStrictOrderedRing (AdjoinRoot (Polynomial.X ^ 2 - Polynomial.C a)) ∧ IsOrderedModule F (AdjoinRoot (Polynomial.X ^ 2 - Polynomial.C a))

theorem lift_poly_span_nonneg_isSquare {F : Type u_1} {K : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Field K] [Algebra F K] {f : Polynomial F} {r : K} (hAdj : IsIntegralUniqueGen r f) {x : K} (hx : x ∈ Submodule.span ↥(Subsemiring.nonneg F) {x : K | IsSquare x}) : ∃ (g : Polynomial F), (Polynomial.aeval r) g = x ∧ g ∈ Submodule.span (↥(Subsemiring.nonneg F)) ((fun (x : Polynomial F) => x * x) '' {g : Polynomial F | g.natDegree < f.natDegree})

theorem minus_one_notMem_span_nonneg_isSquare_mod_f {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {f : Polynomial F} (hf₁ : f.Monic) (hf₂ : Irreducible f) (hf₃ : Odd f.natDegree) {g : Polynomial F} (hg : g ∈ Submodule.span (↥(Subsemiring.nonneg F)) ((fun (x : Polynomial F) => x * x) '' {g : Polynomial F | g.natDegree < f.natDegree})) : ¬f ∣ g + 1

theorem odd_deg_ordered {F : Type u_1} {K : Type u_2} [Field F] [LinearOrder F] [IsStrictOrderedRing F] [Field K] [Algebra F K] (h_rank : Odd (Module.finrank F K)) : ∃ (x : LinearOrder K), IsStrictOrderedRing K ∧ IsOrderedModule F K