Characteristic of semirings

theorem charP_iff (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) : CharP R p ↔ ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x

class CharP (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) : Prop

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.

• cast_eq_zero_iff' : ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x

theorem CharP.cast_eq_zero_iff' {R : Type u_1} : ∀ {inst : AddMonoidWithOne R} {p : ℕ} [self : CharP R p] (x : ℕ), ↑x = 0 ↔ p ∣ x

theorem CharP.cast_eq_zero_iff (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] (a : ℕ) : ↑a = 0 ↔ p ∣ a

theorem CharP.congr {R : Type u_1} [AddMonoidWithOne R] (p : ℕ) [CharP R p] {q : ℕ} (h : p = q) : CharP R q

theorem CharP.natCast_eq_natCast' (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] {a : ℕ} {b : ℕ} (h : a ≡ b [MOD p]) : ↑a = ↑b

@[simp]

theorem CharP.cast_eq_zero (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] : ↑p = 0

theorem CharP.ofNat_eq_zero (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] [p.AtLeastTwo] : OfNat.ofNat p = 0

theorem CharP.natCast_eq_natCast_mod (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] (a : ℕ) : ↑a = ↑(a % p)

theorem CharP.eq (R : Type u_1) [AddMonoidWithOne R] {p : ℕ} {q : ℕ} (_hp : CharP R p) (_hq : CharP R q) : p = q

instance CharP.ofCharZero (R : Type u_1) [AddMonoidWithOne R] [CharZero R] : CharP R 0

Equations

• ⋯ = ⋯

theorem CharP.natCast_eq_natCast (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] {a : ℕ} {b : ℕ} [IsRightCancelAdd R] : ↑a = ↑b ↔ a ≡ b [MOD p]

theorem CharP.natCast_injOn_Iio (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] [IsRightCancelAdd R] : Set.InjOn Nat.cast (Set.Iio p)

theorem CharP.intCast_injOn_Ico (R : Type u_1) [AddGroupWithOne R] (p : ℕ) [CharP R p] [IsRightCancelAdd R] : Set.InjOn Int.cast (Set.Ico 0 ↑p)

theorem CharP.intCast_eq_zero_iff (R : Type u_1) [AddGroupWithOne R] (p : ℕ) [CharP R p] (a : ℤ) : ↑a = 0 ↔ ↑p ∣ a

theorem CharP.intCast_eq_intCast (R : Type u_1) [AddGroupWithOne R] (p : ℕ) [CharP R p] {a : ℤ} {b : ℤ} : ↑a = ↑b ↔ a ≡ b [ZMOD ↑p]

theorem CharP.intCast_eq_intCast_mod (R : Type u_1) [AddGroupWithOne R] (p : ℕ) [CharP R p] {a : ℤ} : ↑a = ↑(a % ↑p)

theorem CharP.charP_to_charZero (R : Type u_1) [AddGroupWithOne R] [CharP R 0] : CharZero R

theorem CharP.charP_zero_iff_charZero (R : Type u_1) [AddGroupWithOne R] : CharP R 0 ↔ CharZero R

theorem CharP.exists (R : Type u_1) [NonAssocSemiring R] : ∃ (p : ℕ), CharP R p

theorem CharP.exists_unique (R : Type u_1) [NonAssocSemiring R] : ∃! p : ℕ, CharP R p

noncomputable def ringChar (R : Type u_1) [NonAssocSemiring R] : ℕ

Noncomputable function that outputs the unique characteristic of a semiring.

Equations

• ringChar R = Classical.choose ⋯

theorem ringChar.spec (R : Type u_1) [NonAssocSemiring R] (x : ℕ) : ↑x = 0 ↔ ringChar R ∣ x

theorem ringChar.eq (R : Type u_1) [NonAssocSemiring R] (p : ℕ) [C : CharP R p] : ringChar R = p

instance ringChar.charP (R : Type u_1) [NonAssocSemiring R] : CharP R (ringChar R)

Equations

• ⋯ = ⋯

theorem ringChar.of_eq {R : Type u_1} [NonAssocSemiring R] {p : ℕ} (h : ringChar R = p) : CharP R p

