# The Gaussian integers

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-04-22.

module commutative-algebra.gaussian-integers where

Imports
open import commutative-algebra.commutative-rings

open import elementary-number-theory.difference-integers
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

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

open import ring-theory.rings


## Idea

The Gaussian integers are the complex numbers of the form a + bi, where a and b are integers.

## Definition

### The underlying type of the Gaussian integers

ℤ[i] : UU lzero
ℤ[i] = ℤ × ℤ


### Observational equality of the Gaussian integers

Eq-ℤ[i] : ℤ[i] → ℤ[i] → UU lzero
Eq-ℤ[i] x y = (pr1 x ＝ pr1 y) × (pr2 x ＝ pr2 y)

refl-Eq-ℤ[i] : (x : ℤ[i]) → Eq-ℤ[i] x x
pr1 (refl-Eq-ℤ[i] x) = refl
pr2 (refl-Eq-ℤ[i] x) = refl

Eq-eq-ℤ[i] : {x y : ℤ[i]} → x ＝ y → Eq-ℤ[i] x y
Eq-eq-ℤ[i] {x} refl = refl-Eq-ℤ[i] x

eq-Eq-ℤ[i]' : {x y : ℤ[i]} → Eq-ℤ[i] x y → x ＝ y
eq-Eq-ℤ[i]' {a , b} {.a , .b} (refl , refl) = refl

eq-Eq-ℤ[i] : {x y : ℤ[i]} → pr1 x ＝ pr1 y → pr2 x ＝ pr2 y → x ＝ y
eq-Eq-ℤ[i] {a , b} {.a , .b} refl refl = refl


### The Gaussian integer zero

zero-ℤ[i] : ℤ[i]
pr1 zero-ℤ[i] = zero-ℤ
pr2 zero-ℤ[i] = zero-ℤ


### The Gaussian integer one

one-ℤ[i] : ℤ[i]
pr1 one-ℤ[i] = one-ℤ
pr2 one-ℤ[i] = zero-ℤ


### The inclusion of the integers into the Gaussian integers

gaussian-int-ℤ : ℤ → ℤ[i]
pr1 (gaussian-int-ℤ x) = x
pr2 (gaussian-int-ℤ x) = zero-ℤ


### The Gaussian integer i

i-ℤ[i] : ℤ[i]
pr1 i-ℤ[i] = zero-ℤ
pr2 i-ℤ[i] = one-ℤ


### The Gaussian integer -i

neg-i-ℤ[i] : ℤ[i]
pr1 neg-i-ℤ[i] = zero-ℤ
pr2 neg-i-ℤ[i] = neg-one-ℤ


add-ℤ[i] : ℤ[i] → ℤ[i] → ℤ[i]
pr1 (add-ℤ[i] (a , b) (a' , b')) = a +ℤ a'
pr2 (add-ℤ[i] (a , b) (a' , b')) = b +ℤ b'

infixl 35 _+ℤ[i]_

{x x' y y' : ℤ[i]} → x ＝ x' → y ＝ y' → x +ℤ[i] y ＝ x' +ℤ[i] y'


### Negatives of Gaussian integers

neg-ℤ[i] : ℤ[i] → ℤ[i]
pr1 (neg-ℤ[i] (a , b)) = neg-ℤ a
pr2 (neg-ℤ[i] (a , b)) = neg-ℤ b


### Multiplication of Gaussian integers

mul-ℤ[i] : ℤ[i] → ℤ[i] → ℤ[i]
pr1 (mul-ℤ[i] (a , b) (a' , b')) = (a *ℤ a') -ℤ (b *ℤ b')
pr2 (mul-ℤ[i] (a , b) (a' , b')) = (a *ℤ b') +ℤ (a' *ℤ b)

infixl 40 _*ℤ[i]_
_*ℤ[i]_ = mul-ℤ[i]

ap-mul-ℤ[i] :
{x x' y y' : ℤ[i]} → x ＝ x' → y ＝ y' → x *ℤ[i] y ＝ x' *ℤ[i] y'
ap-mul-ℤ[i] p q = ap-binary mul-ℤ[i] p q


### Conjugation of Gaussian integers

conjugate-ℤ[i] : ℤ[i] → ℤ[i]
pr1 (conjugate-ℤ[i] (a , b)) = a
pr2 (conjugate-ℤ[i] (a , b)) = neg-ℤ b


### The Gaussian integers form a commutative ring

left-unit-law-add-ℤ[i] : (x : ℤ[i]) → zero-ℤ[i] +ℤ[i] x ＝ x
left-unit-law-add-ℤ[i] (a , b) = eq-Eq-ℤ[i] refl refl

