Positive rational numbers
Content created by Louis Wasserman, malarbol, Fredrik Bakke and Garrett Figueroa.
Created on 2024-04-25.
Last modified on 2025-10-07.
{-# OPTIONS --lossy-unification #-} module elementary-number-theory.positive-rational-numbers where
Imports
open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.cross-multiplication-difference-integer-fractions open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integers open import elementary-number-theory.negative-integers open import elementary-number-theory.nonzero-natural-numbers open import elementary-number-theory.nonzero-rational-numbers open import elementary-number-theory.positive-and-negative-integers open import elementary-number-theory.positive-integer-fractions open import elementary-number-theory.positive-integers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.cartesian-product-types open import foundation.coproduct-types open import foundation.decidable-subtypes open import foundation.dependent-pair-types open import foundation.function-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels open import set-theory.countable-sets
Idea
A rational number x
is said to
be positive¶
if its underlying fraction is
positive.
Positive rational numbers are a subsemigroup of the additive monoid of rational numbers and a submonoid of the multiplicative monoid of rational numbers.
Definitions
The property of being a positive rational number
module _ (x : ℚ) where is-positive-ℚ : UU lzero is-positive-ℚ = is-positive-fraction-ℤ (fraction-ℚ x) is-prop-is-positive-ℚ : is-prop is-positive-ℚ is-prop-is-positive-ℚ = is-prop-is-positive-fraction-ℤ (fraction-ℚ x) is-positive-prop-ℚ : Prop lzero pr1 is-positive-prop-ℚ = is-positive-ℚ pr2 is-positive-prop-ℚ = is-prop-is-positive-ℚ decidable-subtype-positive-ℚ : decidable-subtype lzero ℚ decidable-subtype-positive-ℚ x = decidable-subtype-positive-fraction-ℤ (fraction-ℚ x)
The type of positive rational numbers
positive-ℚ : UU lzero positive-ℚ = type-subtype is-positive-prop-ℚ ℚ⁺ : UU lzero ℚ⁺ = positive-ℚ module _ (x : positive-ℚ) where rational-ℚ⁺ : ℚ rational-ℚ⁺ = pr1 x fraction-ℚ⁺ : fraction-ℤ fraction-ℚ⁺ = fraction-ℚ rational-ℚ⁺ numerator-ℚ⁺ : ℤ numerator-ℚ⁺ = numerator-ℚ rational-ℚ⁺ denominator-ℚ⁺ : ℤ denominator-ℚ⁺ = denominator-ℚ rational-ℚ⁺ is-positive-rational-ℚ⁺ : is-positive-ℚ rational-ℚ⁺ is-positive-rational-ℚ⁺ = pr2 x is-positive-fraction-ℚ⁺ : is-positive-fraction-ℤ fraction-ℚ⁺ is-positive-fraction-ℚ⁺ = is-positive-rational-ℚ⁺ is-positive-numerator-ℚ⁺ : is-positive-ℤ numerator-ℚ⁺ is-positive-numerator-ℚ⁺ = is-positive-rational-ℚ⁺ is-positive-denominator-ℚ⁺ : is-positive-ℤ denominator-ℚ⁺ is-positive-denominator-ℚ⁺ = is-positive-denominator-ℚ rational-ℚ⁺ abstract eq-ℚ⁺ : {x y : ℚ⁺} → rational-ℚ⁺ x = rational-ℚ⁺ y → x = y eq-ℚ⁺ {x} {y} = eq-type-subtype is-positive-prop-ℚ
Properties
The positive rational numbers form a set
set-ℚ⁺ : Set lzero set-ℚ⁺ = set-subset ℚ-Set is-positive-prop-ℚ is-set-ℚ⁺ : is-set ℚ⁺ is-set-ℚ⁺ = is-set-type-Set set-ℚ⁺
The set of positive rational numbers is countable
abstract is-countable-set-ℚ⁺ : is-countable set-ℚ⁺ is-countable-set-ℚ⁺ = is-countable-decidable-subset-is-countable ( ℚ-Set) ( decidable-subtype-positive-ℚ) ( is-countable-ℚ)
The rational image of a positive integer is positive
abstract is-positive-rational-ℤ : (x : ℤ) → is-positive-ℤ x → is-positive-ℚ (rational-ℤ x) is-positive-rational-ℤ x P = P positive-rational-positive-ℤ : positive-ℤ → ℚ⁺ positive-rational-positive-ℤ (z , pos-z) = rational-ℤ z , pos-z positive-rational-ℤ⁺ : ℤ⁺ → ℚ⁺ positive-rational-ℤ⁺ = positive-rational-positive-ℤ one-ℚ⁺ : ℚ⁺ one-ℚ⁺ = (one-ℚ , is-positive-int-positive-ℤ one-positive-ℤ)
The type of positive rational numbers is inhabited
abstract is-inhabited-ℚ⁺ : ║ ℚ⁺ ║₋₁ is-inhabited-ℚ⁺ = unit-trunc-Prop one-ℚ⁺
The rational image of a positive natural number is positive
positive-rational-ℕ⁺ : ℕ⁺ → ℚ⁺ positive-rational-ℕ⁺ n = positive-rational-positive-ℤ (positive-int-ℕ⁺ n)
The rational image of a positive integer fraction is positive
opaque unfolding rational-fraction-ℤ is-positive-rational-fraction-ℤ : {x : fraction-ℤ} (P : is-positive-fraction-ℤ x) → is-positive-ℚ (rational-fraction-ℤ x) is-positive-rational-fraction-ℤ = is-positive-reduce-fraction-ℤ
A rational number x
is positive if and only if 0 < x
module _ (x : ℚ) where opaque unfolding le-ℚ-Prop le-zero-is-positive-ℚ : is-positive-ℚ x → le-ℚ zero-ℚ x le-zero-is-positive-ℚ = is-positive-eq-ℤ (inv (cross-mul-diff-zero-fraction-ℤ (fraction-ℚ x))) is-positive-le-zero-ℚ : le-ℚ zero-ℚ x → is-positive-ℚ x is-positive-le-zero-ℚ = is-positive-eq-ℤ (cross-mul-diff-zero-fraction-ℤ (fraction-ℚ x))
Zero is not a positive rational number
abstract is-not-positive-zero-ℚ : ¬ (is-positive-ℚ zero-ℚ) is-not-positive-zero-ℚ pos-0 = irreflexive-le-ℚ zero-ℚ (le-zero-is-positive-ℚ zero-ℚ pos-0)
The difference of a rational number with a lesser rational number is positive
module _ (x y : ℚ) (H : le-ℚ x y) where abstract is-positive-diff-le-ℚ : is-positive-ℚ (y -ℚ x) is-positive-diff-le-ℚ = is-positive-le-zero-ℚ ( y -ℚ x) ( backward-implication ( iff-translate-diff-le-zero-ℚ x y) ( H)) positive-diff-le-ℚ : ℚ⁺ positive-diff-le-ℚ = y -ℚ x , is-positive-diff-le-ℚ left-law-positive-diff-le-ℚ : (rational-ℚ⁺ positive-diff-le-ℚ) +ℚ x = y left-law-positive-diff-le-ℚ = ( associative-add-ℚ y (neg-ℚ x) x) ∙ ( inv-tr ( λ u → y +ℚ u = y) ( left-inverse-law-add-ℚ x) ( right-unit-law-add-ℚ y)) right-law-positive-diff-le-ℚ : x +ℚ (rational-ℚ⁺ positive-diff-le-ℚ) = y right-law-positive-diff-le-ℚ = commutative-add-ℚ x (y -ℚ x) ∙ left-law-positive-diff-le-ℚ
A nonzero rational number or its negative is positive
opaque unfolding neg-ℚ decide-is-negative-is-positive-is-nonzero-ℚ : {x : ℚ} → is-nonzero-ℚ x → is-positive-ℚ (neg-ℚ x) + is-positive-ℚ x decide-is-negative-is-positive-is-nonzero-ℚ {x} H = rec-coproduct ( inl ∘ is-positive-neg-is-negative-ℤ) ( inr) ( decide-sign-nonzero-ℤ { numerator-ℚ x} ( is-nonzero-numerator-is-nonzero-ℚ x H))
A rational and its negative are not both positive
opaque unfolding neg-ℚ not-is-negative-is-positive-ℚ : (x : ℚ) → ¬ (is-positive-ℚ (neg-ℚ x) × is-positive-ℚ x) not-is-negative-is-positive-ℚ x (N , P) = is-not-negative-and-positive-ℤ ( numerator-ℚ x) ( ( is-negative-eq-ℤ (neg-neg-ℤ (numerator-ℚ x)) (is-negative-neg-is-positive-ℤ {numerator-ℚ (neg-ℚ x)} N)) , ( P))
Positive rational numbers are nonzero
abstract is-nonzero-is-positive-ℚ : {x : ℚ} → is-positive-ℚ x → is-nonzero-ℚ x is-nonzero-is-positive-ℚ {x} H = is-nonzero-is-nonzero-numerator-ℚ x ( is-nonzero-is-positive-ℤ { numerator-ℚ x} ( H)) nonzero-ℚ⁺ : positive-ℚ → nonzero-ℚ nonzero-ℚ⁺ (x , P) = (x , is-nonzero-is-positive-ℚ P)
If p ≤ q
for positive p
, then q
is positive
abstract is-positive-leq-ℚ⁺ : (p : ℚ⁺) (q : ℚ) → leq-ℚ (rational-ℚ⁺ p) q → is-positive-ℚ q is-positive-leq-ℚ⁺ (p , pos-p) q p≤q = is-positive-le-zero-ℚ ( q) ( concatenate-le-leq-ℚ _ _ _ (le-zero-is-positive-ℚ p pos-p) p≤q) is-positive-le-ℚ⁺ : (p : ℚ⁺) (q : ℚ) → le-ℚ (rational-ℚ⁺ p) q → is-positive-ℚ q is-positive-le-ℚ⁺ p q p<q = is-positive-leq-ℚ⁺ p q (leq-le-ℚ p<q)
Recent changes
- 2025-10-07. Louis Wasserman. Multiplication of interior intervals in the rational numbers (#1561).
- 2025-10-04. Louis Wasserman. Split out operations on positive rational numbers (#1562).
- 2025-09-09. Louis Wasserman. The positive rational numbers are countable (#1538).
- 2025-09-04. Louis Wasserman. Suprema and infima of totally bounded subsets of the reals (#1510).
- 2025-08-11. malarbol and Garrett Figueroa. Ring extensions of
ℚ
and rational modules (#1452).