Construct ordered rings from rings with a specified positive cone.

We demonstrate the equivalence between order structures on a ring R and positive cones: subsemirings S of R such that S ∩ -S = 0.

theorem Subsemiring.IsPointed.nonneg (R : Type u_1) [Ring R] [PartialOrder R] [IsOrderedRing R] : (nonneg R).toAddSubmonoid.IsPointed

theorem Subsemiring.IsSpanning.nonneg (R : Type u_1) [Ring R] [LinearOrder R] [IsOrderedRing R] : (nonneg R).toAddSubmonoid.IsSpanning

theorem IsOrderedRing.ofSubsemiring {R : Type u_1} [Ring R] {S : Subsemiring R} (hS : S.toAddSubmonoid.IsPointed) : IsOrderedRing R

@[deprecated AddSubmonoid.IsPointed (since := "2026-10-28")]

class RingConeClass (S : Type u_2) (R : outParam (Type u_3)) [Ring R] [SetLike S R] extends AddGroupConeClass S R, SubsemiringClass S R : Prop

RingConeClass S R says that S is a type of cones in R.

• add_mem {s : S} {a b : R} : a ∈ s → b ∈ s → a + b ∈ s
• zero_mem (s : S) : 0 ∈ s
• eq_zero_of_mem_of_neg_mem {C : S} {a : R} : a ∈ C → -a ∈ C → a = 0
• mul_mem {s : S} {a b : R} : a ∈ s → b ∈ s → a * b ∈ s
• one_mem (s : S) : 1 ∈ s

@[deprecated AddSubmonoid.IsPointed (since := "2026-10-28")]

structure RingCone (R : Type u_2) [Ring R] extends Subsemiring R, AddGroupCone R : Type u_2

A (positive) cone in a ring is a subsemiring that does not contain both a and -a for any nonzero a. This is equivalent to being the set of non-negative elements of some order making the ring into a partially ordered ring.

• carrier : Set R
• mul_mem' {a b : R} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• add_mem' {a b : R} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• eq_zero_of_mem_of_neg_mem' {a : R} : a ∈ self.carrier → -a ∈ self.carrier → a = 0

@[instance_reducible, deprecated "no replacement" (since := "2026-10-28")]

instance RingCone.instSetLike (R : Type u_2) [Ring R] : SetLike (RingCone R) R

Equations

• RingCone.instSetLike R = { coe := fun (C : RingCone R) => C.carrier, coe_injective := ⋯ }

@[instance_reducible, deprecated "no replacement" (since := "2026-10-28")]

instance instPartialOrderRingCone (R : Type u_2) [Ring R] : PartialOrder (RingCone R)

Equations

• instPartialOrderRingCone R = PartialOrder.ofSetLike (RingCone R)

@[deprecated "no replacement" (since := "2026-10-28")]

instance RingCone.instRingConeClass (R : Type u_2) [Ring R] : RingConeClass (RingCone R) R

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingCone.mem_mk {R : Type u_2} [Ring R] {toSubsemiring : Subsemiring R} (eq_zero_of_mem_of_neg_mem : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0) {x : R} : x ∈ { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem } ↔ x ∈ toSubsemiring

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingCone.coe_set_mk {R : Type u_2} [Ring R] {toSubsemiring : Subsemiring R} (eq_zero_of_mem_of_neg_mem : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0) : ↑{ toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem } = ↑toSubsemiring

@[deprecated Subsemiring.IsPointed.nonneg (since := "2026-10-28")]

def RingCone.nonneg (T : Type u_2) [Ring T] [PartialOrder T] [IsOrderedRing T] : RingCone T

Construct a cone from the set of non-negative elements of a partially ordered ring.

Equations

• RingCone.nonneg T = { toSubsemiring := Subsemiring.nonneg T, eq_zero_of_mem_of_neg_mem' := ⋯ }

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingCone.nonneg_toSubsemiring {T : Type u_2} [Ring T] [PartialOrder T] [IsOrderedRing T] : (nonneg T).toSubsemiring = Subsemiring.nonneg T

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingCone.nonneg_toAddGroupCone {T : Type u_2} [Ring T] [PartialOrder T] [IsOrderedRing T] : (nonneg T).toAddGroupCone = AddGroupCone.nonneg T

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingCone.mem_nonneg {T : Type u_2} [Ring T] [PartialOrder T] [IsOrderedRing T] {a : T} : a ∈ nonneg T ↔ 0 ≤ a

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingCone.coe_nonneg {T : Type u_2} [Ring T] [PartialOrder T] [IsOrderedRing T] : ↑(nonneg T) = {x : T | 0 ≤ x}

@[deprecated Subsemiring.IsSpanning.nonneg (since := "2026-10-28")]

instance RingCone.nonneg.hasMemOrNegMem {T : Type u_3} [Ring T] [LinearOrder T] [IsOrderedRing T] : HasMemOrNegMem (nonneg T)

@[deprecated IsOrderedRing.ofSubsemiring (since := "2026-10-28")]

theorem IsOrderedRing.mkOfCone {S : Type u_2} {R : Type u_3} [Ring R] [SetLike S R] (C : S) [RingConeClass S R] : IsOrderedRing R

Construct a partially ordered ring by designating a cone in a ring.