The nonpositive rational numbers

Content created by Louis Wasserman.

Created on 2025-10-07.
Last modified on 2025-10-17.

{-# OPTIONS --lossy-unification #-}

module elementary-number-theory.nonpositive-rational-numbers where
Imports 
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-rational-numbers
open import elementary-number-theory.nonnegative-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.dependent-pair-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels

Idea

A rational number x is said to be nonpositive if its numerator is a nonpositive integer.

Definitions

The property of being a nonpositive rational number

module _
  (q : ℚ)
  where

  opaque
    is-nonpositive-ℚ : UU lzero
    is-nonpositive-ℚ = is-nonnegative-ℚ (neg-ℚ q)

    is-prop-is-nonpositive-ℚ : is-prop is-nonpositive-ℚ
    is-prop-is-nonpositive-ℚ = is-prop-is-nonnegative-ℚ (neg-ℚ q)

  is-nonpositive-prop-ℚ : Prop lzero
  is-nonpositive-prop-ℚ = (is-nonpositive-ℚ , is-prop-is-nonpositive-ℚ)

The type of nonpositive rational numbers

nonpositive-ℚ : UU lzero
nonpositive-ℚ = type-subtype is-nonpositive-prop-ℚ

ℚ⁰⁻ : UU lzero
ℚ⁰⁻ = nonpositive-ℚ

module _
  (x : nonpositive-ℚ)
  where

  rational-ℚ⁰⁻ : ℚ
  rational-ℚ⁰⁻ = pr1 x

  fraction-ℚ⁰⁻ : fraction-ℤ
  fraction-ℚ⁰⁻ = fraction-ℚ rational-ℚ⁰⁻

  numerator-ℚ⁰⁻ : ℤ
  numerator-ℚ⁰⁻ = numerator-ℚ rational-ℚ⁰⁻

  denominator-ℚ⁰⁻ : ℤ
  denominator-ℚ⁰⁻ = denominator-ℚ rational-ℚ⁰⁻

Properties

Equality on nonpositive rational numbers

abstract
  eq-ℚ⁰⁻ : {x y : ℚ⁰⁻} → rational-ℚ⁰⁻ x ＝ rational-ℚ⁰⁻ y → x ＝ y
  eq-ℚ⁰⁻ {x} {y} = eq-type-subtype is-nonpositive-prop-ℚ

A rational number is nonpositive if and only if it is less than or equal to zero

opaque
  unfolding is-nonpositive-ℚ

  leq-zero-is-nonpositive-ℚ : {q : ℚ} → is-nonpositive-ℚ q → leq-ℚ q zero-ℚ
  leq-zero-is-nonpositive-ℚ {q} is-nonpos-q =
    binary-tr
      ( leq-ℚ)
      ( neg-neg-ℚ q)
      ( neg-zero-ℚ)
      ( neg-leq-ℚ (leq-zero-is-nonnegative-ℚ is-nonpos-q))

  is-nonpositive-leq-zero-ℚ : {q : ℚ} → leq-ℚ q zero-ℚ → is-nonpositive-ℚ q
  is-nonpositive-leq-zero-ℚ {q} q≤0 =
    is-nonnegative-leq-zero-ℚ
      ( tr
        ( λ y → leq-ℚ y (neg-ℚ q))
        ( neg-zero-ℚ)
        ( neg-leq-ℚ q≤0))

is-nonpositive-iff-leq-zero-ℚ : (q : ℚ) → is-nonpositive-ℚ q ↔ leq-ℚ q zero-ℚ
is-nonpositive-iff-leq-zero-ℚ q =
  ( leq-zero-is-nonpositive-ℚ ,
    is-nonpositive-leq-zero-ℚ)

If p ≤ q and q is nonpositive, then p is nonpositive

abstract
  is-nonpositive-leq-ℚ⁰⁻ :
    (q : ℚ⁰⁻) (p : ℚ) → leq-ℚ p (rational-ℚ⁰⁻ q) → is-nonpositive-ℚ p
  is-nonpositive-leq-ℚ⁰⁻ (q , nonpos-q) p p≤q =
    is-nonpositive-leq-zero-ℚ
      ( transitive-leq-ℚ p q zero-ℚ
        ( leq-zero-is-nonpositive-ℚ nonpos-q)
        ( p≤q))

Recent changes