Mathlib.Algebra.CharP.Defs

CharP structure

(R : Type*) [AddMonoidWithOne R] (p : semiOutParam ℕ)

Full source

/-- The generator of the kernel of the unique homomorphism ℕ → R for a semiring R.

*Warning*: for a semiring `R`, `CharP R 0` and `CharZero R` need not coincide.
* `CharP R 0` asks that only `0 : ℕ` maps to `0 : R` under the map `ℕ → R`;
* `CharZero R` requires an injection `ℕ ↪ R`.

For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
`CharZero {0, 1}` does not hold and yet `CharP {0, 1} 0` does.
This example is formalized in `Counterexamples/CharPZeroNeCharZero.lean`.
-/
@[mk_iff]
class _root_.CharP (R : Type*) [AddMonoidWithOne R] (p : semiOutParam ℕ) : Prop where
  cast_eq_zero_iff (R p) : ∀ x : ℕ, (x : R) = 0 ↔ p ∣ x

Characteristic of a Semiring

Informal description

The structure `CharP R p` expresses that the semiring (or additive monoid with one) $R$ has characteristic $p$, meaning that the unique homomorphism from the natural numbers to $R$ has kernel generated by $p$. *Warning*: For a semiring $R$, `CharP R 0` and `CharZero R` do not necessarily coincide. Specifically: - `CharP R 0` means that only $0 \in \mathbb{N}$ maps to $0 \in R$ under the canonical homomorphism $\mathbb{N} \to R$. - `CharZero R` requires that the canonical homomorphism $\mathbb{N} \to R$ is injective. For example, the semiring $\{0, 1\}$ with addition defined by the maximum operation (where $1$ is absorbing) satisfies `CharP \{0, 1\} 0` but not `CharZero \{0, 1\}`.

CharP.cast_eq_zero_iff' theorem

(R : Type*) [AddMonoidWithOne R] (p : ℕ) [CharP R p] (a : ℕ) : (a : R) = 0 ↔ p ∣ a

Full source

@[deprecated CharP.cast_eq_zero_iff (since := "2025-04-03")]
lemma cast_eq_zero_iff' (R : Type*) [AddMonoidWithOne R] (p : ℕ) [CharP R p] (a : ℕ) :
    (a : R) = 0 ↔ p ∣ a := cast_eq_zero_iff R p a

Characteristic Divisibility Criterion: $(a : R) = 0 \leftrightarrow p \mid a$

Informal description

Let $R$ be an additive monoid with one and characteristic $p$. For any natural number $a$, the canonical image of $a$ in $R$ is zero if and only if $p$ divides $a$. In other words, $(a : R) = 0 \leftrightarrow p \mid a$.

CharP.ofNat_eq_zero' theorem

(p : ℕ) [CharP R p] (a : ℕ) [a.AtLeastTwo] (h : p ∣ a) : (ofNat(a) : R) = 0

Full source

lemma _root_.CharP.ofNat_eq_zero' (p : ℕ) [CharP R p]
    (a : ℕ) [a.AtLeastTwo] (h : p ∣ a) :
    (ofNat(a) : R) = 0 := by
  rwa [← CharP.cast_eq_zero_iff R p] at h

Characteristic Divides Implies Zero for Numerals ≥ 2

Informal description

Let $R$ be an additive monoid with one of characteristic $p$. For any natural number $a \geq 2$ such that $p$ divides $a$, the canonical image of $a$ in $R$ is zero, i.e., $a = 0$ in $R$.

CharP.congr theorem

{q : ℕ} (h : p = q) : CharP R q

Full source

lemma congr {q : ℕ} (h : p = q) : CharP R q := h ▸ ‹CharP R p›

Characteristic Preservation Under Equality

Informal description

Let $R$ be an additive monoid with one and let $p$ be a natural number. If $R$ has characteristic $p$ and $p = q$ for some natural number $q$, then $R$ also has characteristic $q$.

CharP.cast_eq_zero theorem

: (p : R) = 0

Full source

@[simp] lemma cast_eq_zero : (p : R) = 0 := (cast_eq_zero_iff R p p).2 dvd_rfl

Characteristic implies $p = 0$ in $R$

Informal description

Let $R$ be an additive monoid with one of characteristic $p$. Then the canonical image of $p$ in $R$ is zero, i.e., $p = 0$ in $R$.

CharP.ofNat_eq_zero theorem

[p.AtLeastTwo] : (ofNat(p) : R) = 0

Full source

lemma ofNat_eq_zero [p.AtLeastTwo] : (ofNat(p) : R) = 0 := cast_eq_zero R p

Characteristic $p$ implies $p = 0$ for numerals $\geq 2$ in $R$

Informal description

Let $R$ be an additive monoid with one of characteristic $p$, where $p \geq 2$ is a natural number. Then the canonical image of $p$ in $R$ is zero, i.e., $\text{ofNat}(p) = 0$ in $R$.

