Homotopy Type Theory ordered field > history (Rev #5, changes)

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

Definition

< ordered field

With strict order

An ordered field is a strictly ordered integral \mathbb{Q}-algebra such that for every element a:Aa:A such that max(a,a)>0\max(a, -a) \gt 0, there is an element b:Ab:A such that ab=1a \cdot b = 1.

With positivity

An ordered field is a commutative ring with a predicate isPositive\mathrm{isPositive} such that

  • zero is not positive:
isPositive(0)\mathrm{isPositive}(0) \to \emptyset
  • one is positive:
isPositive(1)\mathrm{isPositive}(1)
  • 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)
  • for every term a:Aa:A, b:Ab:A, if aa is positive and bb is positive, then aba \cdot b is positive
a:A b:AisPositive(a)×isPositive(b)isPositive(ab)\prod_{a:A} \prod_{b:A} \mathrm{isPositive}(a) \times \mathrm{isPositive}(b) \to \mathrm{isPositive}(a \cdot b)
  • for every term a:Aa:A, if aa is positive, then there exists a bb such that ab=1a \cdot b = 1 and ba=1b \cdot a = 1
a:AisPositive(a)[ b:A(ab=1)×(ba=1)]\prod_{a:A} \mathrm{isPositive}(a) \to \left[\sum_{b:A} (a \cdot b = 1) \times (b \cdot a = 1)\right]

Examples

See also

Revision on June 16, 2022 at 18:43:54 by Anonymous?. See the history of this page for a list of all contributions to it.