Constructing an ordered ring from a ring with a specified positive cone.

Positive cones

ink

structure Ring.PositiveCone (α : Type u_1) [inst : Ring α] extends AddCommGroup.PositiveCone : Type u_1

• In a positive cone, 1 is nonneg

  one_nonneg : AddCommGroup.PositiveCone.nonneg toPositiveCone 1

• In a positive cone, if a and b are pos then so is a * b

  mul_pos : ∀ (a b : α), AddCommGroup.PositiveCone.pos toPositiveCone a → AddCommGroup.PositiveCone.pos toPositiveCone b → AddCommGroup.PositiveCone.pos toPositiveCone (a * b)

A positive cone in a ring consists of a positive cone in underlying AddCommGroup, which contains 1 and such that the positive elements are closed under multiplication.

ink

structure Ring.TotalPositiveCone (α : Type u_1) [inst : Ring α] extends Ring.PositiveCone : Type u_1

• For any a the proposition nonneg a is decidable

  nonnegDecidable : DecidablePred toPositiveCone_1.toPositiveCone.nonneg

• Either a or -a is nonneg

  nonneg_total : ∀ (a : α), AddCommGroup.PositiveCone.nonneg toPositiveCone_1.toPositiveCone a ∨ AddCommGroup.PositiveCone.nonneg toPositiveCone_1.toPositiveCone (-a)

A total positive cone in a nontrivial ring induces a linear order.

ink

abbrev Ring.TotalPositiveCone.toTotalPositiveCone {α : Type u_1} [inst : Ring α] (self : Ring.TotalPositiveCone α) : AddCommGroup.TotalPositiveCone α

Forget that a TotalPositiveCone in a ring respects the multiplicative structure.

Equations

• One or more equations did not get rendered due to their size.

ink

theorem Ring.PositiveCone.one_pos {α : Type u_1} [inst : Ring α] [inst : Nontrivial α] (C : Ring.PositiveCone α) : AddCommGroup.PositiveCone.pos C.toPositiveCone 1

ink

def StrictOrderedRing.mkOfPositiveCone {α : Type u_1} [inst : Ring α] [inst : Nontrivial α] (C : Ring.PositiveCone α) : StrictOrderedRing α

Construct a StrictOrderedRing by designating a positive cone in an existing Ring.

Equations

• One or more equations did not get rendered due to their size.

ink

def LinearOrderedRing.mkOfPositiveCone {α : Type u_1} [inst : Ring α] [inst : Nontrivial α] (C : Ring.TotalPositiveCone α) : LinearOrderedRing α

Construct a LinearOrderedRing by designating a positive cone in an existing Ring.

Equations

• One or more equations did not get rendered due to their size.