CharP.eq theorem

{p q : ℕ} (_hp : CharP R p) (_hq : CharP R q) : p = q

Full source

lemma eq {p q : ℕ} (_hp : CharP R p) (_hq : CharP R q) : p = q :=
  Nat.dvd_antisymm ((cast_eq_zero_iff R p q).1 (cast_eq_zero _ _))
    ((cast_eq_zero_iff R q p).1 (cast_eq_zero _ _))

Uniqueness of Characteristic in Additive Monoids with One

Informal description

For any additive monoid with one $R$ and natural numbers $p$ and $q$, if $R$ has characteristic $p$ and characteristic $q$, then $p = q$.

CharP.ofCharZero instance

[CharZero R] : CharP R 0

Full source

instance ofCharZero [CharZero R] : CharP R 0 where
  cast_eq_zero_iff x := by rw [zero_dvd_iff, ← Nat.cast_zero, Nat.cast_inj]

Characteristic Zero Implies CharP Zero

Informal description

For any additive monoid with one $R$ of characteristic zero, $R$ has characteristic $0$ as a semiring.

CharP.intCast_eq_zero_iff theorem

(a : ℤ) : (a : R) = 0 ↔ (p : ℤ) ∣ a

Full source

lemma intCast_eq_zero_iff (a : ℤ) : (a : R) = 0 ↔ (p : ℤ) ∣ a := by
  rcases lt_trichotomy a 0 with (h | rfl | h)
  · rw [← neg_eq_zero, ← Int.cast_neg, ← Int.dvd_neg]
    lift -a to ℕ using Int.neg_nonneg.mpr (le_of_lt h) with b
    rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]
  · simp only [Int.cast_zero, eq_self_iff_true, Int.dvd_zero]
  · lift a to ℕ using le_of_lt h with b
    rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]

Characteristic Condition for Integer Coercion: $a = 0 \leftrightarrow p \mid a$

Informal description

Let $R$ be a semiring with characteristic $p$. For any integer $a \in \mathbb{Z}$, the canonical homomorphism $\mathbb{Z} \to R$ maps $a$ to zero if and only if $p$ divides $a$ in $\mathbb{Z}$. In other words, $a = 0$ in $R$ if and only if $p \mid a$.

CharP.charP_to_charZero theorem

[CharP R 0] : CharZero R

Full source

lemma charP_to_charZero [CharP R 0] : CharZero R :=
  charZero_of_inj_zero fun n h0 => eq_zero_of_zero_dvd ((cast_eq_zero_iff R 0 n).mp h0)

Characteristic Zero Implies Injective Natural Number Homomorphism

Informal description

If a semiring $R$ has characteristic $0$ (i.e., $\text{CharP}\,R\,0$ holds), then the canonical homomorphism from the natural numbers to $R$ is injective (i.e., $R$ satisfies $\text{CharZero}\,R$).

CharP.charP_zero_iff_charZero theorem

: CharP R 0 ↔ CharZero R

Full source

lemma charP_zero_iff_charZero : CharPCharP R 0 ↔ CharZero R :=
  ⟨fun _ ↦ charP_to_charZero R, fun _ ↦ ofCharZero R⟩

Characteristic Zero Equivalence: $\text{CharP}\,R\,0$ iff $\text{CharZero}\,R$

Informal description

For any additive monoid with one $R$, the following are equivalent: 1. $R$ has characteristic zero as a semiring (i.e., $\text{CharP}\,R\,0$ holds). 2. The canonical homomorphism from the natural numbers to $R$ is injective (i.e., $\text{CharZero}\,R$ holds).

CharP.exists theorem

: ∃ p, CharP R p

Full source

lemma «exists» : ∃ p, CharP R p :=
  letI := Classical.decEq R
  by_cases
    (fun H : ∀ p : ℕ, (p : R) = 0 → p = 0 =>
      ⟨0, ⟨fun x => by rw [zero_dvd_iff]; exact ⟨H x, by rintro rfl; simp⟩⟩⟩)
    fun H =>
    ⟨Nat.find (not_forall.1 H),
      ⟨fun x =>
        ⟨fun H1 =>
          Nat.dvd_of_mod_eq_zero
            (by_contradiction fun H2 =>
              Nat.find_min (not_forall.1 H)
                (Nat.mod_lt x <|
                  Nat.pos_of_ne_zero <| not_of_not_imp <| Nat.find_spec (not_forall.1 H))
                (not_imp_of_and_not
                  ⟨by
                    rwa [← Nat.mod_add_div x (Nat.find (not_forall.1 H)), Nat.cast_add,
                      Nat.cast_mul,
                      of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
                      zero_mul, add_zero] at H1,
                    H2⟩)),
          fun H1 => by
          rw [← Nat.mul_div_cancel' H1, Nat.cast_mul,
            of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
            zero_mul]⟩⟩⟩

