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

Positive cones

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

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.

• nonneg : α → Prop
• pos : α → Prop
• pos_iff : ∀ (a : α), self.pos a ↔ self.nonneg a ∧ ¬self.nonneg (-a)
• zero_nonneg : self.nonneg 0
• add_nonneg : ∀ {a b : α}, self.nonneg a → self.nonneg b → self.nonneg (a + b)
• nonneg_antisymm : ∀ {a : α}, self.nonneg a → self.nonneg (-a) → a = 0
• one_nonneg : self.nonneg 1

  In a positive cone, 1 is nonneg

• mul_pos : ∀ (a b : α), self.pos a → self.pos b → self.pos (a * b)

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

theorem Ring.PositiveCone.one_nonneg {α : Type u_2} [Ring α] (self : Ring.PositiveCone α) : self.nonneg 1

In a positive cone, 1 is nonneg

theorem Ring.PositiveCone.mul_pos {α : Type u_2} [Ring α] (self : Ring.PositiveCone α) (a : α) (b : α) : self.pos a → self.pos b → self.pos (a * b)

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

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

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

• nonneg : α → Prop
• pos : α → Prop
• pos_iff : ∀ (a : α), self.pos a ↔ self.nonneg a ∧ ¬self.nonneg (-a)
• zero_nonneg : self.nonneg 0
• add_nonneg : ∀ {a b : α}, self.nonneg a → self.nonneg b → self.nonneg (a + b)
• nonneg_antisymm : ∀ {a : α}, self.nonneg a → self.nonneg (-a) → a = 0
• one_nonneg : self.nonneg 1
• mul_pos : ∀ (a b : α), self.pos a → self.pos b → self.pos (a * b)
• nonnegDecidable : DecidablePred self.nonneg

  For any a the proposition nonneg a is decidable

• nonneg_total : ∀ (a : α), self.nonneg a ∨ self.nonneg (-a)

  Either a or -a is nonneg

@[reducible]

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

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

Equations

• self.toTotalPositiveCone = { toPositiveCone := self.toPositiveCone, nonnegDecidable := self.nonnegDecidable, nonneg_total := ⋯ }

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

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

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

Equations

• StrictOrderedRing.mkOfPositiveCone C = let __src := inst✝; let __src_1 := OrderedAddCommGroup.mkOfPositiveCone C.toPositiveCone; StrictOrderedRing.mk ⋯ ⋯ ⋯

def LinearOrderedRing.mkOfPositiveCone {α : Type u_1} [Ring α] [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.