The ring of integers

Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2023-09-21.
Last modified on 2023-11-24.

module elementary-number-theory.ring-of-integers where
open import commutative-algebra.commutative-rings

open import elementary-number-theory.addition-integers
open import
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import
open import group-theory.homomorphisms-groups

open import ring-theory.homomorphisms-rings
open import ring-theory.initial-rings
open import ring-theory.integer-multiples-of-elements-rings
open import ring-theory.rings


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

ℤ-Commutative-Ring : Commutative-Ring lzero
pr1 ℤ-Commutative-Ring = ℤ-Ring
pr2 ℤ-Commutative-Ring = commutative-mul-ℤ


The integer multiples in ℤ-Ring coincide with multiplication in

is-mul-integer-multiple-ℤ-Ring :
  (k l : )  integer-multiple-Ring ℤ-Ring k l  mul-ℤ k l
is-mul-integer-multiple-ℤ-Ring (inl zero-ℕ) l =
  ( integer-multiple-neg-one-Ring ℤ-Ring l) 
  ( is-left-mul-neg-one-neg-ℤ l)
is-mul-integer-multiple-ℤ-Ring (inl (succ-ℕ k)) l =
  ( integer-multiple-pred-Ring ℤ-Ring (inl k) l) 
  ( ap
    ( λ t  right-subtraction-Ring ℤ-Ring t l)
    ( is-mul-integer-multiple-ℤ-Ring (inl k) l)) 
  ( commutative-add-ℤ (mul-ℤ (inl k) l) (neg-ℤ l)) 
  ( inv (left-predecessor-law-mul-ℤ (inl k) l))
is-mul-integer-multiple-ℤ-Ring (inr (inl _)) l =
  ( integer-multiple-zero-Ring ℤ-Ring l) 
  ( inv (left-zero-law-mul-ℤ l))
is-mul-integer-multiple-ℤ-Ring (inr (inr zero-ℕ)) l =
  ( integer-multiple-one-Ring ℤ-Ring l) 
  ( inv (left-unit-law-mul-ℤ l))
