Construct ordered rings from rings with a specified positive cone.

In this file we provide the structure RingCone that encodes axioms of ordered rings in terms of the subset of non-negative elements.

We also provide constructors that convert between cones in rings and the corresponding ordered rings.

class RingConeClass (S : Type u_1) (R : outParam (Type u_2)) [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

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

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]

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

Equations

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

@[instance_reducible]

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

Equations

• instPartialOrderRingCone R = PartialOrder.ofSetLike (RingCone R)

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

@[simp]

theorem RingCone.mem_mk {R : Type u_1} [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]

theorem RingCone.coe_set_mk {R : Type u_1} [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

def RingCone.nonneg (T : Type u_1) [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]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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