From 8b3c961bc8bf321340274e5929cb8f5a3dda7aab Mon Sep 17 00:00:00 2001 From: FM22 Date: Fri, 20 Dec 2024 21:17:40 +0000 Subject: [PATCH] join up to cones --- .../Mathlib/Algebra/Order/Ring/Cone.lean | 48 +++++++- .../RealClosedField/RingOrdering/Basic.lean | 115 ++++++++++++------ .../RealClosedField/RingOrdering/Defns.lean | 61 ++++++---- .../RealClosedField/Semireal.Field.lean | 7 +- 4 files changed, 161 insertions(+), 70 deletions(-) diff --git a/RealClosedField/Mathlib/Algebra/Order/Ring/Cone.lean b/RealClosedField/Mathlib/Algebra/Order/Ring/Cone.lean index 7e70c25..adf16d7 100644 --- a/RealClosedField/Mathlib/Algebra/Order/Ring/Cone.lean +++ b/RealClosedField/Mathlib/Algebra/Order/Ring/Cone.lean @@ -7,6 +7,7 @@ import Mathlib.Algebra.Order.Group.Cone import Mathlib.Algebra.Order.Ring.Basic import Mathlib.Algebra.Ring.Subsemiring.Order import RealClosedField.RealClosedField.RingOrdering.Basic +import Mathlib.RingTheory.Ideal.Quotient.Basic /-! # Construct ordered rings from rings with a specified positive cone. @@ -46,6 +47,14 @@ instance RingCone.instRingConeClass (R : Type*) [Ring R] : namespace RingCone +@[simp] +theorem mem_toSubsemiring (R : Type*) [Ring R] (C : RingCone R) {x : R} : + x ∈ C.toSubsemiring ↔ x ∈ C := Iff.rfl + +@[simp] +theorem coe_toSubsemiring (R : Type*) [Ring R] (C : RingCone R) : + (C.toSubsemiring : Set R) = C := rfl + variable {T : Type*} [OrderedRing T] {a : T} variable (T) in @@ -118,9 +127,42 @@ instance RingConeClass.instIsOrdering_of_isMaxCone {S R : Type*} [Nontrivial R] RingPreordering.IsOrdering C where mem_or_neg_mem' x := by obtain ⟨C, hC⟩ := C; exact mem_or_neg_mem C x -/- TODO : decide whether to keep this cursed subtype instance, or whether to change to a def. -/ +/- TODO : decide whether to keep the above cursed subtype instance, + or whether to change to a def. -/ + +@[reducible] def RingCone.mkOfRingPreordering {S R : Type*} + [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P : S} + (hP : RingPreordering.AddSubgroup.support P = ⊥) : RingCone R where + __ := (RingPreorderingClass.toRingPreordering P).toSubsemiring + eq_zero_of_mem_of_neg_mem' {a} := by + have : ∀ x, x ∈ RingPreordering.AddSubgroup.support P → x ∈ (⊥ : AddSubgroup R) := by simp_all + rcases hP with - + aesop + /- TODO : make this proof less awful -/ + +instance RingCone.mkOfRingPreordering.inst_isMaxCone {S R : Type*} + [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P : S} [RingPreordering.IsOrdering P] + (hP : RingPreordering.AddSubgroup.support P = ⊥) : IsMaxCone <| mkOfRingPreordering hP where + mem_or_neg_mem' := RingPreordering.mem_or_neg_mem P + +@[reducible] def LinearOrderedRing.mkOfRingOrdering {S R : Type*} [CommRing R] [IsDomain R] + [SetLike S R] [RingPreorderingClass S R] {P : S} [RingPreordering.IsOrdering P] + [DecidablePred (· ∈ P)] + (hP : RingPreordering.AddSubgroup.support P = ⊥) : LinearOrderedRing R := + have : DecidablePred (· ∈ RingCone.mkOfRingPreordering hP) := by assumption + mkOfCone <| RingCone.mkOfRingPreordering hP + +@[reducible] def RingCone.mkOfRingPreordering_field {S F : Type*} + [Field F] [SetLike S F] [RingPreorderingClass S F] (P : S) : RingCone F := + mkOfRingPreordering <| RingPreordering.support_eq_bot P + +variable {S R : Type*} [CommRing R] (I : Ideal R) + +#check Ideal.Quotient.one + +@[reducible] def RingCone.mkOfRingPoreordering_quot {S R : Type*} + [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P : S} [RingPreordering.IsOrdering P] : + RingCone (R ⧸ (RingPreordering.Ideal.support P)) -/- TODO: prime orderings with support {0} are maximal cones; - deduce prime orderings on fields are maximal cones -/ /- TODO: orderings with support I induce maximal ring cones on R/I -/ /- TODO: ordering on an ID <-> ordering on its fraction field -/ diff --git a/RealClosedField/RealClosedField/RingOrdering/Basic.lean b/RealClosedField/RealClosedField/RingOrdering/Basic.lean index b47a04a..4bf36c2 100644 --- a/RealClosedField/RealClosedField/RingOrdering/Basic.lean +++ b/RealClosedField/RealClosedField/RingOrdering/Basic.lean @@ -60,20 +60,38 @@ theorem nonempty_chain_bddAbove {R : Type*} [CommRing R] (by simpa using (hc.some.square_mem' x))) (by have a : ∀ x ∈ (toSubsemiring '' c), -1 ∉ x := fun P' hP' => by - obtain ⟨P, _, rfl⟩ := (by aesop : ∃ x ∈ c, x.toSubsemiring = P') + obtain ⟨P, _, rfl⟩ := show ∃ x ∈ c, x.toSubsemiring = P' by simp_all simpa using P.minus_one_not_mem' simp_all [Subsemiring.coe_sSup_of_directedOn (by simp [hc]) (IsChain.directedOn (IsChain.image _ _ _ (by aesop) hcc))]), fun _ _ => by simpa using CompleteLattice.le_sSup (toSubsemiring '' c) _ (by aesop)⟩ +variable (P) in +theorem AddSubgroup.one_not_mem_support : 1 ∉ support P := by + aesop (add unsafe forward (minus_one_not_mem P)) + +variable (P) in +theorem AddSubgroup.support_neq_top : support P ≠ ⊤ := fun eq => by + have : 1 ∉ (⊤ : AddSubgroup R) := by rw[← eq]; exact one_not_mem_support P + simp_all + +variable (P) in +theorem Ideal.one_not_mem_support [HasIdealSupport P] : 1 ∉ support P := + AddSubgroup.one_not_mem_support P + +variable (P) in +theorem Ideal.support_neq_top [HasIdealSupport P] : support P ≠ ⊤ := fun eq => by + have : 1 ∉ (⊤ : Ideal R) := by rw[← eq]; exact one_not_mem_support P + simp_all + namespace HasIdealSupport -theorem smul_mem [RingPreordering.HasIdealSupport P] +theorem smul_mem [HasIdealSupport P] (x : R) {a : R} (h₁a : a ∈ P) (h₂a : -a ∈ P) : x * a ∈ P := by have := smul_mem_support P simp_all -theorem neg_smul_mem [RingPreordering.HasIdealSupport P] +theorem neg_smul_mem [HasIdealSupport P] (x : R) {a : R} (h₁a : a ∈ P) (h₂a : -a ∈ P) : -(x * a) ∈ P := by have := smul_mem_support P simp_all @@ -90,7 +108,30 @@ theorem hasIdealSupport_of_isUnit_2 (isUnit_2 : IsUnit (2 : R)) : HasIdealSuppor ring_nf at mem ⊢ assumption -/- TODO: support always 0 in a field (elementary approach) -/ +theorem support_eq_bot {S F : Type*} [Field F] [SetLike S F] [RingPreorderingClass S F] (P : S) : + AddSubgroup.support P = ⊥ := by + refine AddSubgroup.ext (fun x => Iff.intro (fun h => ?_) (fun h => by aesop)) + by_contra hz + apply minus_one_not_mem P + rw [show -1 = x * (-x)⁻¹ by field_simp [show x ≠ 0 by simp_all]] + aesop + +theorem support_eq_bot' {S F : Type*} [Field F] [SetLike S F] [RingPreorderingClass S F] (P : S) : + AddSubgroup.support P = ⊥ := by + rcases em <| (2 : F) = 0 with eq | neq + · refine False.elim <| minus_one_not_mem P ?_ + rw [show (-1 : F) = 1 by linear_combination -eq] + apply one_mem + · apply AddSubgroup.ext + have : HasIdealSupport P := hasIdealSupport_of_isUnit_2 (by aesop) + have h : Ideal.support P = ⊥ := by + aesop (add unsafe forward (eq_bot_or_eq_top (Ideal.support P)), + unsafe forward (Ideal.support_neq_top P)) + have : ∀ x, x ∈ Ideal.support P ↔ x ∈ (⊥ : Ideal F) := by simp_all + rcases h with - + simp_all + +/- TODO : decide which proof to use -/ /-! ## (Prime) orderings @@ -118,13 +159,13 @@ instance IsOrdering.hasIdealSupport : HasIdealSupport P where end IsOrdering -instance preordering_support_isPrime [IsPrimeOrdering P] : - (Ideal.preordering_support P).IsPrime where - ne_top' h := minus_one_not_mem P (by aesop : 1 ∈ Ideal.preordering_support P).2 +instance support_isPrime [IsPrimeOrdering P] : + (Ideal.support P).IsPrime where + ne_top' h := minus_one_not_mem P (by aesop : 1 ∈ Ideal.support P).2 mem_or_mem' := IsPrimeOrdering.mem_or_mem' instance isPrimeOrdering_of_isOrdering - [IsOrdering P] [(Ideal.preordering_support P).IsPrime] : IsPrimeOrdering P where + [IsOrdering P] [(Ideal.support P).IsPrime] : IsPrimeOrdering P where mem_or_neg_mem' := mem_or_neg_mem P mem_or_mem' := Ideal.IsPrime.mem_or_mem (by assumption) @@ -133,7 +174,7 @@ theorem isPrimeOrdering_iff : refine Iff.intro (fun prime a b h₁ => ?_) (fun h => ?_) · by_contra h₂ have : a * b ∈ P := by simpa using mul_mem (by aesop : -a ∈ P) (by aesop : -b ∈ P) - have : a ∈ Ideal.preordering_support P ∨ b ∈ Ideal.preordering_support P := + have : a ∈ Ideal.support P ∨ b ∈ Ideal.support P := Ideal.IsPrime.mem_or_mem inferInstance (by simp_all) simp_all · refine ⟨by aesop, fun {x y} hxy => ?_⟩ @@ -173,12 +214,12 @@ instance comap.instIsOrdering (P : RingPreordering B) [IsOrdering P] (f : A →+ @[simp] theorem mem_comap_support {P : RingPreordering B} {f : A →+* B} {x : A} : - x ∈ AddSubgroup.preordering_support (P.comap f) ↔ f x ∈ AddSubgroup.preordering_support P := + x ∈ AddSubgroup.support (P.comap f) ↔ f x ∈ AddSubgroup.support P := by simp @[simp] theorem comap_support {P : RingPreordering B} {f : A →+* B} : - AddSubgroup.preordering_support (P.comap f) = (AddSubgroup.preordering_support P).comap f := + AddSubgroup.support (P.comap f) = (AddSubgroup.support P).comap f := by ext; simp instance comap_hasIdealSupport (P : RingPreordering B) [HasIdealSupport P] (f : A →+* B) : @@ -187,17 +228,17 @@ instance comap_hasIdealSupport (P : RingPreordering B) [HasIdealSupport P] (f : @[simp] theorem mem_comap_support' {P : RingPreordering B} [HasIdealSupport P] {f : A →+* B} {x : A} : - x ∈ Ideal.preordering_support (P.comap f) ↔ f x ∈ Ideal.preordering_support P := by simp + x ∈ Ideal.support (P.comap f) ↔ f x ∈ Ideal.support P := by simp @[simp] theorem comap_support' {P : RingPreordering B} [HasIdealSupport P] {f : A →+* B} : - Ideal.preordering_support (P.comap f) = (Ideal.preordering_support P).comap f := + Ideal.support (P.comap f) = (Ideal.support P).comap f := by ext; simp /-- The preimage of a prime ordering along a ring homomorphism is a prime ordering. -/ instance comap.instIsPrimeOrdering (P : RingPreordering B) [IsPrimeOrdering P] (f : A →+* B) : IsPrimeOrdering (comap f P) := by - have : (Ideal.preordering_support (P.comap f)).IsPrime := by rw [comap_support']; infer_instance + have : (Ideal.support (P.comap f)).IsPrime := by rw [comap_support']; infer_instance infer_instance /-! ## map -/ @@ -205,7 +246,7 @@ instance comap.instIsPrimeOrdering (P : RingPreordering B) [IsPrimeOrdering P] ( /-- The image of a preordering `P` along a surjective ring homomorphism with kernel contained in the support of `P` is a preordering. -/ def map {f : A →+* B} {P : RingPreordering A} (hf : Function.Surjective f) - (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P) : RingPreordering B where + (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) : RingPreordering B where __ := P.toSubsemiring.map f square_mem' x := by obtain ⟨x', rfl⟩ := hf x @@ -218,43 +259,43 @@ def map {f : A →+* B} {P : RingPreordering A} (hf : Function.Surjective f) @[simp] theorem coe_map {f : A →+* B} {P : RingPreordering A} (hf : Function.Surjective f) - (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P) : + (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) : (map hf hsupp : Set B) = f '' P := rfl @[simp] theorem mem_map {f : A →+* B} {P : RingPreordering A} (hf : Function.Surjective f) - (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P) : + (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) : y ∈ map hf hsupp ↔ ∃ x ∈ P, f x = y := Iff.rfl /-- The image of an ordering `P` along a surjective ring homomorphism with kernel contained in the support of `P` is an ordering. -/ instance map.instIsOrdering {f : A →+* B} {P : RingPreordering A} [IsOrdering P] (hf : Function.Surjective f) - (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P) : + (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) : IsOrdering (map hf hsupp) where mem_or_neg_mem' x := by obtain ⟨x', rfl⟩ := hf x have := mem_or_neg_mem P x' aesop -@[simp] +@[simp↓] theorem mem_map_support {f : A →+* B} {P : RingPreordering A} {hf : Function.Surjective f} - {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P} {x : B} : - x ∈ AddSubgroup.preordering_support (map hf hsupp) ↔ - ∃ y ∈ AddSubgroup.preordering_support P, f y = x := by + {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P} {x : B} : + x ∈ AddSubgroup.support (map hf hsupp) ↔ + ∃ y ∈ AddSubgroup.support P, f y = x := by refine Iff.intro (fun ⟨⟨a, ⟨ha₁, ha₂⟩⟩, ⟨b, ⟨hb₁, hb₂⟩⟩⟩ => ?_) (by aesop) have : -(a + b) + b ∈ P := by exact add_mem (hsupp (show f (a + b) = 0 by simp_all)).2 hb₁ aesop @[simp] theorem map_support {f : A →+* B} {P : RingPreordering A} {hf : Function.Surjective f} - {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P} : - AddSubgroup.preordering_support (map hf hsupp) = (AddSubgroup.preordering_support P).map f := - by ext; rw [mem_map_support]; simp + {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P} : + AddSubgroup.support (map hf hsupp) = (AddSubgroup.support P).map f := by + ext; simp instance map_hasIdealSupport {f : A →+* B} {P : RingPreordering A} [HasIdealSupport P] (hf : Function.Surjective f) - (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P) : + (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) : HasIdealSupport (map hf hsupp) where smul_mem_support' x a ha := by rw [mem_map_support] at ha @@ -263,30 +304,30 @@ instance map_hasIdealSupport {f : A →+* B} {P : RingPreordering A} [HasIdealSu have := smul_mem_support P x' ha' aesop -@[simp] +@[simp↓] theorem mem_map_support' {f : A →+* B} {P : RingPreordering A} [HasIdealSupport P] {hf : Function.Surjective f} - {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P} {x : B} : - x ∈ Ideal.preordering_support (map hf hsupp) ↔ - ∃ y ∈ Ideal.preordering_support P, f y = x := by simp [Ideal.preordering_support] + {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P} {x : B} : + x ∈ Ideal.support (map hf hsupp) ↔ + ∃ y ∈ Ideal.support P, f y = x := by simp [Ideal.support] @[simp] theorem map_support' {f : A →+* B} {P : RingPreordering A} [HasIdealSupport P] {hf : Function.Surjective f} - {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P} : - Ideal.preordering_support (map hf hsupp) = (Ideal.preordering_support P).map f := by - ext; rw [mem_map_support']; refine Iff.intro (fun h => ?_) (fun h => ?_) - · rcases h with ⟨x', hx', rfl⟩; exact Ideal.mem_map_of_mem f hx' - · exact Ideal.mem_image_of_mem_map_of_surjective f hf h + {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P} : + Ideal.support (map hf hsupp) = (Ideal.support P).map f := by + ext; simp [Ideal.mem_map_iff_of_surjective f hf] /-- The image of a prime ordering `P` along a surjective ring homomorphism with kernel contained in the support of `P` is a prime ordering. -/ instance map.instIsPrimeOrdering {f : A →+* B} {P : RingPreordering A} [IsPrimeOrdering P] (hf : Function.Surjective f) - (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P) : + (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) : IsPrimeOrdering (map hf hsupp) := by - have : (Ideal.preordering_support (map hf hsupp)).IsPrime := by + have : (Ideal.support (map hf hsupp)).IsPrime := by simpa using Ideal.map_isPrime_of_surjective hf (by simpa using hsupp) infer_instance end RingPreordering + +/- TODO : specialise to quotient map R ->> R/supp(P) -/ diff --git a/RealClosedField/RealClosedField/RingOrdering/Defns.lean b/RealClosedField/RealClosedField/RingOrdering/Defns.lean index 856386e..ec2d897 100644 --- a/RealClosedField/RealClosedField/RingOrdering/Defns.lean +++ b/RealClosedField/RealClosedField/RingOrdering/Defns.lean @@ -11,7 +11,7 @@ import Mathlib.RingTheory.Ideal.Basic ## Preorderings -/ -section Preordering +section defns variable (S R : Type*) [CommRing R] [SetLike S R] @@ -43,6 +43,14 @@ instance RingPreordering.instRingPreorderingClass : RingPreorderingClass (RingPr square_mem {P} := P.square_mem' minus_one_not_mem {P} := P.minus_one_not_mem' +@[simp] +theorem RingPreordering.mem_toSubsemiring {P : RingPreordering R} {x : R} : + x ∈ P.toSubsemiring ↔ x ∈ P := Iff.rfl + +@[simp] +theorem RingPreordering.coe_toSubsemiring {P : RingPreordering R} : + (P.toSubsemiring : Set R) = P := rfl + variable {S R : Type*} [CommRing R] [SetLike S R] [RingPreorderingClass S R] (P : S) def RingPreorderingClass.toRingPreordering : RingPreordering R where @@ -55,10 +63,15 @@ def RingPreorderingClass.toRingPreordering : RingPreordering R where minus_one_not_mem' := minus_one_not_mem P @[simp] -lemma RingPreorderingClass.coe_toRingPreordering : (toRingPreordering P : Set R) = P := by +lemma RingPreorderingClass.mem_toRingPreordering {x : R} : + x ∈ (toRingPreordering P : Set R) ↔ x ∈ P := by rw [toRingPreordering]; aesop -end Preordering +@[simp] +lemma RingPreorderingClass.coe_toRingPreordering : (toRingPreordering P : Set R) = P := by + rw [toRingPreordering]; rfl + +end defns variable {S R : Type*} [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P : S} @@ -66,59 +79,55 @@ variable {S R : Type*} [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P ## Support -/ -namespace AddSubgroup +namespace RingPreordering.AddSubgroup variable (P) in /-- The support of a ring preordering `P` in a commutative ring `R` is the set of elements `x` in `R` such that both `x` and `-x` lie in `P`. -/ -def preordering_support : AddSubgroup R where +def support : AddSubgroup R where carrier := {x : R | x ∈ P ∧ -x ∈ P} zero_mem' := by aesop add_mem' := by aesop neg_mem' := by aesop -@[simp] lemma mem_support : x ∈ preordering_support P ↔ x ∈ P ∧ -x ∈ P := Iff.rfl -@[simp, norm_cast] lemma coe_support : preordering_support P = {x : R | x ∈ P ∧ -x ∈ P} := rfl +@[simp] lemma mem_support : x ∈ support P ↔ x ∈ P ∧ -x ∈ P := Iff.rfl +@[simp, norm_cast] lemma coe_support : support P = {x : R | x ∈ P ∧ -x ∈ P} := rfl end AddSubgroup -namespace RingPreordering - variable (P) in class HasIdealSupport : Prop where - smul_mem_support' (x : R) {a : R} (ha : a ∈ AddSubgroup.preordering_support P) : - x * a ∈ AddSubgroup.preordering_support P + smul_mem_support' (x : R) {a : R} (ha : a ∈ AddSubgroup.support P) : + x * a ∈ AddSubgroup.support P variable (P) in /-- Technical lemma to get P as explicit argument -/ -lemma smul_mem_support [RingPreordering.HasIdealSupport P] : - ∀ (x : R) {a : R}, a ∈ AddSubgroup.preordering_support P → - x * a ∈ AddSubgroup.preordering_support P := +lemma smul_mem_support [HasIdealSupport P] : + ∀ (x : R) {a : R}, a ∈ AddSubgroup.support P → + x * a ∈ AddSubgroup.support P := HasIdealSupport.smul_mem_support' (P := P) theorem hasIdealSupport (h : ∀ x a : R, a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P) : HasIdealSupport P where smul_mem_support' := by simp_all -end RingPreordering - namespace Ideal -variable [RingPreordering.HasIdealSupport P] +variable [HasIdealSupport P] variable (P) in /-- The support of a ring preordering `P` in a commutative ring `R` is the set of elements `x` in `R` such that both `x` and `-x` lie in `P`. -/ -def preordering_support : Ideal R where - __ := AddSubgroup.preordering_support P - smul_mem' := by simpa using RingPreordering.smul_mem_support P +def support : Ideal R where + __ := AddSubgroup.support P + smul_mem' := by simpa using smul_mem_support P -@[simp] lemma mem_support : x ∈ preordering_support P ↔ x ∈ P ∧ -x ∈ P := Iff.rfl -@[simp, norm_cast] lemma coe_support : preordering_support P = {x : R | x ∈ P ∧ -x ∈ P} := rfl +@[simp] lemma mem_support : x ∈ support P ↔ x ∈ P ∧ -x ∈ P := Iff.rfl +@[simp, norm_cast] lemma coe_support : support P = {x : R | x ∈ P ∧ -x ∈ P} := rfl end Ideal @@ -126,8 +135,6 @@ end Ideal ## (Prime) orderings -/ -namespace RingPreordering - section IsOrdering variable (P) in @@ -148,9 +155,11 @@ variable (P) in /-- A prime ordering `P` on a ring `R` is an ordering whose support is a prime ideal. -/ class IsPrimeOrdering : Prop where mem_or_neg_mem' (x : R) : x ∈ P ∨ -x ∈ P - mem_or_mem' {x y : R} (h : x * y ∈ AddSubgroup.preordering_support P) : - x ∈ AddSubgroup.preordering_support P ∨ y ∈ AddSubgroup.preordering_support P + mem_or_mem' {x y : R} (h : x * y ∈ AddSubgroup.support P) : + x ∈ AddSubgroup.support P ∨ y ∈ AddSubgroup.support P instance isOrdering [IsPrimeOrdering P] : IsOrdering P where mem_or_neg_mem' := IsPrimeOrdering.mem_or_neg_mem' + +end RingPreordering diff --git a/RealClosedField/RealClosedField/Semireal.Field.lean b/RealClosedField/RealClosedField/Semireal.Field.lean index b040d38..a619d4d 100644 --- a/RealClosedField/RealClosedField/Semireal.Field.lean +++ b/RealClosedField/RealClosedField/Semireal.Field.lean @@ -33,7 +33,6 @@ noncomputable def LinearOrderedField.mkOfIsSemireal [IsSemireal F] : LinearOrder theorem ArtinSchreier_basic : Nonempty ({S : LinearOrderedField F // S.toField = ‹Field F›}) ↔ IsSemireal F := by - refine Iff.intro (fun h => ?_) (fun h => ?_) - · rcases Classical.choice h with ⟨inst, rfl⟩ - infer_instance - · exact Nonempty.intro ⟨LinearOrderedField.mkOfIsSemireal F, rfl⟩ + refine Iff.intro (fun h => ?_) (fun _ => Nonempty.intro ⟨LinearOrderedField.mkOfIsSemireal F, rfl⟩) + rcases Classical.choice h with ⟨inst, rfl⟩ + infer_instance