On the Characteristic of a Ring

I was reading the section on the characteristic of a field in my textbook.

In the Textbook

The definition goes something like this:

Let be the natural homomorphism from to a field .

• If $Ker(\phi) = (0)$, the characteristic is $0$.

• If $p$ is a prime number and $Ker(\phi) = p\Z$, the characteristic is $p$.

In mathlib

I tried looking for it in mathlib (with some help from an LLM), and found this:

class _root_.CharP (R : Type*) [AddMonoidWithOne R] (p : outParam ℕ) : Prop where
  cast_eq_zero_iff (R p) : ∀ x : ℕ, (x : R) = 0 ↔ p ∣ x

It seems this is how it’s defined.

But… this looks quite different from the textbook definition.

Neither $Ker$ nor $p\Z$ makes an appearance here. Maybe this is just a “classic mathlib moment.”

Defining Characteristic Following the Textbook

Just to see, I tried defining it myself while following the textbook as closely as possible (again, with some help from an LLM):

import Mathlib.RingTheory.Ideal.Maps

class CharP (K : Type) [Ring K] (p : ℕ) : Prop where
  kernel_eq_span : RingHom.ker (Int.castRingHom K) = Ideal.span { (p : ℤ) }

And… it compiled without errors!

Though, I still feel like I might not fully grasp everything yet…

Notes on the Textbook-Style Definition

It seems RingHom.ker (Int.castRingHom K) corresponds to .

As for the Ideal.span part:

• Ideal.span {(p : ℤ)} is the set of all multiples of (i.e., ).
• Ideal.span {(0 : ℤ)} is the ideal generated by , which is .

It turns out you don’t actually need to write a separate case for “If it is …”. The single expression covers both!

That’s all for today!