Existence of Characteristic for Semirings

Informal description

For any semiring (or additive monoid with one) $R$, there exists a natural number $p$ such that $R$ has characteristic $p$, meaning the unique homomorphism $\mathbb{N} \to R$ has kernel generated by $p$.

CharP.existsUnique theorem

: ∃! p, CharP R p

Full source

lemma existsUnique : ∃! p, CharP R p :=
  let ⟨c, H⟩ := CharP.exists R
  ⟨c, H, fun _y H2 => CharP.eq R H2 H⟩

Uniqueness of Characteristic for Semirings

Informal description

For any semiring (or additive monoid with one) $R$, there exists a unique natural number $p$ such that $R$ has characteristic $p$, meaning the unique homomorphism $\mathbb{N} \to R$ has kernel generated by $p$.

ringChar definition

[NonAssocSemiring R] : ℕ

Full source

/-- Noncomputable function that outputs the unique characteristic of a semiring. -/
noncomputable def ringChar [NonAssocSemiring R] : ℕ := Classical.choose (CharP.existsUnique R)

Characteristic of a semiring

Informal description

The characteristic of a semiring $R$ is the unique natural number $p$ such that for any natural number $x$, the canonical image of $x$ in $R$ is zero if and only if $p$ divides $x$. This is equivalent to saying that the kernel of the canonical homomorphism $\mathbb{N} \to R$ is generated by $p$.

ringChar.spec theorem

: ∀ x : ℕ, (x : R) = 0 ↔ ringChar R ∣ x

Full source

lemma spec : ∀ x : ℕ, (x : R) = 0 ↔ ringChar R ∣ x := by
  letI : CharP R (ringChar R) := (Classical.choose_spec (CharP.existsUnique R)).1
  exact CharP.cast_eq_zero_iff R (ringChar R)

Characteristic Divisibility Criterion for Semirings

Informal description

For any natural number $x$, the canonical image of $x$ in a semiring $R$ is zero if and only if the characteristic of $R$ divides $x$. In other words, $(x : R) = 0 \leftrightarrow \text{ringChar}(R) \mid x$.

ringChar.eq theorem

(p : ℕ) [C : CharP R p] : ringChar R = p

Full source

lemma eq (p : ℕ) [C : CharP R p] : ringChar R = p :=
  ((Classical.choose_spec (CharP.existsUnique R)).2 p C).symm

Characteristic Equality: $\text{ringChar}\, R = p$ when $R$ has characteristic $p$

Informal description

For any semiring $R$ and natural number $p$, if $R$ has characteristic $p$ (i.e., $\text{CharP}\, R\, p$ holds), then the ring characteristic of $R$ equals $p$, i.e., $\text{ringChar}\, R = p$.

ringChar.charP instance

: CharP R (ringChar R)

Full source

instance charP : CharP R (ringChar R) :=
  ⟨spec R⟩

Characteristic Property of a Semiring's Ring Characteristic

Informal description

For any semiring $R$, the characteristic of $R$ (as defined by `ringChar R`) satisfies the `CharP` property. That is, the canonical homomorphism from the natural numbers to $R$ has kernel generated by $\text{ringChar}(R)$.

ringChar.of_eq theorem

{p : ℕ} (h : ringChar R = p) : CharP R p

Full source

lemma of_eq {p : ℕ} (h : ringChar R = p) : CharP R p :=
  CharP.congr (ringChar R) h

Characteristic from Ring Characteristic Equality: $\text{ringChar}\, R = p$ implies $\text{CharP}\, R\, p$

Informal description

For any semiring $R$ and natural number $p$, if the ring characteristic of $R$ equals $p$ (i.e., $\text{ringChar}\, R = p$), then $R$ has characteristic $p$ (i.e., $\text{CharP}\, R\, p$ holds).

ringChar.dvd theorem

{x : ℕ} (hx : (x : R) = 0) : ringChar R ∣ x

Full source

lemma dvd {x : ℕ} (hx : (x : R) = 0) : ringCharringChar R ∣ x :=
  (spec R x).1 hx

Characteristic Divides Natural Number When Image is Zero

Informal description

For any natural number $x$, if the canonical image of $x$ in a semiring $R$ is zero (i.e., $(x : R) = 0$), then the characteristic of $R$ divides $x$ (i.e., $\text{ringChar}(R) \mid x$).

ringChar.Nat.cast_ringChar theorem

: (ringChar R : R) = 0

Full source

lemma Nat.cast_ringChar : (ringChar R : R) = 0 := by rw [ringChar.spec]

Characteristic Vanishes in Semiring: $(\text{ringChar}(R) : R) = 0$

Informal description

For any semiring $R$, the canonical image of its characteristic $\text{ringChar}(R)$ in $R$ is equal to zero, i.e., $(\text{ringChar}(R) : R) = 0$.

