The positive, negative, and nonnegative rational numbers

Content created by Louis Wasserman and Fredrik Bakke.

Created on 2025-04-25.
Last modified on 2025-10-17.

module elementary-number-theory.positive-and-negative-rational-numbers where
Imports 
open import elementary-number-theory.inequality-rational-numbers
open import elementary-number-theory.negative-rational-numbers
open import elementary-number-theory.nonnegative-rational-numbers
open import elementary-number-theory.nonpositive-rational-numbers
open import elementary-number-theory.nonzero-rational-numbers
open import elementary-number-theory.positive-and-negative-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.binary-transport
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.function-types
open import foundation.functoriality-coproduct-types
open import foundation.identity-types
open import foundation.negation
open import foundation.transport-along-identifications
open import foundation.universe-levels

Idea

In this file, we outline basic relations between negative, nonnegative, positive, and nonpositive rational numbers.

Properties

Trichotomies

A rational number is either negative, zero, or positive

abstract
  trichotomy-sign-ℚ :
    {l : Level} {A : UU l} (x : ℚ) →
    ( is-negative-ℚ x → A) →
    ( x ＝ zero-ℚ → A) →
    ( is-positive-ℚ x → A) →
    A
  trichotomy-sign-ℚ x neg zero pos =
    trichotomy-le-ℚ
      ( x)
      ( zero-ℚ)
      ( λ x<0 → neg (is-negative-le-zero-ℚ x<0))
      ( zero)
      ( λ 0<x → pos (is-positive-le-zero-ℚ 0<x))

Dichotomies

A rational number is either negative or nonnegative

abstract
  decide-is-negative-is-nonnegative-ℚ :
    (q : ℚ) →
    is-negative-ℚ q + is-nonnegative-ℚ q
  decide-is-negative-is-nonnegative-ℚ q =
    map-coproduct
      ( is-negative-le-zero-ℚ)
      ( is-nonnegative-leq-zero-ℚ)
      ( decide-le-leq-ℚ q zero-ℚ)

A rational number is either positive or nonpositive

abstract
  decide-is-positive-is-nonpositive-ℚ :
    (q : ℚ) →
    is-positive-ℚ q + is-nonpositive-ℚ q
  decide-is-positive-is-nonpositive-ℚ q =
    map-coproduct
      ( is-positive-le-zero-ℚ)
      ( is-nonpositive-leq-zero-ℚ)
      ( decide-le-leq-ℚ zero-ℚ q)

A rational number is nonpositive or nonnegative

abstract
  is-nonpositive-or-nonnegative-ℚ :
    (q : ℚ) →
    is-nonpositive-ℚ q + is-nonnegative-ℚ q
  is-nonpositive-or-nonnegative-ℚ q =
    map-coproduct
      ( is-nonpositive-leq-zero-ℚ)
      ( is-nonnegative-leq-zero-ℚ)
      ( linear-leq-ℚ q zero-ℚ)

If a rational number is nonzero, it is negative or positive

decide-is-negative-is-positive-is-nonzero-ℚ :
  {q : ℚ} → is-nonzero-ℚ q → is-negative-ℚ q + is-positive-ℚ q
decide-is-negative-is-positive-is-nonzero-ℚ {q} q≠0 =
  trichotomy-sign-ℚ q
    ( inl)
    ( ex-falso ∘ q≠0)
    ( inr)

Implications

Any positive rational number is nonnegative

opaque
  unfolding is-nonnegative-ℚ is-positive-ℚ

  is-nonnegative-is-positive-ℚ : {q : ℚ} → is-positive-ℚ q → is-nonnegative-ℚ q
  is-nonnegative-is-positive-ℚ = is-nonnegative-is-positive-ℤ

nonnegative-ℚ⁺ : ℚ⁺ → ℚ⁰⁺
nonnegative-ℚ⁺ (q , H) = (q , is-nonnegative-is-positive-ℚ H)

Any negative rational number is nonpositive

opaque
  unfolding is-negative-ℚ is-nonpositive-ℚ

  is-nonpositive-is-negative-ℚ : {q : ℚ} → is-negative-ℚ q → is-nonpositive-ℚ q
  is-nonpositive-is-negative-ℚ = is-nonnegative-is-positive-ℚ

