# Addition on the rational numbers

Content created by Fredrik Bakke, malarbol, Egbert Rijke, Julian KG, fernabnor and louismntnu.

Created on 2023-06-25.

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


Imports
open import elementary-number-theory.addition-integer-fractions
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.reduced-integer-fractions

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.interchange-law


## Idea

We introduce addition on the rational numbers and derive its basic properties.

## Definition

add-ℚ : ℚ → ℚ → ℚ
add-ℚ (x , p) (y , q) = rational-fraction-ℤ (add-fraction-ℤ x y)

add-ℚ' : ℚ → ℚ → ℚ

infixl 35 _+ℚ_

{x y x' y' : ℚ} → x ＝ x' → y ＝ y' → x +ℚ y ＝ x' +ℚ y'


## Properties

### Unit laws

abstract
left-unit-law-add-ℚ : (x : ℚ) → zero-ℚ +ℚ x ＝ x
eq-ℚ-sim-fraction-ℤ
( x)
is-retraction-rational-fraction-ℚ (x , p)

right-unit-law-add-ℚ : (x : ℚ) → x +ℚ zero-ℚ ＝ x
eq-ℚ-sim-fraction-ℤ
( x)
is-retraction-rational-fraction-ℚ (x , p)


abstract
(x y z : ℚ) →
(x +ℚ y) +ℚ z ＝ x +ℚ (y +ℚ z)
associative-add-ℚ (x , px) (y , py) (z , pz) =
equational-reasoning
rational-fraction-ℤ
by eq-ℚ-sim-fraction-ℤ _ _
( symmetric-sim-fraction-ℤ _ _
( refl-sim-fraction-ℤ z))
by eq-ℚ-sim-fraction-ℤ _ _ (associative-add-fraction-ℤ x y z)
＝ rational-fraction-ℤ
by eq-ℚ-sim-fraction-ℤ _ _
( refl-sim-fraction-ℤ x)


abstract
(x y : ℚ) →
x +ℚ y ＝ y +ℚ x
commutative-add-ℚ (x , px) (y , py) =
eq-ℚ-sim-fraction-ℤ


abstract
(x y u v : ℚ) → (x +ℚ y) +ℚ (u +ℚ v) ＝ (x +ℚ u) +ℚ (y +ℚ v)
interchange-law-commutative-and-associative


### The negative of a rational number is its additive inverse

abstract
left-inverse-law-add-ℚ : (x : ℚ) → (neg-ℚ x) +ℚ x ＝ zero-ℚ
( eq-ℚ-sim-fraction-ℤ
( add-fraction-ℤ (neg-fraction-ℤ (fraction-ℚ x)) (fraction-ℚ x))
( fraction-ℚ zero-ℚ)
( sim-is-zero-numerator-fraction-ℤ
( add-fraction-ℤ (neg-fraction-ℤ (fraction-ℚ x)) (fraction-ℚ x))
( fraction-ℚ zero-ℚ)
( refl))) ∙
( is-retraction-rational-fraction-ℚ zero-ℚ)

right-inverse-law-add-ℚ : (x : ℚ) → x +ℚ (neg-ℚ x) ＝ zero-ℚ


### The negatives of rational numbers distribute over addition

abstract