CharP.neg_one_ne_one theorem

[AddGroupWithOne R] (p : ℕ) [CharP R p] [Fact (2 < p)] : (-1 : R) ≠ (1 : R)

Full source

lemma CharP.neg_one_ne_one [AddGroupWithOne R] (p : ℕ) [CharP R p] [Fact (2 < p)] :
    (-1 : R) ≠ (1 : R) := by
  rw [ne_comm, ← sub_ne_zero, sub_neg_eq_add, one_add_one_eq_two, ← Nat.cast_two, Ne,
    CharP.cast_eq_zero_iff R p 2]
  exact fun h ↦ (Fact.out : 2 < p).not_le <| Nat.le_of_dvd Nat.zero_lt_two h

Distinctness of Negated and Positive Unity in Characteristic Greater Than Two

Informal description

Let $R$ be an additive group with one of characteristic $p$, where $p > 2$. Then $-1 \neq 1$ in $R$.

CharP.cast_eq_mod theorem

(p : ℕ) [CharP R p] (k : ℕ) : (k : R) = (k % p : ℕ)

Full source

lemma cast_eq_mod (p : ℕ) [CharP R p] (k : ℕ) : (k : R) = (k % p : ℕ) :=
  calc
    (k : R) = ↑(k % p + p * (k / p)) := by rw [Nat.mod_add_div]
    _ = ↑(k % p) := by simp [cast_eq_zero]

Canonical Image Modulo Characteristic: $(k : R) = (k \bmod p : \mathbb{N})$

Informal description

Let $R$ be a semiring with characteristic $p$. For any natural number $k$, the canonical image of $k$ in $R$ is equal to the canonical image of $k \bmod p$ in $R$, i.e., $(k : R) = (k \bmod p : \mathbb{N})$.

CharP.ringChar_zero_iff_CharZero theorem

: ringChar R = 0 ↔ CharZero R

Full source

lemma ringChar_zero_iff_CharZero : ringCharringChar R = 0 ↔ CharZero R := by
  rw [ringChar.eq_iff, charP_zero_iff_charZero]

Characteristic Zero Equivalence: $\mathrm{ringChar}\,R = 0$ iff $\mathrm{CharZero}\,R$

Informal description

For any semiring $R$, the ring characteristic $\mathrm{ringChar}\,R$ is zero if and only if $R$ has characteristic zero (i.e., the canonical homomorphism $\mathbb{N} \to R$ is injective).

CharP.char_ne_one theorem

[Nontrivial R] (p : ℕ) [hc : CharP R p] : p ≠ 1

Full source

lemma char_ne_one [Nontrivial R] (p : ℕ) [hc : CharP R p] : p ≠ 1 := fun hp : p = 1 =>
  have : (1 : R) = 0 := by simpa using (cast_eq_zero_iff R p 1).mpr (hp ▸ dvd_refl p)
  absurd this one_ne_zero

Characteristic of Nontrivial Semiring is Not One

Informal description

For a nontrivial semiring $R$ with characteristic $p$, the characteristic $p$ cannot be equal to $1$.

CharP.char_is_prime_of_two_le theorem

(p : ℕ) [CharP R p] (hp : 2 ≤ p) : Nat.Prime p

Full source

