The Gaussian integers

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

Created on 2022-04-22.
Last modified on 2024-02-06.

module commutative-algebra.gaussian-integers where
Imports 
open import commutative-algebra.commutative-rings

open import elementary-number-theory.addition-integers
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-ℤ

Addition of Gaussian integers

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]_
_+ℤ[i]_ = add-ℤ[i]

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

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
right-unit-law-add-ℤ[i] (a , b) =
  eq-Eq-ℤ[i] (right-unit-law-add-ℤ a) (right-unit-law-add-ℤ b)

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

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

right-inverse-law-add-ℤ[i] :
  (x : ℤ[i]) → x +ℤ[i] (neg-ℤ[i] x) ＝ zero-ℤ[i]
right-inverse-law-add-ℤ[i] (a , b) =
  eq-Eq-ℤ[i] (right-inverse-law-add-ℤ a) (right-inverse-law-add-ℤ b)

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

left-unit-law-mul-ℤ[i] : (x : ℤ[i]) → one-ℤ[i] *ℤ[i] x ＝ x
left-unit-law-mul-ℤ[i] (a , b) =
  eq-Eq-ℤ[i]
    ( right-unit-law-add-ℤ a)
    ( 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]
    ( ( ap-add-ℤ
        ( right-unit-law-mul-ℤ a)
        ( ap neg-ℤ (right-zero-law-mul-ℤ b))) ∙
      ( right-unit-law-add-ℤ a))
    ( 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]
    ( ( ap-add-ℤ
        ( ( right-distributive-mul-add-ℤ
            ( a *ℤ c)
            ( neg-one-ℤ *ℤ (b *ℤ d))
            ( e)) ∙
          ( ap-add-ℤ
            ( 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) ∙
              ( ap-add-ℤ
                ( associative-mul-ℤ a d f)
                ( associative-mul-ℤ c b f)))) ∙
          ( ( left-distributive-mul-add-ℤ
              ( neg-one-ℤ)
              ( a *ℤ (d *ℤ f))
              ( c *ℤ (b *ℤ f)))))) ∙
      ( ( interchange-law-add-add-ℤ
          ( a *ℤ (c *ℤ e))
          ( neg-ℤ (b *ℤ (e *ℤ d)))
          ( neg-ℤ (a *ℤ (d *ℤ f)))
          ( neg-ℤ (c *ℤ (b *ℤ f)))) ∙
        ( ap-add-ℤ
          ( ( ap-add-ℤ
              ( refl {x = a *ℤ (c *ℤ e)})
              ( inv
                ( right-negative-law-mul-ℤ a (d *ℤ f)))) ∙
            ( inv
              ( left-distributive-mul-add-ℤ a
                ( c *ℤ e)
                ( neg-ℤ (d *ℤ f)))))
          ( ( inv
              ( left-distributive-mul-add-ℤ
                ( neg-one-ℤ)
                ( b *ℤ (e *ℤ d))
                ( c *ℤ (b *ℤ f)))) ∙
            ( ap neg-ℤ
              ( ( ap-add-ℤ
                  ( refl {x = b *ℤ (e *ℤ d)})
                  ( ( ap (c *ℤ_) (commutative-mul-ℤ b f)) ∙
                    ( ( inv (associative-mul-ℤ c f b)) ∙
                      ( commutative-mul-ℤ (c *ℤ f) b)))) ∙
                ( ( inv
                    ( left-distributive-mul-add-ℤ b
                      ( e *ℤ d)
                      ( c *ℤ f))) ∙
                  ( ap
                    ( b *ℤ_)
                    ( commutative-add-ℤ (e *ℤ d) (c *ℤ f))))))))))
    ( ( ap-add-ℤ
        ( ( right-distributive-mul-add-ℤ
            ( 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)) ∙
          ( ap-add-ℤ
            ( ( 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)))))) ∙
      ( ( interchange-law-add-add-ℤ
          ( (a *ℤ c) *ℤ f)
          ( neg-ℤ ((b *ℤ d) *ℤ f))
          ( a *ℤ (e *ℤ d))
          ( (c *ℤ e) *ℤ b)) ∙
        ( ap-add-ℤ
          ( ( ap-add-ℤ
              ( associative-mul-ℤ a c f)
              ( refl)) ∙
            ( inv (left-distributive-mul-add-ℤ a (c *ℤ f) (e *ℤ d))))
          ( ( ap-add-ℤ
              ( ( ap
                  ( neg-ℤ)
                  ( ( associative-mul-ℤ b d f) ∙
                    ( commutative-mul-ℤ b (d *ℤ f)))) ∙
                ( inv (left-negative-law-mul-ℤ (d *ℤ f) b)))
              ( refl)) ∙
            ( ( inv
                ( ( right-distributive-mul-add-ℤ
                    ( neg-ℤ (d *ℤ f))
                    ( c *ℤ e) b))) ∙
              ( ap
                ( _*ℤ b)
                ( commutative-add-ℤ (neg-ℤ (d *ℤ f)) (c *ℤ e))))))))

left-distributive-mul-add-ℤ[i] :
  (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-add-ℤ
        ( left-distributive-mul-add-ℤ a c e)
        ( ( ap neg-ℤ (left-distributive-mul-add-ℤ b d f)) ∙
          ( left-distributive-mul-add-ℤ neg-one-ℤ (b *ℤ d) (b *ℤ f)))) ∙
      ( interchange-law-add-add-ℤ
        ( a *ℤ c)
        ( a *ℤ e)
        ( neg-ℤ (b *ℤ d))
        ( neg-ℤ (b *ℤ f))))
    ( ( ap-add-ℤ
        ( left-distributive-mul-add-ℤ a d f)
        ( right-distributive-mul-add-ℤ c e b)) ∙
      ( interchange-law-add-add-ℤ
        ( a *ℤ d)
        ( a *ℤ f)
        ( c *ℤ b)
        ( e *ℤ b)))

right-distributive-mul-add-ℤ[i] :
  (x y z : ℤ[i]) →
  (x +ℤ[i] y) *ℤ[i] z ＝ (x *ℤ[i] z) +ℤ[i] (y *ℤ[i] z)
right-distributive-mul-add-ℤ[i] x y 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
pr1 (pr2 ℤ[i]-Semigroup) = add-ℤ[i]
pr2 (pr2 ℤ[i]-Semigroup) = associative-add-ℤ[i]

ℤ[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
pr2 ℤ[i]-Ab = commutative-add-ℤ[i]

ℤ[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]

Recent changes