The additive group of 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.additive-group-of-rational-numbers where
Imports 
open import elementary-number-theory.addition-rational-numbers
open import elementary-number-theory.rational-numbers

open import foundation.dependent-pair-types
open import foundation.unital-binary-operations
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.groups
open import group-theory.monoids
open import group-theory.semigroups

Idea

The type of rational numbers equipped with addition is a commutative group with unit zero-ℚ and inverse given byneg-ℚ.

Definitions

The additive abelian group of rational numbers

semigroup-add-ℚ : Semigroup lzero
pr1 semigroup-add-ℚ = ℚ-Set
pr1 (pr2 semigroup-add-ℚ) = add-ℚ
pr2 (pr2 semigroup-add-ℚ) = associative-add-ℚ

is-unital-add-ℚ : is-unital add-ℚ
pr1 is-unital-add-ℚ = zero-ℚ
pr1 (pr2 is-unital-add-ℚ) = left-unit-law-add-ℚ
pr2 (pr2 is-unital-add-ℚ) = right-unit-law-add-ℚ

monoid-add-ℚ : Monoid lzero
pr1 monoid-add-ℚ = semigroup-add-ℚ
pr2 monoid-add-ℚ = is-unital-add-ℚ

group-add-ℚ : Group lzero
pr1 group-add-ℚ = semigroup-add-ℚ
pr1 (pr2 group-add-ℚ) = is-unital-add-ℚ
pr1 (pr2 (pr2 group-add-ℚ)) = neg-ℚ
pr1 (pr2 (pr2 (pr2 group-add-ℚ))) = left-inverse-law-add-ℚ
pr2 (pr2 (pr2 (pr2 group-add-ℚ))) = right-inverse-law-add-ℚ

Properties

Tha additive group of rational numbers is commutative

abelian-group-add-ℚ : Ab lzero
pr1 abelian-group-add-ℚ = group-add-ℚ
pr2 abelian-group-add-ℚ = commutative-add-ℚ

Recent changes