Negative rational numbers
Content created by Louis Wasserman and Fredrik Bakke.
Created on 2025-03-25.
Last modified on 2025-10-17.
{-# OPTIONS --lossy-unification #-} module elementary-number-theory.negative-rational-numbers where
Imports
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-integer-fractions open import elementary-number-theory.negative-integers 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.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.action-on-identifications-functions open import foundation.binary-relations open import foundation.binary-transport open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels
Idea
A rational number x
is said to
be negative¶
if its negation is positive.
Negative rational numbers are a subsemigroup of the additive monoid of rational numbers.
Definitions
The property of being a negative rational number
module _ (q : ℚ) where opaque is-negative-ℚ : UU lzero is-negative-ℚ = is-positive-ℚ (neg-ℚ q) is-prop-is-negative-ℚ : is-prop is-negative-ℚ is-prop-is-negative-ℚ = is-prop-is-positive-ℚ (neg-ℚ q) is-negative-prop-ℚ : Prop lzero pr1 is-negative-prop-ℚ = is-negative-ℚ pr2 is-negative-prop-ℚ = is-prop-is-negative-ℚ
The type of negative rational numbers
negative-ℚ : UU lzero negative-ℚ = type-subtype is-negative-prop-ℚ ℚ⁻ : UU lzero ℚ⁻ = negative-ℚ module _ (x : negative-ℚ) where rational-ℚ⁻ : ℚ rational-ℚ⁻ = pr1 x fraction-ℚ⁻ : fraction-ℤ fraction-ℚ⁻ = fraction-ℚ rational-ℚ⁻ numerator-ℚ⁻ : ℤ numerator-ℚ⁻ = numerator-ℚ rational-ℚ⁻ denominator-ℚ⁻ : ℤ denominator-ℚ⁻ = denominator-ℚ rational-ℚ⁻ is-negative-rational-ℚ⁻ : is-negative-ℚ rational-ℚ⁻ is-negative-rational-ℚ⁻ = pr2 x opaque unfolding is-negative-ℚ is-positive-ℚ neg-ℚ is-negative-fraction-ℚ⁻ : is-negative-fraction-ℤ fraction-ℚ⁻ is-negative-fraction-ℚ⁻ = tr ( is-negative-ℤ) ( neg-neg-ℤ _) ( is-negative-neg-is-positive-ℤ is-negative-rational-ℚ⁻) is-negative-numerator-ℚ⁻ : is-negative-ℤ numerator-ℚ⁻ is-negative-numerator-ℚ⁻ = is-negative-fraction-ℚ⁻ 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-negative-prop-ℚ
Properties
The negative rational numbers form a set
is-set-ℚ⁻ : is-set ℚ⁻ is-set-ℚ⁻ = is-set-type-subtype is-negative-prop-ℚ is-set-ℚ
The rational image of a negative integer is negative
opaque unfolding is-negative-ℚ is-positive-ℚ neg-ℚ is-negative-rational-ℤ : (x : ℤ) → is-negative-ℤ x → is-negative-ℚ (rational-ℤ x) is-negative-rational-ℤ _ = is-positive-neg-is-negative-ℤ negative-rational-negative-ℤ : negative-ℤ → ℚ⁻ negative-rational-negative-ℤ (x , x-is-neg) = rational-ℤ x , is-negative-rational-ℤ x x-is-neg neg-one-ℚ⁻ : ℚ⁻ neg-one-ℚ⁻ = (neg-one-ℚ , is-negative-rational-ℤ _ _)
The rational image of a negative integer fraction is negative
opaque unfolding is-negative-ℚ is-negative-rational-fraction-ℤ : {x : fraction-ℤ} → is-negative-fraction-ℤ x → is-negative-ℚ (rational-fraction-ℤ x) is-negative-rational-fraction-ℤ {x} P = tr ( is-positive-ℚ) ( neg-rational-fraction-ℤ _) ( is-positive-rational-fraction-ℤ ( is-positive-neg-negative-fraction-ℤ x P))
A rational number x
is negative if and only if x < 0
opaque unfolding is-negative-ℚ le-zero-is-negative-ℚ : {x : ℚ} → is-negative-ℚ x → le-ℚ x zero-ℚ le-zero-is-negative-ℚ {x} is-neg-x = binary-tr ( le-ℚ) ( neg-neg-ℚ x) ( neg-zero-ℚ) ( neg-le-ℚ (le-zero-is-positive-ℚ is-neg-x)) is-negative-le-zero-ℚ : {x : ℚ} → le-ℚ x zero-ℚ → is-negative-ℚ x is-negative-le-zero-ℚ {x} x<0 = is-positive-le-zero-ℚ ( tr ( λ y → le-ℚ y (neg-ℚ x)) ( neg-zero-ℚ) ( neg-le-ℚ x<0)) is-negative-iff-le-zero-ℚ : (x : ℚ) → is-negative-ℚ x ↔ le-ℚ x zero-ℚ is-negative-iff-le-zero-ℚ x = ( le-zero-is-negative-ℚ , is-negative-le-zero-ℚ) abstract leq-zero-is-negative-ℚ : {x : ℚ} → is-negative-ℚ x → leq-ℚ x zero-ℚ leq-zero-is-negative-ℚ is-neg-x = leq-le-ℚ (le-zero-is-negative-ℚ is-neg-x)
The difference of a rational number with a greater rational number is negative
module _ (x y : ℚ) (H : le-ℚ x y) where opaque unfolding is-negative-ℚ is-negative-diff-le-ℚ : is-negative-ℚ (x -ℚ y) is-negative-diff-le-ℚ = inv-tr ( is-positive-ℚ) ( distributive-neg-diff-ℚ x y) ( is-positive-diff-le-ℚ x y H) negative-diff-le-ℚ : ℚ⁻ negative-diff-le-ℚ = x -ℚ y , is-negative-diff-le-ℚ
Negative rational numbers are nonzero
opaque unfolding is-negative-ℚ is-nonzero-is-negative-ℚ : {x : ℚ} → is-negative-ℚ x → is-nonzero-ℚ x is-nonzero-is-negative-ℚ {x} H = tr ( is-nonzero-ℚ) ( neg-neg-ℚ x) ( is-nonzero-neg-ℚ (is-nonzero-is-positive-ℚ H)) nonzero-ℚ⁻ : ℚ⁻ → nonzero-ℚ nonzero-ℚ⁻ (x , N) = (x , is-nonzero-is-negative-ℚ N)
Inequality on negative rational numbers
leq-ℚ⁻ : Relation lzero ℚ⁻ leq-ℚ⁻ p q = leq-ℚ (rational-ℚ⁻ p) (rational-ℚ⁻ q) le-ℚ⁻ : Relation lzero ℚ⁻ le-ℚ⁻ p q = le-ℚ (rational-ℚ⁻ p) (rational-ℚ⁻ q)
If p ≤ q
for negative q
, then p
is negative
abstract is-negative-leq-ℚ⁻ : (q : ℚ⁻) (p : ℚ) → leq-ℚ p (rational-ℚ⁻ q) → is-negative-ℚ p is-negative-leq-ℚ⁻ (q , neg-q) p p≤q = is-negative-le-zero-ℚ ( concatenate-leq-le-ℚ p q zero-ℚ p≤q (le-zero-is-negative-ℚ neg-q)) is-negative-le-ℚ⁻ : (q : ℚ⁻) (p : ℚ) → le-ℚ p (rational-ℚ⁻ q) → is-negative-ℚ p is-negative-le-ℚ⁻ q p p<q = is-negative-leq-ℚ⁻ q p (leq-le-ℚ p<q)
There is no greatest negative rational number
opaque mediant-zero-ℚ⁻ : ℚ⁻ → ℚ⁻ mediant-zero-ℚ⁻ (q , is-neg-q) = ( mediant-ℚ q zero-ℚ , is-negative-le-zero-ℚ ( le-right-mediant-ℚ _ _ (le-zero-is-negative-ℚ is-neg-q))) le-mediant-zero-ℚ⁻ : (q : ℚ⁻) → le-ℚ (rational-ℚ⁻ q) (rational-ℚ⁻ (mediant-zero-ℚ⁻ q)) le-mediant-zero-ℚ⁻ (q , is-neg-q) = le-left-mediant-ℚ _ _ (le-zero-is-negative-ℚ is-neg-q) rational-mediant-zero-ℚ⁻ : ℚ⁻ → ℚ rational-mediant-zero-ℚ⁻ q = rational-ℚ⁻ (mediant-zero-ℚ⁻ q)
Recent changes
- 2025-10-17. Louis Wasserman. Reorganize signed arithmetic on rational numbers (#1582).
- 2025-10-15. Louis Wasserman. Inequalities from multiplication of signed real numbers (#1584).
- 2025-10-11. Louis Wasserman. Square roots of nonnegative real numbers (#1570).
- 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).