lemma char_is_prime_of_two_le (p : ℕ) [CharP R p] (hp : 2 ≤ p) : Nat.Prime p :=
  suffices ∀ (d) (_ : d ∣ p), d = 1 ∨ d = p from Nat.prime_def.mpr ⟨hp, this⟩
  fun (d : ℕ) (hdvd : ∃ e, p = d * e) =>
  let ⟨e, hmul⟩ := hdvd
  have : (p : R) = 0 := (cast_eq_zero_iff R p p).mpr (dvd_refl p)
  have : (d : R) * e = 0 := @Nat.cast_mul R _ d e ▸ hmul ▸ this
  Or.elim (eq_zero_or_eq_zero_of_mul_eq_zero this)
    (fun hd : (d : R) = 0 =>
      have : p ∣ d := (cast_eq_zero_iff R p d).mp hd
      show d = 1 ∨ d = p from Or.inr (this.antisymm' ⟨e, hmul⟩))
    fun he : (e : R) = 0 =>
    have : p ∣ e := (cast_eq_zero_iff R p e).mp he
    have : e ∣ p := dvd_of_mul_left_eq d (Eq.symm hmul)
    have : e = p := ‹e ∣ p›.antisymm ‹p ∣ e›
    have h₀ : 0 < p := by omega
    have : d * p = 1 * p := by rw [‹e = p›] at hmul; rw [one_mul]; exact Eq.symm hmul
    show d = 1 ∨ d = p from Or.inl (mul_right_cancel₀ h₀.ne' this)

Characteristic $\geq 2$ implies prime characteristic

Informal description

For any semiring $R$ with characteristic $p \geq 2$, the characteristic $p$ is a prime number.

CharP.char_is_prime_or_zero theorem

(p : ℕ) [hc : CharP R p] : Nat.Prime p ∨ p = 0

Full source

lemma char_is_prime_or_zero (p : ℕ) [hc : CharP R p] : Nat.PrimeNat.Prime p ∨ p = 0 :=
  match p, hc with
  | 0, _ => Or.inr rfl
  | 1, hc => absurd (Eq.refl (1 : ℕ)) (@char_ne_one R _ _ (1 : ℕ) hc)
  | m + 2, hc => Or.inl (@char_is_prime_of_two_le R _ _ (m + 2) hc (Nat.le_add_left 2 m))

Characteristic is Prime or Zero

Informal description

For any semiring $R$ with characteristic $p$, either $p$ is a prime number or $p = 0$.

CharP.char_prime_of_ne_zero theorem

{p : ℕ} [CharP R p] (hp : p ≠ 0) : p.Prime

Full source

/-- The characteristic is prime if it is non-zero. -/
lemma char_prime_of_ne_zero {p : ℕ} [CharP R p] (hp : p ≠ 0) : p.Prime :=
  (CharP.char_is_prime_or_zero R p).resolve_right hp

Nonzero Characteristic Implies Prime Characteristic

Informal description

For any semiring $R$ with characteristic $p \neq 0$, the characteristic $p$ is a prime number.

CharP.exists' theorem

(R : Type*) [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] : CharZero R ∨ ∃ p : ℕ, Fact p.Prime ∧ CharP R p

Full source

lemma exists' (R : Type*) [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] :
    CharZeroCharZero R ∨ ∃ p : ℕ, Fact p.Prime ∧ CharP R p := by
  obtain ⟨p, hchar⟩ := CharP.exists R
  rcases char_is_prime_or_zero R p with h | rfl
  exacts [Or.inr ⟨p, Fact.mk h, hchar⟩, Or.inl (charP_to_charZero R)]

Characteristic of Nontrivial Rings Without Zero Divisors is Zero or Prime

Informal description

Let $R$ be a nontrivial non-associative ring without zero divisors. Then either: 1. The canonical homomorphism $\mathbb{N} \to R$ is injective (i.e., $R$ has characteristic zero), or 2. There exists a prime number $p$ such that $R$ has characteristic $p$.

CharP.char_is_prime_of_pos theorem

(p : ℕ) [NeZero p] [CharP R p] : Fact p.Prime

Full source

lemma char_is_prime_of_pos (p : ℕ) [NeZero p] [CharP R p] : Fact p.Prime :=
  ⟨(CharP.char_is_prime_or_zero R _).resolve_right <| NeZero.ne p⟩

Nonzero Characteristic Implies Prime Characteristic

Informal description

For any semiring $R$ with characteristic $p \neq 0$, the characteristic $p$ is a prime number.

CharP.CharOne.subsingleton theorem

[CharP R 1] : Subsingleton R

Full source

lemma CharOne.subsingleton [CharP R 1] : Subsingleton R :=
  Subsingleton.intro <|
    suffices ∀ r : R, r = 0 from fun a b => show a = b by rw [this a, this b]
    fun r =>
    calc
      r = 1 * r := by rw [one_mul]
      _ = (1 : ℕ) * r := by rw [Nat.cast_one]
      _ = 0 * r := by rw [CharP.cast_eq_zero]
      _ = 0 := by rw [zero_mul]

Subsingleton Property of Semirings with Characteristic 1

Informal description

If a semiring $R$ has characteristic 1, then $R$ is a subsingleton (i.e., all elements of $R$ are equal).

CharP.false_of_nontrivial_of_char_one theorem

[Nontrivial R] [CharP R 1] : False

Full source

lemma false_of_nontrivial_of_char_one [Nontrivial R] [CharP R 1] : False := by
  have : Subsingleton R := CharOne.subsingleton
  exact false_of_nontrivial_of_subsingleton R

Contradiction in Nontrivial Semirings with Characteristic 1

Informal description

If a semiring $R$ is nontrivial (contains at least two distinct elements) and has characteristic 1, then this leads to a contradiction.

CharP.ringChar_ne_one theorem

[Nontrivial R] : ringChar R ≠ 1

Full source

lemma ringChar_ne_one [Nontrivial R] : ringCharringChar R ≠ 1 := by
  intro h
  apply zero_ne_one' R
  symm
  rw [← Nat.cast_one, ringChar.spec, h]

Non-trivial semirings have characteristic different from one

Informal description

For any nontrivial semiring $R$, the characteristic of $R$ is not equal to $1$.

CharP.nontrivial_of_char_ne_one theorem

{v : ℕ} (hv : v ≠ 1) [hr : CharP R v] : Nontrivial R

Full source

lemma nontrivial_of_char_ne_one {v : ℕ} (hv : v ≠ 1) [hr : CharP R v] : Nontrivial R :=
  ⟨⟨(1 : ℕ), 0, fun h =>
      hv <| by rwa [CharP.cast_eq_zero_iff _ v, Nat.dvd_one] at h⟩⟩

Nontriviality of Semirings with Characteristic Different from One

Informal description

For any semiring $R$ with characteristic $v \neq 1$, the semiring $R$ is nontrivial (i.e., contains at least two distinct elements).

NeZero.of_not_dvd theorem

[CharP R p] (h : ¬p ∣ n) : NeZero (n : R)

Full source

lemma of_not_dvd [CharP R p] (h : ¬p ∣ n) : NeZero (n : R) :=
  ⟨(CharP.cast_eq_zero_iff R p n).not.mpr h⟩

Nonzero Image of Non-Divisible Natural Number in Characteristic $p$ Semiring

Informal description

Let $R$ be a semiring with characteristic $p$. If a natural number $n$ is not divisible by $p$, then the canonical image of $n$ in $R$ is nonzero, i.e., $n \neq 0$ in $R$.

NeZero.not_char_dvd theorem

(p : ℕ) [CharP R p] (k : ℕ) [h : NeZero (k : R)] : ¬p ∣ k

Full source

lemma not_char_dvd (p : ℕ) [CharP R p] (k : ℕ) [h : NeZero (k : R)] : ¬p ∣ k := by
  rwa [← CharP.cast_eq_zero_iff R p k, ← Ne, ← neZero_iff]

Non-divisibility of Nonzero Elements by Characteristic

Informal description

Let $R$ be a semiring with characteristic $p$, and let $k$ be a natural number such that the image of $k$ in $R$ is nonzero. Then $p$ does not divide $k$.

ExpChar classInductive

: ℕ → Prop

Full source

/-- The definition of the exponential characteristic of a semiring. -/
class inductive ExpChar : ℕ → Prop
  | zero [CharZero R] : ExpChar 1
  | prime {q : ℕ} (hprime : q.Prime) [hchar : CharP R q] : ExpChar q

Exponential characteristic of a semiring

Informal description

The exponential characteristic of a semiring $ R $ is defined to be 1 if $ R $ has characteristic 0, and equal to the ordinary characteristic $ p $ if $ R $ has prime characteristic $ p $. This concept is useful for simplifying theorem statements in contexts where the characteristic may be zero or prime.

expChar_prime instance

(p) [CharP R p] [Fact p.Prime] : ExpChar R p

Full source

instance expChar_prime (p) [CharP R p] [Fact p.Prime] : ExpChar R p := ExpChar.prime Fact.out

Exponential Characteristic for Prime Characteristic Semirings

Informal description

For any semiring $R$ with characteristic $p$ where $p$ is a prime number, the exponential characteristic of $R$ is $p$.

expChar_one instance

[CharZero R] : ExpChar R 1

Full source

instance expChar_one [CharZero R] : ExpChar R 1 := ExpChar.zero

Exponential Characteristic of Characteristic Zero Rings is One

Informal description

For any additive monoid with one $R$ of characteristic zero, the exponential characteristic of $R$ is 1.

expChar_ne_zero theorem

(p : ℕ) [hR : ExpChar R p] : p ≠ 0

Full source

lemma expChar_ne_zero (p : ℕ) [hR : ExpChar R p] : p ≠ 0 := by
  cases hR
  · exact one_ne_zero
  · exact ‹p.Prime›.ne_zero

Nonzero Exponential Characteristic

Informal description

For any semiring $R$ with exponential characteristic $p$, we have $p \neq 0$.

ExpChar.eq theorem

{p q : ℕ} (hp : ExpChar R p) (hq : ExpChar R q) : p = q

Full source

/-- The exponential characteristic is unique. -/
lemma ExpChar.eq {p q : ℕ} (hp : ExpChar R p) (hq : ExpChar R q) : p = q := by
  rcases hp with ⟨hp⟩ | ⟨hp'⟩
  · rcases hq with hq | hq'
    exacts [rfl, False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hq'))]
  · rcases hq with hq | hq'
    exacts [False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hp')),
      CharP.eq R ‹_› ‹_›]

Uniqueness of Exponential Characteristic

Informal description

For any semiring $R$ and natural numbers $p$ and $q$, if $R$ has exponential characteristic $p$ and exponential characteristic $q$, then $p = q$.

ExpChar.congr theorem

{p : ℕ} (q : ℕ) [hq : ExpChar R q] (h : q = p) : ExpChar R p

Full source

lemma ExpChar.congr {p : ℕ} (q : ℕ) [hq : ExpChar R q] (h : q = p) : ExpChar R p := h ▸ hq

Exponential Characteristic Congruence: $q = p$ implies $\text{ExpChar}(R, p)$

Informal description

Given a semiring $R$ with exponential characteristic $q$ and a natural number $p$ such that $q = p$, then $R$ has exponential characteristic $p$.

expChar_one_of_char_zero theorem

(q : ℕ) [hp : CharP R 0] [hq : ExpChar R q] : q = 1

Full source

/-- The exponential characteristic is one if the characteristic is zero. -/
lemma expChar_one_of_char_zero (q : ℕ) [hp : CharP R 0] [hq : ExpChar R q] : q = 1 := by
  rcases hq with q | hq_prime
  · rfl
  · exact False.elim <| hq_prime.ne_zero <| ‹CharP R q›.eq R hp

Exponential Characteristic is One for Characteristic Zero Semirings

Informal description

For any semiring $R$ with characteristic $0$ and exponential characteristic $q$, it holds that $q = 1$.

char_eq_expChar_iff theorem

(p q : ℕ) [hp : CharP R p] [hq : ExpChar R q] : p = q ↔ p.Prime

Full source

/-- The characteristic equals the exponential characteristic iff the former is prime. -/
lemma char_eq_expChar_iff (p q : ℕ) [hp : CharP R p] [hq : ExpChar R q] : p = q ↔ p.Prime := by
  rcases hq with q | hq_prime
  · rw [(CharP.eq R hp inferInstance : p = 0)]
    decide
  · exact ⟨fun hpq => hpq.symm ▸ hq_prime, fun _ => CharP.eq R hp ‹CharP R q›⟩

Characteristic Equals Exponential Characteristic iff Prime

Informal description

For a semiring $R$ with characteristic $p$ and exponential characteristic $q$, the equality $p = q$ holds if and only if $p$ is a prime number.

expChar_is_prime_or_one theorem

(q : ℕ) [hq : ExpChar R q] : Nat.Prime q ∨ q = 1

Full source

/-- The exponential characteristic is a prime number or one.
See also `CharP.char_is_prime_or_zero`. -/
lemma expChar_is_prime_or_one (q : ℕ) [hq : ExpChar R q] : Nat.PrimeNat.Prime q ∨ q = 1 := by
  cases hq with
  | zero => exact .inr rfl
  | prime hp => exact .inl hp

Exponential Characteristic is Prime or One

Informal description

For any semiring $R$ with exponential characteristic $q$, the value $q$ is either a prime number or equal to $1$.

expChar_pos theorem

(q : ℕ) [ExpChar R q] : 0 < q

Full source

/-- The exponential characteristic is positive. -/
lemma expChar_pos (q : ℕ) [ExpChar R q] : 0 < q := by
  rcases expChar_is_prime_or_one R q with h | rfl
  exacts [Nat.Prime.pos h, Nat.one_pos]

Positivity of Exponential Characteristic

Informal description

For any semiring $R$ with exponential characteristic $q$, the value $q$ is positive, i.e., $0 < q$.

expChar_pow_pos theorem

(q : ℕ) [ExpChar R q] (n : ℕ) : 0 < q ^ n

Full source

/-- Any power of the exponential characteristic is positive. -/
lemma expChar_pow_pos (q : ℕ) [ExpChar R q] (n : ℕ) : 0 < q ^ n :=
  Nat.pow_pos (expChar_pos R q)

Positivity of Powers of Exponential Characteristic

Informal description

For any semiring $R$ with exponential characteristic $q$ and any natural number $n$, the power $q^n$ is positive, i.e., $0 < q^n$.

ringExpChar definition

: ℕ

Full source

/-- Noncomputable function that outputs the unique exponential characteristic of a semiring. -/
noncomputable def ringExpChar : ℕ := max (ringChar R) 1

Exponential characteristic of a semiring

Informal description

The exponential characteristic of a semiring $R$ is defined as the maximum between the characteristic of $R$ and 1. This means it equals 1 when the characteristic is 0, and equals the characteristic otherwise (when the characteristic is prime).

ringExpChar.eq theorem

(q : ℕ) [h : ExpChar R q] : ringExpChar R = q

Full source

lemma ringExpChar.eq (q : ℕ) [h : ExpChar R q] : ringExpChar R = q := by
  rcases h with _ | h
  · haveI := CharP.ofCharZero R
    rw [ringExpChar, ringChar.eq R 0]; rfl
  rw [ringExpChar, ringChar.eq R q]
  exact Nat.max_eq_left h.one_lt.le

Equality of Ring Exponential Characteristic: $\text{ringExpChar}\, R = q$

Informal description

For any semiring $R$ with exponential characteristic $q$, the ring exponential characteristic of $R$ equals $q$, i.e., $\text{ringExpChar}\, R = q$.

char_zero_of_expChar_one theorem

(p : ℕ) [hp : CharP R p] [hq : ExpChar R 1] : p = 0

Full source

/-- The exponential characteristic is one if the characteristic is zero. -/
lemma char_zero_of_expChar_one (p : ℕ) [hp : CharP R p] [hq : ExpChar R 1] : p = 0 := by
  cases hq
  · exact CharP.eq R hp inferInstance
  · exact False.elim (CharP.char_ne_one R 1 rfl)

Characteristic Zero from Exponential Characteristic One

Informal description

For any semiring $R$ with characteristic $p$ and exponential characteristic $1$, the characteristic $p$ must be $0$.

charZero_of_expChar_one' theorem

[hq : ExpChar R 1] : CharZero R

Full source

/-- The characteristic is zero if the exponential characteristic is one. -/
lemma charZero_of_expChar_one' [hq : ExpChar R 1] : CharZero R := by
  cases hq
  · assumption
  · exact False.elim (CharP.char_ne_one R 1 rfl)

Characteristic Zero from Exponential Characteristic One

Informal description

If a semiring $R$ has exponential characteristic $1$, then $R$ has characteristic zero, meaning the canonical homomorphism $\mathbb{N} \to R$ is injective.

expChar_one_iff_char_zero theorem

(p q : ℕ) [CharP R p] [ExpChar R q] : q = 1 ↔ p = 0

Full source

/-- The exponential characteristic is one iff the characteristic is zero. -/
lemma expChar_one_iff_char_zero (p q : ℕ) [CharP R p] [ExpChar R q] : q = 1 ↔ p = 0 := by
  constructor
  · rintro rfl
    exact char_zero_of_expChar_one R p
  · rintro rfl
    exact expChar_one_of_char_zero R q

Exponential Characteristic One iff Characteristic Zero

Informal description

For a semiring $R$ with characteristic $p$ and exponential characteristic $q$, the exponential characteristic $q$ equals $1$ if and only if the characteristic $p$ equals $0$.

ExpChar.exists theorem

[Ring R] [IsDomain R] : ∃ q, ExpChar R q

Full source

lemma ExpChar.exists [Ring R] [IsDomain R] : ∃ q, ExpChar R q := by
  obtain _ | ⟨p, ⟨hp⟩, _⟩ := CharP.exists' R
  exacts [⟨1, .zero⟩, ⟨p, .prime hp⟩]

Existence of Exponential Characteristic for Domains

Informal description

For any domain $R$ (a nontrivial ring without zero divisors), there exists a natural number $q$ such that $R$ has exponential characteristic $q$. Here, the exponential characteristic is defined as: - $q = 1$ if $R$ has characteristic $0$, or - $q = p$ if $R$ has prime characteristic $p$.

ExpChar.exists_unique theorem

[Ring R] [IsDomain R] : ∃! q, ExpChar R q

Full source

lemma ExpChar.exists_unique [Ring R] [IsDomain R] : ∃! q, ExpChar R q :=
  let ⟨q, H⟩ := ExpChar.exists R
  ⟨q, H, fun _ H2 ↦ ExpChar.eq H2 H⟩

Uniqueness of Exponential Characteristic for Domains

Informal description

For any domain $R$ (a nontrivial ring without zero divisors), there exists a unique natural number $q$ such that $R$ has exponential characteristic $q$, where: - $q = 1$ if $R$ has characteristic $0$, or - $q = p$ if $R$ has prime characteristic $p$.

ringExpChar.expChar instance

[Ring R] [IsDomain R] : ExpChar R (ringExpChar R)

Full source

instance ringExpChar.expChar [Ring R] [IsDomain R] : ExpChar R (ringExpChar R) := by
  obtain ⟨q, _⟩ := ExpChar.exists R
  rwa [ringExpChar.eq R q]

Exponential Characteristic of a Domain Equals Its Ring Exponential Characteristic

Informal description

For any domain $R$, the exponential characteristic of $R$ is equal to its ring exponential characteristic. That is, if $R$ has characteristic 0, then its exponential characteristic is 1; otherwise, if $R$ has prime characteristic $p$, then its exponential characteristic is $p$.

ringExpChar.of_eq theorem

[Ring R] [IsDomain R] {q : ℕ} (h : ringExpChar R = q) : ExpChar R q

Full source

lemma ringExpChar.of_eq [Ring R] [IsDomain R] {q : ℕ} (h : ringExpChar R = q) : ExpChar R q :=
  h ▸ ringExpChar.expChar R

Exponential Characteristic of a Domain Determined by Ring Exponential Characteristic

Informal description

Let $R$ be a domain (a nontrivial ring without zero divisors) and let $q$ be a natural number. If the ring exponential characteristic of $R$ equals $q$, then $R$ has exponential characteristic $q$. That is: - If $R$ has characteristic $0$, then $q = 1$ and $\text{ExpChar}(R, 1)$ holds. - If $R$ has prime characteristic $p$, then $q = p$ and $\text{ExpChar}(R, p)$ holds.

Main definitions