Mathlib.Algebra.CharP.Basic

CharP.natCast_eq_natCast' theorem

(h : a ≡ b [MOD p]) : (a : R) = b

Full source

lemma natCast_eq_natCast' (h : a ≡ b [MOD p]) : (a : R) = b := by
  wlog hle : a ≤ b
  · exact (this R p h.symm (le_of_not_le hle)).symm
  rw [Nat.modEq_iff_dvd' hle] at h
  rw [← Nat.sub_add_cancel hle, Nat.cast_add, (cast_eq_zero_iff R p _).mpr h, zero_add]

Characteristic $p$ Semiring Homomorphism Preserves Congruence Modulo $p$

Informal description

Let $R$ be a semiring with characteristic $p$. For any natural numbers $a$ and $b$ such that $a \equiv b \pmod{p}$, the canonical homomorphism satisfies $(a : R) = (b : R)$.

CharP.natCast_eq_natCast_mod theorem

(a : ℕ) : (a : R) = a % p

Full source

lemma natCast_eq_natCast_mod (a : ℕ) : (a : R) = a % p :=
  natCast_eq_natCast' R p (Nat.mod_modEq a p).symm

Canonical Homomorphism Equals Remainder Modulo Characteristic

Informal description

Let $R$ be a semiring with characteristic $p$. For any natural number $a$, the canonical homomorphism from $\mathbb{N}$ to $R$ satisfies $(a : R) = (a \% p)$, where $a \% p$ denotes the remainder of $a$ divided by $p$.

CharP.natCast_eq_natCast theorem

: (a : R) = b ↔ a ≡ b [MOD p]

Full source

lemma natCast_eq_natCast : (a : R) = b ↔ a ≡ b [MOD p] := by
  wlog hle : a ≤ b
  · rw [eq_comm, this R p (le_of_not_le hle), Nat.ModEq.comm]
  rw [Nat.modEq_iff_dvd' hle, ← cast_eq_zero_iff R p (b - a),
    ← add_right_cancel_iff (G := R) (a := a) (b := b - a), zero_add, ← Nat.cast_add,
    Nat.sub_add_cancel hle, eq_comm]

Characteristic Condition for Natural Number Casts: $(a : R) = (b : R) \leftrightarrow a \equiv b \pmod{p}$

Informal description

For any natural numbers $a$ and $b$ in an additive monoid with one $R$ of characteristic $p$, the canonical homomorphism satisfies $(a : R) = (b : R)$ if and only if $a \equiv b \pmod{p}$.

CharP.natCast_injOn_Iio theorem

: (Set.Iio p).InjOn ((↑) : ℕ → R)

Full source

lemma natCast_injOn_Iio : (Set.Iio p).InjOn ((↑) : ℕ → R) :=
  fun _a ha _b hb hab ↦ ((natCast_eq_natCast _ _).1 hab).eq_of_lt_of_lt ha hb

Injectivity of Natural Number Cast on $[0, p)$ in Semirings of Characteristic $p$

Informal description

For a semiring $R$ of characteristic $p$, the canonical map from natural numbers to $R$ is injective on the interval $[0, p)$, i.e., for any $a, b \in \mathbb{N}$ with $a, b < p$, if $(a : R) = (b : R)$ then $a = b$.

CharP.intCast_eq_intCast theorem

: (a : R) = b ↔ a ≡ b [ZMOD p]

Full source

lemma intCast_eq_intCast : (a : R) = b ↔ a ≡ b [ZMOD p] := by
  rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.intCast_eq_zero_iff R p, Int.modEq_iff_dvd]

Characteristic Condition for Integer Casts: $(a : R) = (b : R) \leftrightarrow a \equiv b \pmod{p}$

Informal description

For any integers $a$ and $b$ in an additive group with one $R$ of characteristic $p$, the canonical homomorphism satisfies $(a : R) = (b : R)$ if and only if $a \equiv b \pmod{p}$.

CharP.intCast_eq_intCast_mod theorem

: (a : R) = a % (p : ℤ)

Full source

lemma intCast_eq_intCast_mod : (a : R) = a % (p : ℤ) :=
  (CharP.intCast_eq_intCast R p).mpr (Int.mod_modEq a p).symm

Integer Cast Equals Remainder Modulo Characteristic

Informal description

