Homotopy Type Theory ordered abelian group > history (changes)

Showing changes from revision #5 to #6: Added | Removed | Changed

Definition

With strict order

An ordered abelian group is an abelian group AA with a strict order <\lt and a family of dependent terms

a:A,b:Aα(a,b):(0<a)×(0<b)(0<a+b)a:A, b:A \vdash \alpha(a, b): (0 \lt a) \times (0 \lt b) \to (0 \lt a + b)

With positivity

An ordered abelian group is an abelian group AA with a predicate isPositive\mathrm{isPositive} such that

  • zero is not positive:
isPositive(0)\mathrm{isPositive}(0) \to \emptyset
  • for every term a:Aa:A, if aa is not positive and a-a is not positive, then a=0a = 0
a:A((isPositive(a))×(isPositive(a)))(a=0)\prod_{a:A} ((\mathrm{isPositive}(a) \to \emptyset) \times (\mathrm{isPositive}(-a) \to \emptyset)) \to (a = 0)
  • for every term a:Aa:A, if aa is positive, then a-a is not positive.
a:A b:AisPositive(a)(isPositive(a))\prod_{a:A} \prod_{b:A} \mathrm{isPositive}(a) \to (\mathrm{isPositive}(-a) \to \emptyset)
  • for every term a:Aa:A, b:Ab:A, if aa is positive, then either bb is positive or aba - b is positive.
a:A b:AisPositive(a)[isPositive(b)+isPositive(ab)]\prod_{a:A} \prod_{b:A} \mathrm{isPositive}(a) \to \left[\mathrm{isPositive}(b) + \mathrm{isPositive}(a - b)\right]
  • for every term a:Aa:A, b:Ab:A, if aa is positive and bb is positive, then a+ba + b is positive
a:A b:AisPositive(a)×isPositive(b)isPositive(a+b)\prod_{a:A} \prod_{b:A} \mathrm{isPositive}(a) \times \mathrm{isPositive}(b) \to \mathrm{isPositive}(a + b)

Examples

See also

Last revised on June 16, 2022 at 22:40:15. See the history of this page for a list of all contributions to it.