is-mul-integer-multiple-ℤ-Ring (inr (inr (succ-ℕ k))) l =
  ( integer-multiple-succ-Ring ℤ-Ring (inr (inr k)) l) 
  ( ap (add-ℤ' l) (is-mul-integer-multiple-ℤ-Ring (inr (inr k)) l)) 
  ( commutative-add-ℤ _ l) 
  ( inv (left-successor-law-mul-ℤ (inr (inr k)) l))

is-integer-multiple-ℤ :
  (k : )  integer-multiple-Ring ℤ-Ring k one-ℤ  k
is-integer-multiple-ℤ k =
  ( is-mul-integer-multiple-ℤ-Ring k one-ℤ) 
  ( right-unit-law-mul-ℤ k)

The ring of integers is the initial ring

The homomorphism from to a ring

module _
  {l1 : Level} (R : Ring l1)

  hom-group-initial-hom-Ring : hom-Group ℤ-Group (group-Ring R)
  hom-group-initial-hom-Ring = hom-element-Group (group-Ring R) (one-Ring R)

  map-initial-hom-Ring :   type-Ring R
  map-initial-hom-Ring =
    map-hom-Group ℤ-Group (group-Ring R) hom-group-initial-hom-Ring

  preserves-add-initial-hom-Ring :
    (k l : ) 
    map-initial-hom-Ring (add-ℤ k l) 
    add-Ring R (map-initial-hom-Ring k) (map-initial-hom-Ring l)
  preserves-add-initial-hom-Ring k l =
      ( ℤ-Group)
      ( group-Ring R)
      ( hom-group-initial-hom-Ring)
      { k}
      { l}

  preserves-one-initial-hom-Ring : map-initial-hom-Ring one-ℤ  one-Ring R
  preserves-one-initial-hom-Ring = integer-multiple-one-Ring R (one-Ring R)

  preserves-mul-initial-hom-Ring :
    (k l : ) 
    map-initial-hom-Ring (mul-ℤ k l) 
    mul-Ring R (map-initial-hom-Ring k) (map-initial-hom-Ring l)
  preserves-mul-initial-hom-Ring k l =
    ( ap map-initial-hom-Ring (commutative-mul-ℤ k l)) 
    ( integer-multiple-mul-Ring R l k (one-Ring R)) 
    ( ap (integer-multiple-Ring R l) (inv (right-unit-law-mul-Ring R _))) 
    ( inv (right-integer-multiple-law-mul-Ring R l _ _))

  initial-hom-Ring : hom-Ring ℤ-Ring R
  pr1 initial-hom-Ring = hom-group-initial-hom-Ring
  pr1 (pr2 initial-hom-Ring) {x} {y} = preserves-mul-initial-hom-Ring x y
  pr2 (pr2 initial-hom-Ring) = preserves-one-initial-hom-Ring

Any ring homomorphisms from to R is equal to the homomorphism initial-hom-Ring

module _
  {l : Level} (R : Ring l)

  htpy-initial-hom-Ring :
    (f : hom-Ring ℤ-Ring R)  htpy-hom-Ring ℤ-Ring R (initial-hom-Ring R) f
  htpy-initial-hom-Ring f k =
    ( inv
      ( ( preserves-integer-multiples-hom-Ring ℤ-Ring R f k one-ℤ) 
        ( ap
          ( integer-multiple-Ring R k)
          ( preserves-one-hom-Ring ℤ-Ring R f)))) 
    ( ap (map-hom-Ring ℤ-Ring R f) (is-integer-multiple-ℤ k))

  contraction-initial-hom-Ring :
    (f : hom-Ring ℤ-Ring R)  initial-hom-Ring R  f
  contraction-initial-hom-Ring f =
    eq-htpy-hom-Ring ℤ-Ring R (initial-hom-Ring R) f (htpy-initial-hom-Ring f)

The ring of integers is the initial ring

is-initial-ℤ-Ring : is-initial-Ring ℤ-Ring
pr1 (is-initial-ℤ-Ring S) = initial-hom-Ring S
pr2 (is-initial-ℤ-Ring S) f = contraction-initial-hom-Ring S f

Integer multiplication in the ring of integers coincides with multiplication of integers

integer-multiple-one-ℤ-Ring :
  (k : )  integer-multiple-Ring ℤ-Ring k one-ℤ  k
integer-multiple-one-ℤ-Ring (inl zero-ℕ) = refl
integer-multiple-one-ℤ-Ring (inl (succ-ℕ n)) =
  ap pred-ℤ (integer-multiple-one-ℤ-Ring (inl n))
integer-multiple-one-ℤ-Ring (inr (inl _)) = refl
integer-multiple-one-ℤ-Ring (inr (inr zero-ℕ)) = refl
integer-multiple-one-ℤ-Ring (inr (inr (succ-ℕ n))) =
  ap succ-ℤ (integer-multiple-one-ℤ-Ring (inr (inr n)))

compute-integer-multiple-ℤ-Ring :
  (k l : )  integer-multiple-Ring ℤ-Ring k l  mul-ℤ k l
compute-integer-multiple-ℤ-Ring k l =
    integer-multiple-Ring ℤ-Ring k l
     integer-multiple-Ring ℤ-Ring k (integer-multiple-Ring ℤ-Ring l one-ℤ)
        ( integer-multiple-Ring ℤ-Ring k)
        ( inv (integer-multiple-one-ℤ-Ring l))
     integer-multiple-Ring ℤ-Ring (mul-ℤ k l) one-ℤ
      inv (integer-multiple-mul-Ring ℤ-Ring k l one-ℤ)
     mul-ℤ k l
      integer-multiple-one-ℤ-Ring _

Recent changes