For any integer $a$ in an additive group with one $R$ of characteristic $p$, the canonical homomorphism satisfies $(a : R) = (a \% p)$, where $a \% p$ denotes the remainder of $a$ divided by $p$.

CharP.intCast_injOn_Ico theorem

[IsRightCancelAdd R] : InjOn (Int.cast : ℤ → R) (Ico 0 p)

Full source

lemma intCast_injOn_Ico [IsRightCancelAdd R] : InjOn (Int.cast : ℤ → R) (Ico 0 p) := by
  rintro a ⟨ha₀, ha⟩ b ⟨hb₀, hb⟩ hab
  lift a to ℕ using ha₀
  lift b to ℕ using hb₀
  norm_cast at *
  exact natCast_injOn_Iio _ _ ha hb hab

Injectivity of Integer Cast on $[0, p)$ in Semirings with Right-Cancellative Addition

Informal description

Let $R$ be a semiring with right-cancellative addition. The canonical homomorphism from the integers to $R$ is injective on the interval $[0, p) \subseteq \mathbb{Z}$.

CharP.cast_ne_zero_of_ne_of_prime theorem

[Nontrivial R] {p q : ℕ} [CharP R p] (hq : q.Prime) (hneq : p ≠ q) : (q : R) ≠ 0

Full source

/-- If a ring `R` is of characteristic `p`, then for any prime number `q` different from `p`,
it is not zero in `R`. -/
lemma cast_ne_zero_of_ne_of_prime [Nontrivial R]
    {p q : ℕ} [CharP R p] (hq : q.Prime) (hneq : p ≠ q) : (q : R) ≠ 0 := fun h ↦ by
  rw [cast_eq_zero_iff R p q] at h
  rcases hq.eq_one_or_self_of_dvd _ h with h | h
  · subst h
    exact false_of_nontrivial_of_char_one (R := R)
  · exact hneq h

Nonzero image of distinct prime in characteristic $p$ semiring

Informal description

Let $R$ be a nontrivial semiring of characteristic $p$, and let $q$ be a prime number different from $p$. Then the canonical image of $q$ in $R$ is nonzero, i.e., $q \neq 0$ in $R$.

CharP.ringChar_of_prime_eq_zero theorem

[Nontrivial R] {p : ℕ} (hprime : Nat.Prime p) (hp0 : (p : R) = 0) : ringChar R = p

Full source

lemma ringChar_of_prime_eq_zero [Nontrivial R] {p : ℕ} (hprime : Nat.Prime p)
    (hp0 : (p : R) = 0) : ringChar R = p :=
  Or.resolve_left ((Nat.dvd_prime hprime).1 (ringChar.dvd hp0)) ringChar_ne_one

Characteristic of a Semiring Determined by Prime Vanishing Condition

Informal description

Let $R$ be a nontrivial non-associative semiring. For any prime natural number $p$, if the canonical image of $p$ in $R$ equals zero (i.e., $p = 0$ in $R$), then the characteristic of $R$ is equal to $p$.

CharP.charP_iff_prime_eq_zero theorem

[Nontrivial R] {p : ℕ} (hp : p.Prime) : CharP R p ↔ (p : R) = 0

Full source

lemma charP_iff_prime_eq_zero [Nontrivial R] {p : ℕ} (hp : p.Prime) :
    CharPCharP R p ↔ (p : R) = 0 :=
  ⟨fun _ => cast_eq_zero R p,
   fun hp0 => (ringChar_of_prime_eq_zero hp hp0) ▸ inferInstance⟩

Characterization of Semiring Characteristic via Prime Vanishing Condition

Informal description

Let $R$ be a nontrivial non-associative semiring and let $p$ be a prime natural number. Then $R$ has characteristic $p$ if and only if the canonical image of $p$ in $R$ equals zero, i.e., $p = 0$ in $R$.

Ring.two_ne_zero theorem

{R : Type*} [NonAssocSemiring R] [Nontrivial R] (hR : ringChar R ≠ 2) : (2 : R) ≠ 0

Full source

/-- We have `2 ≠ 0` in a nontrivial ring whose characteristic is not `2`. -/
protected lemma Ring.two_ne_zero {R : Type*} [NonAssocSemiring R] [Nontrivial R]
    (hR : ringCharringChar R ≠ 2) : (2 : R) ≠ 0 := by
  rw [Ne, (by norm_cast : (2 : R) = (2 : ℕ)), ringChar.spec, Nat.dvd_prime Nat.prime_two]
  exact mt (or_iff_left hR).mp CharP.ringChar_ne_one