right-unit-law-add-ℤ[i] : (x : ℤ[i]) → x +ℤ[i] zero-ℤ[i] ＝ x

(x y z : ℤ[i]) → (x +ℤ[i] y) +ℤ[i] z ＝ x +ℤ[i] (y +ℤ[i] z)
associative-add-ℤ[i] (a1 , b1) (a2 , b2) (a3 , b3) =

(x : ℤ[i]) → (neg-ℤ[i] x) +ℤ[i] x ＝ zero-ℤ[i]

(x : ℤ[i]) → x +ℤ[i] (neg-ℤ[i] x) ＝ zero-ℤ[i]

(x y : ℤ[i]) → x +ℤ[i] y ＝ y +ℤ[i] x
commutative-add-ℤ[i] (a , b) (a' , b') =

left-unit-law-mul-ℤ[i] : (x : ℤ[i]) → one-ℤ[i] *ℤ[i] x ＝ x
left-unit-law-mul-ℤ[i] (a , b) =
eq-Eq-ℤ[i]
( ap (b +ℤ_) (right-zero-law-mul-ℤ a) ∙ right-unit-law-add-ℤ b)

right-unit-law-mul-ℤ[i] : (x : ℤ[i]) → x *ℤ[i] one-ℤ[i] ＝ x
right-unit-law-mul-ℤ[i] (a , b) =
eq-Eq-ℤ[i]
( right-unit-law-mul-ℤ a)
( ap neg-ℤ (right-zero-law-mul-ℤ b))) ∙
( ap (_+ℤ b) (right-zero-law-mul-ℤ a))

commutative-mul-ℤ[i] :
(x y : ℤ[i]) → x *ℤ[i] y ＝ y *ℤ[i] x
commutative-mul-ℤ[i] (a , b) (c , d) =
eq-Eq-ℤ[i]
( ap-add-ℤ (commutative-mul-ℤ a c) (ap neg-ℤ (commutative-mul-ℤ b d)))
( commutative-add-ℤ (a *ℤ d) (c *ℤ b))

associative-mul-ℤ[i] :
(x y z : ℤ[i]) → (x *ℤ[i] y) *ℤ[i] z ＝ x *ℤ[i] (y *ℤ[i] z)
associative-mul-ℤ[i] (a , b) (c , d) (e , f) =
eq-Eq-ℤ[i]
( a *ℤ c)
( neg-one-ℤ *ℤ (b *ℤ d))
( e)) ∙
( associative-mul-ℤ a c e)
( ( associative-mul-ℤ neg-one-ℤ (b *ℤ d) e) ∙
( ap
( neg-one-ℤ *ℤ_)
( ( associative-mul-ℤ b d e) ∙
( ap (b *ℤ_) (commutative-mul-ℤ d e)))))))
( ( ap
( neg-ℤ)
( ( right-distributive-mul-add-ℤ (a *ℤ d) (c *ℤ b) f) ∙
( associative-mul-ℤ a d f)
( associative-mul-ℤ c b f)))) ∙
( neg-one-ℤ)
( a *ℤ (d *ℤ f))
( c *ℤ (b *ℤ f)))))) ∙
( a *ℤ (c *ℤ e))
( neg-ℤ (b *ℤ (e *ℤ d)))
( neg-ℤ (a *ℤ (d *ℤ f)))
( neg-ℤ (c *ℤ (b *ℤ f)))) ∙
( refl {x = a *ℤ (c *ℤ e)})
( inv
( right-negative-law-mul-ℤ a (d *ℤ f)))) ∙
( inv
( c *ℤ e)
( neg-ℤ (d *ℤ f)))))
( ( inv
( neg-one-ℤ)
( b *ℤ (e *ℤ d))
( c *ℤ (b *ℤ f)))) ∙
( ap neg-ℤ
( refl {x = b *ℤ (e *ℤ d)})
( ( ap (c *ℤ_) (commutative-mul-ℤ b f)) ∙
( ( inv (associative-mul-ℤ c f b)) ∙
( commutative-mul-ℤ (c *ℤ f) b)))) ∙
( ( inv
( e *ℤ d)
( c *ℤ f))) ∙
( ap
( b *ℤ_)
( commutative-add-ℤ (e *ℤ d) (c *ℤ f))))))))))
( a *ℤ c)
( neg-ℤ (b *ℤ d))
( f)) ∙
( ap
( ((a *ℤ c) *ℤ f) +ℤ_)
( left-negative-law-mul-ℤ (b *ℤ d) f)))
( ( left-distributive-mul-add-ℤ e (a *ℤ d) (c *ℤ b)) ∙
( ( commutative-mul-ℤ e (a *ℤ d)) ∙
( ( associative-mul-ℤ a d e) ∙
( ap (a *ℤ_) (commutative-mul-ℤ d e))))
( ( inv (associative-mul-ℤ e c b)) ∙
( ap (_*ℤ b) (commutative-mul-ℤ e c)))))) ∙
( (a *ℤ c) *ℤ f)
( neg-ℤ ((b *ℤ d) *ℤ f))
( a *ℤ (e *ℤ d))
( (c *ℤ e) *ℤ b)) ∙
( associative-mul-ℤ a c f)
( refl)) ∙
( inv (left-distributive-mul-add-ℤ a (c *ℤ f) (e *ℤ d))))
( ( ap
( neg-ℤ)
( ( associative-mul-ℤ b d f) ∙
( commutative-mul-ℤ b (d *ℤ f)))) ∙
( inv (left-negative-law-mul-ℤ (d *ℤ f) b)))
( refl)) ∙
( ( inv
( neg-ℤ (d *ℤ f))
( c *ℤ e) b))) ∙
( ap
( _*ℤ b)
( commutative-add-ℤ (neg-ℤ (d *ℤ f)) (c *ℤ e))))))))