nonpositive-ℚ⁻ : ℚ⁻ → ℚ⁰⁻
nonpositive-ℚ⁻ (q , H) = (q , is-nonpositive-is-negative-ℚ H)

Operations

The negation of a positive rational number is negative

opaque
  unfolding is-negative-ℚ

  is-negative-neg-is-positive-ℚ :
    {q : ℚ} → is-positive-ℚ q → is-negative-ℚ (neg-ℚ q)
  is-negative-neg-is-positive-ℚ = inv-tr is-positive-ℚ (neg-neg-ℚ _)

neg-ℚ⁺ : ℚ⁺ → ℚ⁻
neg-ℚ⁺ (q , is-pos-q) =
  (neg-ℚ q , is-negative-neg-is-positive-ℚ is-pos-q)

The negation of a negative rational number is positive

opaque
  unfolding is-negative-ℚ

  is-positive-neg-is-negative-ℚ :
    {q : ℚ} → is-negative-ℚ q → is-positive-ℚ (neg-ℚ q)
  is-positive-neg-is-negative-ℚ = id

neg-ℚ⁻ : ℚ⁻ → ℚ⁺
neg-ℚ⁻ (q , is-neg-q) = (neg-ℚ q , is-positive-neg-is-negative-ℚ is-neg-q)

The negation of a nonnegative rational number is nonpositive

opaque
  unfolding is-nonpositive-ℚ

  is-nonpositive-neg-is-nonnegative-ℚ :
    {q : ℚ} → is-nonnegative-ℚ q → is-nonpositive-ℚ (neg-ℚ q)
  is-nonpositive-neg-is-nonnegative-ℚ = inv-tr is-nonnegative-ℚ (neg-neg-ℚ _)

neg-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁻
neg-ℚ⁰⁺ (q , is-nonneg-q) =
  ( neg-ℚ q , is-nonpositive-neg-is-nonnegative-ℚ is-nonneg-q)

The negation of a nonpositive rational number is nonnegative

opaque
  unfolding is-nonpositive-ℚ

  is-nonnegative-neg-is-nonpositive-ℚ :
    {q : ℚ} → is-nonpositive-ℚ q → is-nonnegative-ℚ (neg-ℚ q)
  is-nonnegative-neg-is-nonpositive-ℚ = id

neg-ℚ⁰⁻ : ℚ⁰⁻ → ℚ⁰⁺
neg-ℚ⁰⁻ (q , is-nonpos-q) =
  ( neg-ℚ q , is-nonnegative-neg-is-nonpositive-ℚ is-nonpos-q)

Exclusive cases

A rational number is not both negative and positive

abstract
  is-not-negative-and-positive-ℚ :
    {x : ℚ} → ¬ (is-negative-ℚ x × is-positive-ℚ x)
  is-not-negative-and-positive-ℚ {x} (N , P) =
    not-leq-le-ℚ
      ( zero-ℚ)
      ( x)
      ( le-zero-is-positive-ℚ P)
      ( leq-zero-is-negative-ℚ N)

A rational number is not both negative and nonnegative

abstract
  is-not-negative-and-nonnegativeℚ :
    {x : ℚ} → ¬ (is-negative-ℚ x × is-nonnegative-ℚ x)
  is-not-negative-and-nonnegativeℚ {x} (N , NN) =
    not-leq-le-ℚ
      ( x)
      ( zero-ℚ)
      ( le-zero-is-negative-ℚ N)
      ( leq-zero-is-nonnegative-ℚ NN)

A rational number is not both positive and nonpositive

abstract
  is-not-positive-and-nonpositive-ℚ :
    {x : ℚ} → ¬ (is-positive-ℚ x × is-nonpositive-ℚ x)
  is-not-positive-and-nonpositive-ℚ {x} (P , NP) =
    not-leq-le-ℚ
      ( zero-ℚ)
      ( x)
      ( le-zero-is-positive-ℚ P)
      ( leq-zero-is-nonpositive-ℚ NP)

Recent changes