Construct ordered rings from rings with a specified positive cone.

In this file we provide the structure RingCone that encodes axioms of OrderedRing and LinearOrderedRing 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 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 RingCone.instRingConeClass (R : Type u_1) [Ring R] : RingConeClass (RingCone R) R

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

@[simp]

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

@[simp]

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

@[simp]

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

instance RingCone.nonneg.isMaxCone {T : Type u_2} [LinearOrderedRing T] : IsMaxCone (nonneg T)

@[reducible]

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

Construct a partially ordered ring by designating a cone in a ring. Warning: using this def as a constructor in an instance can lead to diamonds due to non-customisable field: lt.

Equations

• OrderedRing.mkOfCone C = OrderedRing.mk ⋯ ⋯ ⋯

@[reducible]

def LinearOrderedRing.mkOfCone {S : Type u_1} {R : Type u_2} [Ring R] [SetLike S R] (C : S) [IsDomain R] [RingConeClass S R] [IsMaxCone C] (dec : DecidablePred fun (x : R) => x ∈ C) : LinearOrderedRing R

Construct a linearly ordered domain by designating a maximal cone in a domain. Warning: using this def as a constructor in an instance can lead to diamonds due to non-customisable fields: lt, decidableLT, decidableEq, compare.

Equations

• LinearOrderedRing.mkOfCone C dec = LinearOrderedRing.mk ⋯ (fun (x x_1 : R) => dec (x_1 - x)) decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