(x y z : ℤ[i]) →
x *ℤ[i] (y +ℤ[i] z) ＝ (x *ℤ[i] y) +ℤ[i] (x *ℤ[i] z)
left-distributive-mul-add-ℤ[i] (a , b) (c , d) (e , f) =
eq-Eq-ℤ[i]
( ( ap neg-ℤ (left-distributive-mul-add-ℤ b d f)) ∙
( left-distributive-mul-add-ℤ neg-one-ℤ (b *ℤ d) (b *ℤ f)))) ∙
( a *ℤ c)
( a *ℤ e)
( neg-ℤ (b *ℤ d))
( neg-ℤ (b *ℤ f))))
( right-distributive-mul-add-ℤ c e b)) ∙
( a *ℤ d)
( a *ℤ f)
( c *ℤ b)
( e *ℤ b)))

(x y z : ℤ[i]) →
(x +ℤ[i] y) *ℤ[i] z ＝ (x *ℤ[i] z) +ℤ[i] (y *ℤ[i] z)
( commutative-mul-ℤ[i] (x +ℤ[i] y) z) ∙
( ( left-distributive-mul-add-ℤ[i] z x y) ∙
( ap-add-ℤ[i] (commutative-mul-ℤ[i] z x) (commutative-mul-ℤ[i] z y)))

ℤ[i]-Semigroup : Semigroup lzero
pr1 ℤ[i]-Semigroup = product-Set ℤ-Set ℤ-Set

ℤ[i]-Group : Group lzero
pr1 ℤ[i]-Group = ℤ[i]-Semigroup
pr1 (pr1 (pr2 ℤ[i]-Group)) = zero-ℤ[i]
pr1 (pr2 (pr1 (pr2 ℤ[i]-Group))) = left-unit-law-add-ℤ[i]
pr2 (pr2 (pr1 (pr2 ℤ[i]-Group))) = right-unit-law-add-ℤ[i]
pr1 (pr2 (pr2 ℤ[i]-Group)) = neg-ℤ[i]
pr1 (pr2 (pr2 (pr2 ℤ[i]-Group))) = left-inverse-law-add-ℤ[i]
pr2 (pr2 (pr2 (pr2 ℤ[i]-Group))) = right-inverse-law-add-ℤ[i]

ℤ[i]-Ab : Ab lzero
pr1 ℤ[i]-Ab = ℤ[i]-Group

ℤ[i]-Ring : Ring lzero
pr1 ℤ[i]-Ring = ℤ[i]-Ab
pr1 (pr1 (pr2 ℤ[i]-Ring)) = mul-ℤ[i]
pr2 (pr1 (pr2 ℤ[i]-Ring)) = associative-mul-ℤ[i]
pr1 (pr1 (pr2 (pr2 ℤ[i]-Ring))) = one-ℤ[i]
pr1 (pr2 (pr1 (pr2 (pr2 ℤ[i]-Ring)))) = left-unit-law-mul-ℤ[i]
pr2 (pr2 (pr1 (pr2 (pr2 ℤ[i]-Ring)))) = right-unit-law-mul-ℤ[i]
pr1 (pr2 (pr2 (pr2 ℤ[i]-Ring))) = left-distributive-mul-add-ℤ[i]
pr2 (pr2 (pr2 (pr2 ℤ[i]-Ring))) = right-distributive-mul-add-ℤ[i]

ℤ[i]-Commutative-Ring : Commutative-Ring lzero
pr1 ℤ[i]-Commutative-Ring = ℤ[i]-Ring
pr2 ℤ[i]-Commutative-Ring = commutative-mul-ℤ[i]