Characteristic of semirings

theorem Commute.add_pow_prime_pow_eq {R : Type u_1} [Semiring R] {p : ℕ} {x : R} {y : R} (hp : Nat.Prime p) (h : Commute x y) (n : ℕ) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * Finset.sum (Finset.Ioo 0 (p ^ n)) fun k => x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)

theorem Commute.add_pow_prime_eq {R : Type u_1} [Semiring R] {p : ℕ} {x : R} {y : R} (hp : Nat.Prime p) (h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p + ↑p * Finset.sum (Finset.Ioo 0 p) fun k => x ^ k * y ^ (p - k) * ↑(Nat.choose p k / p)

theorem Commute.exists_add_pow_prime_pow_eq {R : Type u_1} [Semiring R] {p : ℕ} {x : R} {y : R} (hp : Nat.Prime p) (h : Commute x y) (n : ℕ) : ∃ r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r

theorem Commute.exists_add_pow_prime_eq {R : Type u_1} [Semiring R] {p : ℕ} {x : R} {y : R} (hp : Nat.Prime p) (h : Commute x y) : ∃ r, (x + y) ^ p = x ^ p + y ^ p + ↑p * r

theorem add_pow_prime_pow_eq {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : Nat.Prime p) (x : R) (y : R) (n : ℕ) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * Finset.sum (Finset.Ioo 0 (p ^ n)) fun k => x ^ k * y ^ (p ^ n - k) * ↑(Nat.choose (p ^ n) k / p)

theorem add_pow_prime_eq {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : Nat.Prime p) (x : R) (y : R) : (x + y) ^ p = x ^ p + y ^ p + ↑p * Finset.sum (Finset.Ioo 0 p) fun k => x ^ k * y ^ (p - k) * ↑(Nat.choose p k / p)

theorem exists_add_pow_prime_pow_eq {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : Nat.Prime p) (x : R) (y : R) (n : ℕ) : ∃ r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r

theorem exists_add_pow_prime_eq {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : Nat.Prime p) (x : R) (y : R) : ∃ r, (x + y) ^ p = x ^ p + y ^ p + ↑p * r

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

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

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.

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

@[simp]

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

@[simp]

theorem CharP.cast_card_eq_zero (R : Type u_1) [AddGroupWithOne R] [Fintype R] : ↑(Fintype.card R) = 0

theorem CharP.addOrderOf_one (R : Type u_2) [Semiring R] : CharP R (addOrderOf 1)

theorem CharP.int_cast_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.natCast_eq_natCast (R : Type u_1) [AddGroupWithOne R] (p : ℕ) [CharP R p] {a : ℕ} {b : ℕ} : ↑a = ↑b ↔ a ≡ b [MOD p]

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

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

Equations

• CharP.ofCharZero = CharP.ofCharZero.proof_1

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

theorem CharP.congr {R : Type u} [AddMonoidWithOne R] {p : ℕ} (q : ℕ) [hq : CharP R q] (h : q = 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 (_ : ∃! p, CharP R p)

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

• ringChar.charP = ringChar.charP.proof_1

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 add_pow_char_of_commute (R : Type u_1) [Semiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (x : R) (y : R) (h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p

theorem add_pow_char_pow_of_commute (R : Type u_1) [Semiring R] {p : ℕ} {n : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] (x : R) (y : R) (h : Commute x y) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

theorem sub_pow_char_of_commute (R : Type u_1) [Ring R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] (x : R) (y : R) (h : Commute x y) : (x - y) ^ p = x ^ p - y ^ p

theorem sub_pow_char_pow_of_commute (R : Type u_1) [Ring R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {n : ℕ} (x : R) (y : R) (h : Commute x y) : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

theorem add_pow_char (R : Type u_1) [CommSemiring R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] (x : R) (y : R) : (x + y) ^ p = x ^ p + y ^ p

theorem add_pow_char_pow (R : Type u_1) [CommSemiring R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {n : ℕ} (x : R) (y : R) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

theorem sub_pow_char (R : Type u_1) [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] (x : R) (y : R) : (x - y) ^ p = x ^ p - y ^ p

theorem sub_pow_char_pow (R : Type u_1) [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] {n : ℕ} (x : R) (y : R) : (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

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

theorem CharP.neg_one_pow_char (R : Type u_1) [CommRing R] (p : ℕ) [CharP R p] [Fact (Nat.Prime p)] : (-1) ^ p = -1

theorem CharP.neg_one_pow_char_pow (R : Type u_1) [CommRing R] (p : ℕ) (n : ℕ) [CharP R p] [Fact (Nat.Prime p)] : (-1) ^ p ^ n = -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

def frobenius (R : Type u_1) [CommSemiring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] : R →+* R

The frobenius map that sends x to x^p

Equations

• One or more equations did not get rendered due to their size.

theorem frobenius_def {R : Type u_1} [CommSemiring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (x : R) : ↑(frobenius R p) x = x ^ p

theorem iterate_frobenius {R : Type u_1} [CommSemiring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (x : R) (n : ℕ) : (↑(frobenius R p))^[n] x = x ^ p ^ n

theorem frobenius_mul {R : Type u_1} [CommSemiring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (x : R) (y : R) : ↑(frobenius R p) (x * y) = ↑(frobenius R p) x * ↑(frobenius R p) y

theorem frobenius_one {R : Type u_1} [CommSemiring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] : ↑(frobenius R p) 1 = 1

theorem MonoidHom.map_frobenius {R : Type u_1} [CommSemiring R] {S : Type v} [CommSemiring S] (f : R →* S) (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] [CharP S p] (x : R) : ↑f (↑(frobenius R p) x) = ↑(frobenius S p) (↑f x)

theorem RingHom.map_frobenius {R : Type u_1} [CommSemiring R] {S : Type v} [CommSemiring S] (g : R →+* S) (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] [CharP S p] (x : R) : ↑g (↑(frobenius R p) x) = ↑(frobenius S p) (↑g x)

theorem MonoidHom.map_iterate_frobenius {R : Type u_1} [CommSemiring R] {S : Type v} [CommSemiring S] (f : R →* S) (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] [CharP S p] (x : R) (n : ℕ) : ↑f ((↑(frobenius R p))^[n] x) = (↑(frobenius S p))^[n] (↑f x)

theorem RingHom.map_iterate_frobenius {R : Type u_1} [CommSemiring R] {S : Type v} [CommSemiring S] (g : R →+* S) (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] [CharP S p] (x : R) (n : ℕ) : ↑g ((↑(frobenius R p))^[n] x) = (↑(frobenius S p))^[n] (↑g x)

theorem MonoidHom.iterate_map_frobenius {R : Type u_1} [CommSemiring R] (x : R) (f : R →* R) (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (n : ℕ) : (↑f)^[n] (↑(frobenius R p) x) = ↑(frobenius R p) ((↑f)^[n] x)

theorem RingHom.iterate_map_frobenius {R : Type u_1} [CommSemiring R] (x : R) (f : R →+* R) (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (n : ℕ) : (↑f)^[n] (↑(frobenius R p) x) = ↑(frobenius R p) ((↑f)^[n] x)

theorem frobenius_zero (R : Type u_1) [CommSemiring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] : ↑(frobenius R p) 0 = 0

theorem frobenius_add (R : Type u_1) [CommSemiring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (x : R) (y : R) : ↑(frobenius R p) (x + y) = ↑(frobenius R p) x + ↑(frobenius R p) y

theorem frobenius_nat_cast (R : Type u_1) [CommSemiring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (n : ℕ) : ↑(frobenius R p) ↑n = ↑n

theorem list_sum_pow_char {R : Type u_1} [CommSemiring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (l : List R) : List.sum l ^ p = List.sum (List.map (fun x => x ^ p) l)

theorem multiset_sum_pow_char {R : Type u_1} [CommSemiring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (s : Multiset R) : Multiset.sum s ^ p = Multiset.sum (Multiset.map (fun x => x ^ p) s)

theorem sum_pow_char {R : Type u_1} [CommSemiring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] {ι : Type u_2} (s : Finset ι) (f : ι → R) : (Finset.sum s fun i => f i) ^ p = Finset.sum s fun i => f i ^ p

theorem frobenius_neg (R : Type u_1) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (x : R) : ↑(frobenius R p) (-x) = -↑(frobenius R p) x

theorem frobenius_sub (R : Type u_1) [CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (x : R) (y : R) : ↑(frobenius R p) (x - y) = ↑(frobenius R p) x - ↑(frobenius R p) y

theorem frobenius_inj (R : Type u_1) [CommRing R] [IsReduced R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] : Function.Injective ↑(frobenius R p)

theorem isSquare_of_charTwo' {R : Type u_2} [Finite R] [CommRing R] [IsReduced R] [CharP R 2] (a : R) : IsSquare a

If ringChar R = 2, where R is a finite reduced commutative ring, then every a : R is a square.

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

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

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

theorem CharP.char_ne_zero_of_finite (R : Type u_1) [NonAssocRing R] (p : ℕ) [CharP R p] [Finite R] : p ≠ 0

The characteristic of a finite ring cannot be zero.

theorem CharP.ringChar_ne_zero_of_finite (R : Type u_1) [NonAssocRing R] [Finite R] : ringChar R ≠ 0

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

@[simp]

theorem CharP.pow_prime_pow_mul_eq_one_iff {R : Type u_1} [CommRing R] [IsReduced R] (p : ℕ) (k : ℕ) (m : ℕ) [Fact (Nat.Prime p)] [CharP R p] (x : R) : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1

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 : ℕ) [hc : 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_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.char_is_prime (R : Type u_1) [Ring R] [NoZeroDivisors R] [Nontrivial R] [Finite R] (p : ℕ) [CharP R p] : Nat.Prime p

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

Equations

• @CharP.CharOne.subsingleton = @CharP.CharOne.subsingleton.proof_1

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

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.

theorem charP_of_ne_zero (R : Type u_1) [NonAssocRing R] [Fintype R] (n : ℕ) (hn : Fintype.card R = n) (hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0) : CharP R n

theorem charP_of_prime_pow_injective (R : Type u_2) [Ring R] [Fintype R] (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (hn : Fintype.card R = p ^ n) (hR : ∀ (i : ℕ), i ≤ n → ↑p ^ i = 0 → i = n) : CharP R (p ^ n)

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

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

Equations

• Nat.lcm.charP = Nat.lcm.charP.proof_1

instance Prod.charP (R : Type u_1) (S : Type v) [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

• Prod.charP = Prod.charP.proof_1

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

Equations

• ULift.charP = ULift.charP.proof_1

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

Equations

• MulOpposite.charP = MulOpposite.charP.proof_1

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