We prove basic properties of orderings on rings, and show that they are preserved under certain operations.
References #
- An introduction to real algebra, by T.Y. Lam. Rocky Mountain J. Math. 14(4): 767-814 (1984). lam_1984
theorem
Subsemiring.IsPreordering.of_le
{R : Type u_1}
[CommRing R]
{P : Subsemiring R}
[P.IsPreordering]
{Q : Subsemiring R}
(hPQ : P ≤ Q)
(hQ : -1 ∉ Q)
:
theorem
Subsemiring.IsPreordering.unitsInv_mem
{R : Type u_1}
[CommRing R]
{P : Subsemiring R}
[P.IsPreordering]
{a : Rˣ}
(ha : ↑a ∈ P)
:
theorem
Subsemiring.IsPreordering.one_notMem_supportAddSubgroup
{R : Type u_1}
[CommRing R]
(P : Subsemiring R)
[P.IsPreordering]
:
theorem
Subsemiring.IsPreordering.one_notMem_support
{R : Type u_1}
[CommRing R]
(P : Subsemiring R)
[P.IsPreordering]
[P.toAddSubmonoid.HasIdealSupport]
:
1 ∉ P.toAddSubmonoid.support
theorem
Subsemiring.IsPreordering.supportAddSubgroup_ne_top
{R : Type u_1}
[CommRing R]
(P : Subsemiring R)
[P.IsPreordering]
:
theorem
Subsemiring.IsPreordering.support_ne_top
{R : Type u_1}
[CommRing R]
(P : Subsemiring R)
[P.IsPreordering]
[P.toAddSubmonoid.HasIdealSupport]
:
theorem
Subsemiring.IsPreordering.isOrdering_iff
{R : Type u_1}
[CommRing R]
{P : Subsemiring R}
[P.IsPreordering]
:
theorem
Subsemiring.IsPreordering.hasIdealSupport_of_isUnit_two
{R : Type u_1}
[CommRing R]
(P : Subsemiring R)
[P.IsPreordering]
(h : IsUnit 2)
:
instance
Subsemiring.IsPreordering.instHasIdealSupportToAddSubmonoidOfFactIsUnitOfNat
{R : Type u_1}
[CommRing R]
(P : Subsemiring R)
[P.IsPreordering]
[h : Fact (IsUnit 2)]
:
instance
Subsemiring.instIsPreorderingOfNontrivialOfHasMemOrNegMemOfIsConeToAddSubmonoid
{R : Type u_1}
[CommRing R]
(P : Subsemiring R)
[Nontrivial R]
[P.toAddSubmonoid.HasMemOrNegMem]
[P.toAddSubmonoid.IsCone]
:
instance
Subsemiring.instIsOrderingOfIsDomainOfHasMemOrNegMemOfIsConeToAddSubmonoid
{R : Type u_1}
[CommRing R]
(P : Subsemiring R)
[IsDomain R]
[P.toAddSubmonoid.HasMemOrNegMem]
[P.toAddSubmonoid.IsCone]
:
theorem
Subsemiring.IsPreordering.ofIsCone
{R : Type u_1}
[CommRing R]
(P : Subsemiring R)
[Nontrivial R]
[P.toAddSubmonoid.IsCone]
(h : sumSq R ≤ P)
:
instance
Subsemiring.instIsPreorderingMin
{R : Type u_1}
[CommRing R]
(P₁ P₂ : Subsemiring R)
[P₁.IsPreordering]
[P₂.IsPreordering]
:
(P₁ ⊓ P₂).IsPreordering
theorem
Subsemiring.IsPreordering.sInf
{R : Type u_1}
[CommRing R]
{S : Set (Subsemiring R)}
(hSn : S.Nonempty)
(hS : ∀ s ∈ S, s.IsPreordering)
:
theorem
Subsemiring.IsPreordering.sSup
{R : Type u_1}
[CommRing R]
{S : Set (Subsemiring R)}
(hSn : S.Nonempty)
(hSd : DirectedOn (fun (x1 x2 : Subsemiring R) => x1 ≤ x2) S)
(hS : ∀ s ∈ S, s.IsPreordering)
:
instance
Subsemiring.instIsOrderingComap
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
(P' : Subsemiring S)
[P'.IsOrdering]
:
(comap f P').IsOrdering
instance
Subsemiring.instIsPreorderingComap
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
(P' : Subsemiring S)
[P'.IsPreordering]
:
(comap f P').IsPreordering
theorem
Subsemiring.IsOrdering.map
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
{f : R →+* S}
{P : Subsemiring R}
[P.IsOrdering]
(hf : Function.Surjective ⇑f)
(hsupp : RingHom.ker f ≤ P.toAddSubmonoid.support)
:
(Subsemiring.map f P).IsOrdering
theorem
Subsemiring.IsPreordering.map
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
{f : R →+* S}
{P : Subsemiring R}
[P.IsPreordering]
(hf : Function.Surjective ⇑f)
(hsupp : f.toAddMonoidHom.ker ≤ P.toAddSubmonoid.supportAddSubgroup)
:
(Subsemiring.map f P).IsPreordering
theorem
Subsemiring.IsPreordering.inv_mem
{F : Type u_1}
[Field F]
{P : Subsemiring F}
[P.IsPreordering]
{a : F}
(ha : a ∈ P)
:
instance
Subsemiring.IsPreordering.instIsConeToAddSubmonoid
{F : Type u_1}
[Field F]
(P : Subsemiring F)
[P.IsPreordering]
:
instance
Subsemiring.IsPreordering.instIsPrimeSupportToAddSubmonoid
{F : Type u_1}
[Field F]
(P : Subsemiring F)
[P.IsPreordering]
: