noncomputable def
Field.ringOrderingOrderedAlgebraEquiv
(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.
Instances For
@[simp]
theorem
Field.ringOrderingOrderedAlgebraEquiv_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)
:
@[simp]
theorem
Field.ringOrderingOrderedAlgebraEquiv_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)
:
↑((ringOrderingOrderedAlgebraEquiv F K).symm ⟨l, ⋯⟩) = ↑((ringOrderingLinearOrderEquiv 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
isSumSq_of_isSquare
{K : Type u_3}
{L : Type u_4}
[Field K]
[Field L]
[Algebra K L]
(hL : IsAdjoinRootMonic' L (Polynomial.X ^ 2 + 1))
(h : ∀ (x : L), IsSquare x)
(a : K)
(ha : IsSumSq a)
:
IsSquare a
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}))
:
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