Nonzero rational numbers

Content created by Fredrik Bakke and malarbol.

Created on 2024-04-25.
Last modified on 2024-04-25.

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

module elementary-number-theory.nonzero-rational-numbers where
Imports 
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.multiplication-rational-numbers
open import elementary-number-theory.multiplicative-monoid-of-rational-numbers
open import elementary-number-theory.nonzero-integers
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.reduced-integer-fractions

open import foundation.action-on-identifications-functions
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.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.submonoids

Idea

The nonzero rational numbers are the rational numbers different from zero-ℚ.

They form a nonempty subset of the rational numbers, stable under neg-ℚ and mul-ℚ.

Definitions

The property of being a nonzero rational number

is-nonzero-prop-ℚ : ℚ → Prop lzero
is-nonzero-prop-ℚ x = (is-nonzero-ℚ x , is-prop-neg)

The nonzero rational numbers

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

module _
  (x : nonzero-ℚ)
  where

  rational-nonzero-ℚ : ℚ
  rational-nonzero-ℚ = pr1 x

  is-nonzero-rational-nonzero-ℚ : is-nonzero-ℚ rational-nonzero-ℚ
  is-nonzero-rational-nonzero-ℚ = pr2 x

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

Properties

A rational number is nonzero if and only if its numerator is a nonzero integer

module _
  (x : ℚ)
  where

  abstract
    is-nonzero-numerator-is-nonzero-ℚ :
      is-nonzero-ℚ x → is-nonzero-ℤ (numerator-ℚ x)
    is-nonzero-numerator-is-nonzero-ℚ H =
      H ∘ (is-zero-is-zero-numerator-ℚ x)

    is-nonzero-is-nonzero-numerator-ℚ :
      is-nonzero-ℤ (numerator-ℚ x) → is-nonzero-ℚ x
    is-nonzero-is-nonzero-numerator-ℚ H = H ∘ (ap numerator-ℚ)

one-ℚ is nonzero

abstract
  is-nonzero-one-ℚ : is-nonzero-ℚ one-ℚ
  is-nonzero-one-ℚ =
    is-nonzero-is-nonzero-numerator-ℚ
      ( one-ℚ)
      ( is-nonzero-one-ℤ)

one-nonzero-ℚ : nonzero-ℚ
one-nonzero-ℚ = (one-ℚ , is-nonzero-one-ℚ)

The negative of a nonzero rational number is nonzero

abstract
  is-nonzero-neg-ℚ : {x : ℚ} → is-nonzero-ℚ x → is-nonzero-ℚ (neg-ℚ x)
  is-nonzero-neg-ℚ {x} H =
    is-nonzero-is-nonzero-numerator-ℚ
      ( neg-ℚ x)
      ( is-nonzero-neg-nonzero-ℤ
        ( numerator-ℚ x)
        ( is-nonzero-numerator-is-nonzero-ℚ x H))

The nonzero negative of a nonzero rational number

neg-nonzero-ℚ : nonzero-ℚ → nonzero-ℚ
neg-nonzero-ℚ (x , H) = (neg-ℚ x , is-nonzero-neg-ℚ H)

The product of two nonzero rational numbers is nonzero

abstract
  is-nonzero-mul-ℚ :
    {x y : ℚ} → is-nonzero-ℚ x → is-nonzero-ℚ y → is-nonzero-ℚ (x *ℚ y)
  is-nonzero-mul-ℚ {x} {y} H K =
    rec-coproduct H K ∘ (decide-is-zero-factor-is-zero-mul-ℚ x y)

The nonzero rational numbers are a multiplicative submonoid of the rational numbers

is-submonoid-mul-nonzero-ℚ :
  is-submonoid-subset-Monoid monoid-mul-ℚ is-nonzero-prop-ℚ
pr1 is-submonoid-mul-nonzero-ℚ = is-nonzero-one-ℚ
pr2 is-submonoid-mul-nonzero-ℚ x y = is-nonzero-mul-ℚ {x} {y}

submonoid-mul-nonzero-ℚ : Submonoid lzero monoid-mul-ℚ
pr1 submonoid-mul-nonzero-ℚ = is-nonzero-prop-ℚ
pr2 submonoid-mul-nonzero-ℚ = is-submonoid-mul-nonzero-ℚ

The factors of a nonzero product of rational numbers are nonzero

abstract
  is-nonzero-left-factor-mul-ℚ :
    (x y : ℚ) → is-nonzero-ℚ (x *ℚ y) → is-nonzero-ℚ x
  is-nonzero-left-factor-mul-ℚ x y H Z =
    H (ap (_*ℚ y) Z ∙ left-zero-law-mul-ℚ y)

  is-nonzero-right-factor-mul-ℚ :
    (x y : ℚ) → is-nonzero-ℚ (x *ℚ y) → is-nonzero-ℚ y
  is-nonzero-right-factor-mul-ℚ x y H Z =
    H (ap (x *ℚ_) Z ∙ right-zero-law-mul-ℚ x)

Recent changes