This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Characteristics of rings

module ring-theory.characteristics-rings where

Imports

open import elementary-number-theory.ring-of-integers

open import foundation.universe-levels

open import ring-theory.ideals-rings
open import ring-theory.kernels-of-ring-homomorphisms
open import ring-theory.rings

Idea

The characteristic of a ring R is defined to be the kernel of the initial ring homomorphism from the ring ℤ of integers to R.

Definitions

Characteristics of rings

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

  characteristic-Ring : ideal-Ring l ℤ-Ring
  characteristic-Ring = kernel-hom-Ring ℤ-Ring R (initial-hom-Ring R)