Construct ordered groups from positive cones

In this file we provide structures PositiveCone and TotalPositiveCone that encode axioms of OrderedAddCommGroup and LinearOrderedAddCommGroup in terms of the (0 ≤ ·) predicate.

We also provide two constructors, OrderedAddCommGroup.mkOfPositiveCone and LinearOrderedAddCommGroup.mkOfPositiveCone, that turn these structures into instances of the corresponding typeclasses.

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

A collection of elements in an AddCommGroup designated as "non-negative". This is useful for constructing an OrderedAddCommGroup by choosing a positive cone in an existing AddCommGroup.

• nonneg : α → Prop

  The characteristic predicate of a positive cone. nonneg a means that 0 ≤ a according to the cone.

• pos : α → Prop

  The characteristic predicate of a positive cone. pos a means that 0 < a according to the cone.

• 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

theorem AddCommGroup.PositiveCone.pos_iff {α : Type u_1} [AddCommGroup α] (self : AddCommGroup.PositiveCone α) (a : α) : self.pos a ↔ self.nonneg a ∧ ¬self.nonneg (-a)

theorem AddCommGroup.PositiveCone.zero_nonneg {α : Type u_1} [AddCommGroup α] (self : AddCommGroup.PositiveCone α) : self.nonneg 0

theorem AddCommGroup.PositiveCone.add_nonneg {α : Type u_1} [AddCommGroup α] (self : AddCommGroup.PositiveCone α) {a : α} {b : α} : self.nonneg a → self.nonneg b → self.nonneg (a + b)

theorem AddCommGroup.PositiveCone.nonneg_antisymm {α : Type u_1} [AddCommGroup α] (self : AddCommGroup.PositiveCone α) {a : α} : self.nonneg a → self.nonneg (-a) → a = 0

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

A positive cone in an AddCommGroup induces a linear order if for every a, either a or -a is non-negative.

• 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
• 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

theorem AddCommGroup.TotalPositiveCone.nonneg_total {α : Type u_1} [AddCommGroup α] (self : AddCommGroup.TotalPositiveCone α) (a : α) : self.nonneg a ∨ self.nonneg (-a)

Either a or -a is nonneg

def OrderedAddCommGroup.mkOfPositiveCone {α : Type u_1} [AddCommGroup α] (C : AddCommGroup.PositiveCone α) : OrderedAddCommGroup α

Construct an OrderedAddCommGroup by designating a positive cone in an existing AddCommGroup.

Equations

• OrderedAddCommGroup.mkOfPositiveCone C = let __src := inst; OrderedAddCommGroup.mk ⋯

def LinearOrderedAddCommGroup.mkOfPositiveCone {α : Type u_1} [AddCommGroup α] (C : AddCommGroup.TotalPositiveCone α) : LinearOrderedAddCommGroup α

Construct a LinearOrderedAddCommGroup by designating a positive cone in an existing AddCommGroup such that for every a, either a or -a is non-negative.

Equations

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