Homotopy Type Theory ordered integral domain > history (Rev #7, changes)

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

Definition

An ordered integral domain is a totally ordered commutative ring? which comes with a strict order <\lt such that

  • 0<10 \lt 1
  • for all elements a:Ra:R and b:Rb:R, if 0<a0 \lt a and 0<b0 \lt b, then 0<a+b0 \lt a + b
  • for all elements a:Ra:R and b:Rb:R, if 0<a0 \lt a and 0<b0 \lt b, then 0<ab0 \lt a \cdot b
  • for all elements a:Ra:R and b:Rb:R, if 0<max(a,a)0 \lt \max(a, -a) and 0<max(b,b)0 \lt \max(b, -b), then 0<max(ab,ab)0 \lt \max(a \cdot b, -a \cdot b)

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 20:02:21 by Anonymous?. See the history of this page for a list of all contributions to it.