Characteristics of rings

Content created by Egbert Rijke and Gregor Perčič.

Created on 2023-09-21.
Last modified on 2025-10-31.

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)

Recent changes