theorem ringChar.eq_iff {R : Type u_1} [NonAssocSemiring R] {p : ℕ} : ringChar R = p ↔ CharP R p

theorem ringChar.dvd {R : Type u_1} [NonAssocSemiring R] {x : ℕ} (hx : ↑x = 0) : ringChar R ∣ x

@[simp]

theorem ringChar.eq_zero {R : Type u_1} [NonAssocSemiring R] [CharZero R] : ringChar R = 0

theorem ringChar.Nat.cast_ringChar {R : Type u_1} [NonAssocSemiring R] : ↑(ringChar R) = 0

theorem CharP.neg_one_ne_one (R : Type u_1) [Ring R] (p : ℕ) [CharP R p] [Fact (2 < p)] : -1 ≠ 1

theorem RingHom.charP_iff_charP {K : Type u_2} {L : Type u_3} [DivisionRing K] [Semiring L] [Nontrivial L] (f : K →+* L) (p : ℕ) : CharP K p ↔ CharP L p

theorem CharP.cast_eq_mod (R : Type u_1) [NonAssocRing R] (p : ℕ) [CharP R p] (k : ℕ) : ↑k = ↑(k % p)

theorem CharP.ringChar_zero_iff_CharZero (R : Type u_1) [NonAssocRing R] : ringChar R = 0 ↔ CharZero R

theorem CharP.char_ne_one (R : Type u_1) [NonAssocSemiring R] [Nontrivial R] (p : ℕ) [hc : CharP R p] : p ≠ 1

theorem CharP.char_is_prime_of_two_le (R : Type u_1) [NonAssocSemiring R] [NoZeroDivisors R] (p : ℕ) [CharP R p] (hp : 2 ≤ p) : Nat.Prime p

theorem CharP.char_is_prime_or_zero (R : Type u_1) [NonAssocSemiring R] [NoZeroDivisors R] [Nontrivial R] (p : ℕ) [hc : CharP R p] : Nat.Prime p ∨ p = 0

theorem CharP.char_prime_of_ne_zero (R : Type u_1) [NonAssocSemiring R] [NoZeroDivisors R] [Nontrivial R] {p : ℕ} [CharP R p] (hp : p ≠ 0) : Nat.Prime p

The characteristic is prime if it is non-zero.

theorem CharP.exists' (R : Type u_2) [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] : CharZero R ∨ ∃ (p : ℕ), Fact (Nat.Prime p) ∧ CharP R p

theorem CharP.char_is_prime_of_pos (R : Type u_1) [NonAssocSemiring R] [NoZeroDivisors R] [Nontrivial R] (p : ℕ) [NeZero p] [CharP R p] : Fact (Nat.Prime p)

theorem CharP.CharOne.subsingleton {R : Type u_1} [NonAssocSemiring R] [CharP R 1] : Subsingleton R

theorem CharP.false_of_nontrivial_of_char_one {R : Type u_1} [NonAssocSemiring R] [Nontrivial R] [CharP R 1] : False

theorem CharP.cast_ne_zero_of_ne_of_prime (R : Type u_1) [NonAssocSemiring R] [Nontrivial R] {p : ℕ} {q : ℕ} [CharP R p] (hq : Nat.Prime q) (hneq : p ≠ q) : ↑q ≠ 0

If a ring R is of characteristic p, then for any prime number q different from p, it is not zero in R.

theorem CharP.ringChar_ne_one {R : Type u_1} [NonAssocSemiring R] [Nontrivial R] : ringChar R ≠ 1

theorem CharP.nontrivial_of_char_ne_one {R : Type u_1} [NonAssocSemiring R] {v : ℕ} (hv : v ≠ 1) [hr : CharP R v] : Nontrivial R

theorem CharP.ringChar_of_prime_eq_zero {R : Type u_1} [NonAssocSemiring R] [Nontrivial R] {p : ℕ} (hprime : Nat.Prime p) (hp0 : ↑p = 0) : ringChar R = p