Nonzero condition for 2 in semirings of characteristic not 2

Informal description

Let $R$ be a nontrivial non-associative semiring. If the characteristic of $R$ is not $2$, then $2 \neq 0$ in $R$.

Ring.neg_one_ne_one_of_char_ne_two theorem

{R : Type*} [NonAssocRing R] [Nontrivial R] (hR : ringChar R ≠ 2) : (-1 : R) ≠ 1

Full source

/-- Characteristic `≠ 2` and nontrivial implies that `-1 ≠ 1`. -/
lemma Ring.neg_one_ne_one_of_char_ne_two {R : Type*} [NonAssocRing R] [Nontrivial R]
    (hR : ringCharringChar R ≠ 2) : (-1 : R) ≠ 1 := fun h =>
  Ring.two_ne_zero hR (one_add_one_eq_two (R := R) ▸ neg_eq_iff_add_eq_zero.mp h)

Distinctness of $-1$ and $1$ in rings of characteristic $\neq 2$

Informal description

Let $R$ be a nontrivial non-associative ring. If the characteristic of $R$ is not $2$, then $-1 \neq 1$ in $R$.

Nat.lcm.charP instance

[CharP S q] : CharP (R × S) (Nat.lcm p q)

Full source

/-- The characteristic of the product of rings is the least common multiple of the
characteristics of the two rings. -/
instance Nat.lcm.charP [CharP S q] : CharP (R × S) (Nat.lcm p q) where
  cast_eq_zero_iff := by
    simp [Prod.ext_iff, CharP.cast_eq_zero_iff R p, CharP.cast_eq_zero_iff S q, Nat.lcm_dvd_iff]

Characteristic of Product Ring is LCM of Characteristics

Informal description

For any two rings $R$ and $S$ with characteristics $p$ and $q$ respectively, the characteristic of the product ring $R \times S$ is the least common multiple of $p$ and $q$.

Prod.charP instance

[CharP S p] : CharP (R × S) p

Full source

/-- The characteristic of the product of two rings of the same characteristic
  is the same as the characteristic of the rings -/
instance Prod.charP [CharP S p] : CharP (R × S) p := by
  convert Nat.lcm.charP R S p p; simp

Characteristic of Product Semiring with Same Characteristic

Informal description

For any two semirings $R$ and $S$ with the same characteristic $p$, the product semiring $R \times S$ also has characteristic $p$.

Prod.charZero_of_left instance

[CharZero R] : CharZero (R × S)

Full source

instance Prod.charZero_of_left [CharZero R] : CharZero (R × S) where
  cast_injective _ _ h := CharZero.cast_injective congr(Prod.fst $h)

Characteristic Zero Preserved in Left Product

Informal description

For any additive monoid with one $R$ and any type $S$, if $R$ has characteristic zero, then the product $R \times S$ also has characteristic zero.

Prod.charZero_of_right instance

[CharZero S] : CharZero (R × S)

Full source

instance Prod.charZero_of_right [CharZero S] : CharZero (R × S) where
  cast_injective _ _ h := CharZero.cast_injective congr(Prod.snd $h)

Characteristic Zero Preserved in Right Product

Informal description

For any additive monoid with one $R$ and any type $S$, if $S$ has characteristic zero, then the product $R \times S$ also has characteristic zero.

ULift.charP instance

[AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP (ULift R) p

Full source

instance ULift.charP [AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP (ULift R) p where
  cast_eq_zero_iff n := Iff.trans ULift.ext_iff <| CharP.cast_eq_zero_iff R p n

Characteristic Preservation in Lifted Types

Informal description

For any additive monoid with one $R$ and natural number $p$, if $R$ has characteristic $p$, then the lifted type $\mathrm{ULift}\, R$ also has characteristic $p$.

MulOpposite.charP instance

[AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP Rᵐᵒᵖ p

Full source

instance MulOpposite.charP [AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP Rᵐᵒᵖ p where
  cast_eq_zero_iff n := MulOpposite.unop_inj.symm.trans <| CharP.cast_eq_zero_iff R p n

Characteristic Preservation in Multiplicative Opposites

Informal description

For any additive monoid with one $R$ and natural number $p$, if $R$ has characteristic $p$, then the multiplicative opposite $R^\text{op}$ also has characteristic $p$.

Int.cast_injOn_of_ringChar_ne_two theorem

{R : Type*} [NonAssocRing R] [Nontrivial R] (hR : ringChar R ≠ 2) : ({0, 1, -1} : Set ℤ).InjOn ((↑) : ℤ → R)

Full source

/-- If two integers from `{0, 1, -1}` result in equal elements in a ring `R`
that is nontrivial and of characteristic not `2`, then they are equal. -/
lemma Int.cast_injOn_of_ringChar_ne_two {R : Type*} [NonAssocRing R] [Nontrivial R]
    (hR : ringCharringChar R ≠ 2) : ({0, 1, -1} : Set ℤ).InjOn ((↑) : ℤ → R) := by
  rintro _ (rfl | rfl | rfl) _ (rfl | rfl | rfl) h <;>
  simp only
    [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
  · exact ((Ring.neg_one_ne_one_of_char_ne_two hR).symm h).elim
  · exact ((Ring.neg_one_ne_one_of_char_ne_two hR) h).elim

Injectivity of Integer Cast on $\{0, 1, -1\}$ in Rings of Characteristic $\neq 2$

Informal description

Let $R$ be a nontrivial non-associative ring with characteristic not equal to $2$. Then the canonical homomorphism from the integers $\mathbb{Z}$ to $R$ is injective when restricted to the set $\{0, 1, -1\}$. In other words, for any $x, y \in \{0, 1, -1\}$, if $x$ and $y$ have the same image in $R$, then $x = y$.

CharZero.charZero_iff_forall_prime_ne_zero theorem

[NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] : CharZero R ↔ ∀ p : ℕ, p.Prime → (p : R) ≠ 0

Full source

lemma charZero_iff_forall_prime_ne_zero [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] :
    CharZeroCharZero R ↔ ∀ p : ℕ, p.Prime → (p : R) ≠ 0 := by
  refine ⟨fun h p hp => by simp [hp.ne_zero], fun h => ?_⟩
  let p := ringChar R
  cases CharP.char_is_prime_or_zero R p with
  | inl hp => simpa using h p hp
  | inr h => have : CharP R 0 := h ▸ inferInstance; exact CharP.charP_to_charZero R

Characterization of characteristic zero rings via primes: $R$ has char 0 iff all primes are nonzero in $R$

Informal description

Let $R$ be a nontrivial non-associative ring with no zero divisors. Then $R$ has characteristic zero if and only if for every prime natural number $p$, the canonical image of $p$ in $R$ is nonzero (i.e., $p \cdot 1_R \neq 0$).

Fin.charP instance

(n : ℕ) [NeZero n] : CharP (Fin n) n

Full source

/-- The characteristic of `F_p` is `p`. -/
@[stacks 09FS "First part. We don't require `p` to be a prime in mathlib."]
instance charP (n : ℕ) [NeZero n] : CharP (Fin n) n where cast_eq_zero_iff _ := natCast_eq_zero

Characteristic of Finite Types $\mathrm{Fin}(n)$ is $n$

Informal description

For any nonzero natural number $n$, the finite type $\mathrm{Fin}(n)$ has characteristic $n$. That is, the smallest positive integer $p$ such that $p \cdot 1 = 0$ in $\mathrm{Fin}(n)$ is $n$ itself.

instExpCharProd instance

(S : Type*) [Semiring S] (p) [ExpChar R p] [ExpChar S p] : ExpChar (R × S) p

Full source

instance (S : Type*) [Semiring S] (p) [ExpChar R p] [ExpChar S p] : ExpChar (R × S) p := by
  obtain hp | ⟨hp⟩ := ‹ExpChar R p›
  · have := Prod.charZero_of_left R S; exact .zero
  obtain _ | _ := ‹ExpChar S p›
  · exact (Nat.not_prime_one hp).elim
  · have := Prod.charP R S p; exact .prime hp

Exponential Characteristic of Product Semiring with Same Exponential Characteristic

Informal description

For any two semirings $R$ and $S$ with the same exponential characteristic $p$, the product semiring $R \times S$ also has exponential characteristic $p$.