theorem CharP.charP_iff_prime_eq_zero {R : Type u_1} [NonAssocSemiring R] [Nontrivial R] {p : ℕ} (hp : Nat.Prime p) : CharP R p ↔ ↑p = 0

theorem Ring.two_ne_zero {R : Type u_2} [NonAssocSemiring R] [Nontrivial R] (hR : ringChar R ≠ 2) : 2 ≠ 0

We have 2 ≠ 0 in a nontrivial ring whose characteristic is not 2.

theorem Ring.neg_one_ne_one_of_char_ne_two {R : Type u_2} [NonAssocRing R] [Nontrivial R] (hR : ringChar R ≠ 2) : -1 ≠ 1

Characteristic ≠ 2 and nontrivial implies that -1 ≠ 1.

theorem Ring.eq_self_iff_eq_zero_of_char_ne_two {R : Type u_2} [NonAssocRing R] [Nontrivial R] [NoZeroDivisors R] (hR : ringChar R ≠ 2) {a : R} : -a = a ↔ a = 0

Characteristic ≠ 2 in a domain implies that -a = a iff a = 0.

instance Nat.lcm.charP (R : Type u_1) (S : Type u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] (p : ℕ) (q : ℕ) [CharP R p] [CharP S q] : CharP (R × S) (p.lcm q)

The characteristic of the product of rings is the least common multiple of the characteristics of the two rings.

Equations

• ⋯ = ⋯

instance Prod.charP (R : Type u_1) (S : Type u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] (p : ℕ) [CharP R p] [CharP S p] : CharP (R × S) p

The characteristic of the product of two rings of the same characteristic is the same as the characteristic of the rings

Equations

• ⋯ = ⋯

instance Prod.charZero_of_left (R : Type u_1) (S : Type u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] [CharZero R] : CharZero (R × S)

Equations

• ⋯ = ⋯

instance Prod.charZero_of_right (R : Type u_1) (S : Type u_2) [AddMonoidWithOne R] [AddMonoidWithOne S] [CharZero S] : CharZero (R × S)

Equations

• ⋯ = ⋯

instance ULift.charP (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP (ULift.{u_2, u_1} R) p

Equations

• ⋯ = ⋯

instance MulOpposite.charP (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP Rᵐᵒᵖ p

Equations

• ⋯ = ⋯

theorem Int.cast_injOn_of_ringChar_ne_two {R : Type u_2} [NonAssocRing R] [Nontrivial R] (hR : ringChar R ≠ 2) : Set.InjOn Int.cast {0, 1, -1}

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.

theorem NeZero.of_not_dvd (R : Type u_1) [AddMonoidWithOne R] {n : ℕ} {p : ℕ} [CharP R p] (h : ¬p ∣ n) : NeZero ↑n

theorem NeZero.not_char_dvd (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] (k : ℕ) [h : NeZero ↑k] : ¬p ∣ k

theorem CharZero.charZero_iff_forall_prime_ne_zero (R : Type u_1) [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] : CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0

instance Fin.charP (n : ℕ) [NeZero n] : CharP (Fin n) n

Equations

• ⋯ = ⋯

Exponential characteristic

This section defines the exponential characteristic, which is defined to be 1 for a ring with characteristic 0 and the same as the ordinary characteristic, if the ordinary characteristic is prime. This concept is useful to simplify some theorem statements. This file establishes a few basic results relating it to the (ordinary characteristic). The definition is stated for a semiring, but the actual results are for nontrivial rings (as far as exponential characteristic one is concerned), respectively a ring without zero-divisors (for prime characteristic).

class inductive ExpChar (R : Type u_1) [AddMonoidWithOne R] : ℕ → Prop

The definition of the exponential characteristic of a semiring.

• zero: ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R], ExpChar R 1
• prime: ∀ {R : Type u_1} [inst : AddMonoidWithOne R] {q : ℕ}, Nat.Prime q → ∀ [hchar : CharP R q], ExpChar R q

instance expChar_prime (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] [Fact (Nat.Prime p)] : ExpChar R p

Equations

• ⋯ = ⋯

instance expChar_one (R : Type u_1) [AddMonoidWithOne R] [CharZero R] : ExpChar R 1

Equations

• ⋯ = ⋯

theorem expChar_ne_zero (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [hR : ExpChar R p] : p ≠ 0

instance instExpCharProd (R : Type u_1) [AddMonoidWithOne R] (S : Type u_2) [Semiring S] (p : ℕ) [ExpChar R p] [ExpChar S p] : ExpChar (R × S) p

Equations

• ⋯ = ⋯

theorem ExpChar.eq {R : Type u_1} [AddMonoidWithOne R] {p : ℕ} {q : ℕ} (hp : ExpChar R p) (hq : ExpChar R q) : p = q

The exponential characteristic is unique.

theorem ExpChar.congr (R : Type u_1) [AddMonoidWithOne R] {p : ℕ} (q : ℕ) [hq : ExpChar R q] (h : q = p) : ExpChar R p

theorem expChar_one_of_char_zero (R : Type u_1) [AddMonoidWithOne R] (q : ℕ) [hp : CharP R 0] [hq : ExpChar R q] : q = 1

The exponential characteristic is one if the characteristic is zero.

theorem char_eq_expChar_iff (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) (q : ℕ) [hp : CharP R p] [hq : ExpChar R q] : p = q ↔ Nat.Prime p

The characteristic equals the exponential characteristic iff the former is prime.

theorem expChar_is_prime_or_one (R : Type u_1) [AddMonoidWithOne R] (q : ℕ) [hq : ExpChar R q] : Nat.Prime q ∨ q = 1

The exponential characteristic is a prime number or one. See also CharP.char_is_prime_or_zero.

theorem expChar_pos (R : Type u_1) [AddMonoidWithOne R] (q : ℕ) [ExpChar R q] : 0 < q

The exponential characteristic is positive.

theorem expChar_pow_pos (R : Type u_1) [AddMonoidWithOne R] (q : ℕ) [ExpChar R q] (n : ℕ) : 0 < q ^ n

Any power of the exponential characteristic is positive.

noncomputable def ringExpChar (R : Type u_1) [NonAssocSemiring R] : ℕ

Noncomputable function that outputs the unique exponential characteristic of a semiring.

Equations

• ringExpChar R = max (ringChar R) 1

theorem ringExpChar.eq (R : Type u_1) [NonAssocSemiring R] (q : ℕ) [h : ExpChar R q] : ringExpChar R = q

@[simp]

theorem ringExpChar.eq_one (R : Type u_1) [NonAssocSemiring R] [CharZero R] : ringExpChar R = 1

theorem char_zero_of_expChar_one (R : Type u_1) [NonAssocSemiring R] [Nontrivial R] (p : ℕ) [hp : CharP R p] [hq : ExpChar R 1] : p = 0

The exponential characteristic is one if the characteristic is zero.

theorem charZero_of_expChar_one' (R : Type u_1) [NonAssocSemiring R] [Nontrivial R] [hq : ExpChar R 1] : CharZero R

The characteristic is zero if the exponential characteristic is one.

theorem expChar_one_iff_char_zero (R : Type u_1) [NonAssocSemiring R] [Nontrivial R] (p : ℕ) (q : ℕ) [CharP R p] [ExpChar R q] : q = 1 ↔ p = 0

The exponential characteristic is one iff the characteristic is zero.

theorem ExpChar.exists (R : Type u_1) [Ring R] [IsDomain R] : ∃ (q : ℕ), ExpChar R q

theorem ExpChar.exists_unique (R : Type u_1) [Ring R] [IsDomain R] : ∃! q : ℕ, ExpChar R q

instance ringExpChar.expChar (R : Type u_1) [Ring R] [IsDomain R] : ExpChar R (ringExpChar R)

Equations

• ⋯ = ⋯

theorem ringExpChar.of_eq {R : Type u_1} [Ring R] [IsDomain R] {q : ℕ} (h : ringExpChar R = q) : ExpChar R q

theorem ringExpChar.eq_iff {R : Type u_1} [Ring R] [IsDomain R] {q : ℕ} : ringExpChar R = q ↔ ExpChar R q