mathlib3 documentation

algebra.char_p.basic

Characteristic of semirings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected]
theorem commute.add_pow_prime_pow_eq {R : Type u_1} [semiring R] {p : } {x y : R} (hp : nat.prime p) (h : commute x y) (n : ) :
(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * (finset.Ioo 0 (p ^ n)).sum (λ (k : ), x ^ k * y ^ (p ^ n - k) * ((p ^ n).choose k / p))
@[protected]
theorem commute.add_pow_prime_eq {R : Type u_1} [semiring R] {p : } {x y : R} (hp : nat.prime p) (h : commute x y) :
(x + y) ^ p = x ^ p + y ^ p + p * (finset.Ioo 0 p).sum (λ (k : ), x ^ k * y ^ (p - k) * (p.choose k / p))
@[protected]
theorem commute.exists_add_pow_prime_pow_eq {R : Type u_1} [semiring R] {p : } {x y : R} (hp : nat.prime p) (h : commute x y) (n : ) :
(r : R), (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * r
@[protected]
theorem commute.exists_add_pow_prime_eq {R : Type u_1} [semiring R] {p : } {x y : R} (hp : nat.prime p) (h : commute x y) :
(r : R), (x + y) ^ p = x ^ p + y ^ p + p * r
theorem add_pow_prime_pow_eq {R : Type u_1} [comm_semiring R] {p : } (hp : nat.prime p) (x y : R) (n : ) :
(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * (finset.Ioo 0 (p ^ n)).sum (λ (k : ), x ^ k * y ^ (p ^ n - k) * ((p ^ n).choose k / p))
theorem add_pow_prime_eq {R : Type u_1} [comm_semiring R] {p : } (hp : nat.prime p) (x y : R) :
(x + y) ^ p = x ^ p + y ^ p + p * (finset.Ioo 0 p).sum (λ (k : ), x ^ k * y ^ (p - k) * (p.choose k / p))
theorem exists_add_pow_prime_pow_eq {R : Type u_1} [comm_semiring R] {p : } (hp : nat.prime p) (x y : R) (n : ) :
(r : R), (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * r
theorem exists_add_pow_prime_eq {R : Type u_1} [comm_semiring R] {p : } (hp : nat.prime p) (x y : R) :
(r : R), (x + y) ^ p = x ^ p + y ^ p + p * r
theorem char_p_iff (R : Type u_1) [add_monoid_with_one R] (p : ) :
char_p R p (x : ), x = 0 p x
@[class]
structure char_p (R : Type u_1) [add_monoid_with_one R] (p : ) :
Prop

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

Warning: for a semiring R, char_p R 0 and char_zero R need not coincide.

  • char_p R 0 asks that only 0 : ℕ maps to 0 : R under the map ℕ → R;
  • char_zero R requires an injection ℕ ↪ R.

For instance, endowing {0, 1} with addition given by max (i.e. 1 is absorbing), shows that char_zero {0, 1} does not hold and yet char_p {0, 1} 0 does. This example is formalized in counterexamples/char_p_zero_ne_char_zero.

Instances of this typeclass
@[simp]
theorem char_p.cast_eq_zero (R : Type u_1) [add_monoid_with_one R] (p : ) [char_p R p] :
p = 0
@[simp]
theorem char_p.int_cast_eq_zero_iff (R : Type u_1) [add_group_with_one R] (p : ) [char_p R p] (a : ) :
a = 0 p a
theorem char_p.int_cast_eq_int_cast (R : Type u_1) [add_group_with_one R] (p : ) [char_p R p] {a b : } :
theorem char_p.nat_cast_eq_nat_cast (R : Type u_1) [add_group_with_one R] (p : ) [char_p R p] {a b : } :
a = b a b [MOD p]
theorem char_p.eq (R : Type u_1) [add_monoid_with_one R] {p q : } (c1 : char_p R p) (c2 : char_p R q) :
p = q
@[protected, instance]
theorem char_p.exists (R : Type u_1) [non_assoc_semiring R] :
(p : ), char_p R p
theorem char_p.exists_unique (R : Type u_1) [non_assoc_semiring R] :
∃! (p : ), char_p R p
theorem char_p.congr {R : Type u} [add_monoid_with_one R] {p : } (q : ) [hq : char_p R q] (h : q = p) :
char_p R p
noncomputable def ring_char (R : Type u_1) [non_assoc_semiring R] :

Noncomputable function that outputs the unique characteristic of a semiring.

Equations
Instances for ring_char
theorem ring_char.spec (R : Type u_1) [non_assoc_semiring R] (x : ) :
theorem ring_char.eq (R : Type u_1) [non_assoc_semiring R] (p : ) [C : char_p R p] :
@[protected, instance]
theorem ring_char.of_eq {R : Type u_1} [non_assoc_semiring R] {p : } (h : ring_char R = p) :
char_p R p
theorem ring_char.eq_iff {R : Type u_1} [non_assoc_semiring R] {p : } :
theorem ring_char.dvd {R : Type u_1} [non_assoc_semiring R] {x : } (hx : x = 0) :
@[simp]
theorem ring_char.eq_zero {R : Type u_1} [non_assoc_semiring R] [char_zero R] :
@[simp]
theorem add_pow_char_of_commute (R : Type u_1) [semiring R] {p : } [hp : fact (nat.prime p)] [char_p R p] (x 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)] [char_p R p] (x 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)] [char_p R p] (x 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)] [char_p R p] {n : } (x y : R) (h : commute x y) :
(x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
theorem add_pow_char (R : Type u_1) [comm_semiring R] {p : } [fact (nat.prime p)] [char_p R p] (x y : R) :
(x + y) ^ p = x ^ p + y ^ p
theorem add_pow_char_pow (R : Type u_1) [comm_semiring R] {p : } [fact (nat.prime p)] [char_p R p] {n : } (x y : R) :
(x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
theorem sub_pow_char (R : Type u_1) [comm_ring R] {p : } [fact (nat.prime p)] [char_p R p] (x y : R) :
(x - y) ^ p = x ^ p - y ^ p
theorem sub_pow_char_pow (R : Type u_1) [comm_ring R] {p : } [fact (nat.prime p)] [char_p R p] {n : } (x y : R) :
(x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n
theorem char_p.neg_one_ne_one (R : Type u_1) [ring R] (p : ) [char_p R p] [fact (2 < p)] :
-1 1
theorem char_p.neg_one_pow_char (R : Type u_1) [comm_ring R] (p : ) [char_p R p] [fact (nat.prime p)] :
(-1) ^ p = -1
theorem char_p.neg_one_pow_char_pow (R : Type u_1) [comm_ring R] (p n : ) [char_p R p] [fact (nat.prime p)] :
(-1) ^ p ^ n = -1
theorem ring_hom.char_p_iff_char_p {K : Type u_1} {L : Type u_2} [division_ring K] [semiring L] [nontrivial L] (f : K →+* L) (p : ) :
char_p K p char_p L p
def frobenius (R : Type u_1) [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] :
R →+* R

The frobenius map that sends x to x^p

Equations
theorem frobenius_def {R : Type u_1} [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] (x : R) :
(frobenius R p) x = x ^ p
theorem iterate_frobenius {R : Type u_1} [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] (x : R) (n : ) :
(frobenius R p)^[n] x = x ^ p ^ n
theorem frobenius_mul {R : Type u_1} [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] (x y : R) :
(frobenius R p) (x * y) = (frobenius R p) x * (frobenius R p) y
theorem frobenius_one {R : Type u_1} [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] :
(frobenius R p) 1 = 1
theorem monoid_hom.map_frobenius {R : Type u_1} [comm_semiring R] {S : Type v} [comm_semiring S] (f : R →* S) (p : ) [fact (nat.prime p)] [char_p R p] [char_p S p] (x : R) :
f ((frobenius R p) x) = (frobenius S p) (f x)
theorem ring_hom.map_frobenius {R : Type u_1} [comm_semiring R] {S : Type v} [comm_semiring S] (g : R →+* S) (p : ) [fact (nat.prime p)] [char_p R p] [char_p S p] (x : R) :
g ((frobenius R p) x) = (frobenius S p) (g x)
theorem monoid_hom.map_iterate_frobenius {R : Type u_1} [comm_semiring R] {S : Type v} [comm_semiring S] (f : R →* S) (p : ) [fact (nat.prime p)] [char_p R p] [char_p S p] (x : R) (n : ) :
f ((frobenius R p)^[n] x) = (frobenius S p)^[n] (f x)
theorem ring_hom.map_iterate_frobenius {R : Type u_1} [comm_semiring R] {S : Type v} [comm_semiring S] (g : R →+* S) (p : ) [fact (nat.prime p)] [char_p R p] [char_p S p] (x : R) (n : ) :
g ((frobenius R p)^[n] x) = (frobenius S p)^[n] (g x)
theorem monoid_hom.iterate_map_frobenius {R : Type u_1} [comm_semiring R] (x : R) (f : R →* R) (p : ) [fact (nat.prime p)] [char_p R p] (n : ) :
f^[n] ((frobenius R p) x) = (frobenius R p) (f^[n] x)
theorem ring_hom.iterate_map_frobenius {R : Type u_1} [comm_semiring R] (x : R) (f : R →+* R) (p : ) [fact (nat.prime p)] [char_p R p] (n : ) :
f^[n] ((frobenius R p) x) = (frobenius R p) (f^[n] x)
theorem frobenius_zero (R : Type u_1) [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] :
(frobenius R p) 0 = 0
theorem frobenius_add (R : Type u_1) [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] (x y : R) :
(frobenius R p) (x + y) = (frobenius R p) x + (frobenius R p) y
theorem frobenius_nat_cast (R : Type u_1) [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] (n : ) :
theorem list_sum_pow_char {R : Type u_1} [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] (l : list R) :
l.sum ^ p = (list.map (λ (_x : R), _x ^ p) l).sum
theorem multiset_sum_pow_char {R : Type u_1} [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] (s : multiset R) :
s.sum ^ p = (multiset.map (λ (_x : R), _x ^ p) s).sum
theorem sum_pow_char {R : Type u_1} [comm_semiring R] (p : ) [fact (nat.prime p)] [char_p R p] {ι : Type u_2} (s : finset ι) (f : ι R) :
s.sum (λ (i : ι), f i) ^ p = s.sum (λ (i : ι), f i ^ p)
theorem frobenius_neg (R : Type u_1) [comm_ring R] (p : ) [fact (nat.prime p)] [char_p R p] (x : R) :
(frobenius R p) (-x) = -(frobenius R p) x
theorem frobenius_sub (R : Type u_1) [comm_ring R] (p : ) [fact (nat.prime p)] [char_p R p] (x y : R) :
(frobenius R p) (x - y) = (frobenius R p) x - (frobenius R p) y
theorem frobenius_inj (R : Type u_1) [comm_ring R] [is_reduced R] (p : ) [fact (nat.prime p)] [char_p R p] :
theorem is_square_of_char_two' {R : Type u_1} [finite R] [comm_ring R] [is_reduced R] [char_p R 2] (a : R) :

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

theorem char_p.cast_eq_mod (R : Type u_1) [non_assoc_ring R] (p : ) [char_p R p] (k : ) :
k = (k % p)
theorem char_p.char_ne_zero_of_finite (R : Type u_1) [non_assoc_ring R] (p : ) [char_p R p] [finite R] :
p 0

The characteristic of a finite ring cannot be zero.

@[simp]
theorem char_p.pow_prime_pow_mul_eq_one_iff {R : Type u_1} [comm_ring R] [is_reduced R] (p k m : ) [fact (nat.prime p)] [char_p R p] (x : R) :
x ^ (p ^ k * m) = 1 x ^ m = 1
theorem char_p.char_ne_one (R : Type u_1) [non_assoc_semiring R] [nontrivial R] (p : ) [hc : char_p R p] :
p 1
theorem char_p.char_is_prime_of_two_le (R : Type u_1) [non_assoc_semiring R] [no_zero_divisors R] (p : ) [hc : char_p R p] (hp : 2 p) :
theorem char_p.char_is_prime (R : Type u_1) [ring R] [no_zero_divisors R] [nontrivial R] [finite R] (p : ) [char_p R p] :
@[protected, instance]
theorem char_p.nontrivial_of_char_ne_one {R : Type u_1} [non_assoc_semiring R] {v : } (hv : v 1) [hr : char_p R v] :
theorem char_p.ring_char_of_prime_eq_zero {R : Type u_1} [non_assoc_semiring R] [nontrivial R] {p : } (hprime : nat.prime p) (hp0 : p = 0) :
@[protected]
theorem ring.two_ne_zero {R : Type u_1} [non_assoc_semiring R] [nontrivial R] (hR : ring_char 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_1} [non_assoc_ring R] [nontrivial R] (hR : ring_char 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_1} [non_assoc_ring R] [nontrivial R] [no_zero_divisors R] (hR : ring_char R 2) {a : R} :
-a = a a = 0

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

theorem char_p_of_ne_zero (R : Type u_1) [non_assoc_ring R] [fintype R] (n : ) (hn : fintype.card R = n) (hR : (i : ), i < n i = 0 i = 0) :
char_p R n
theorem char_p_of_prime_pow_injective (R : Type u_1) [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) :
char_p R (p ^ n)
@[protected, instance]
def nat.lcm.char_p (R : Type u_1) (S : Type v) [add_monoid_with_one R] [add_monoid_with_one S] (p q : ) [char_p R p] [char_p S q] :
char_p (R × S) (p.lcm q)

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

@[protected, instance]
def prod.char_p (R : Type u_1) (S : Type v) [add_monoid_with_one R] [add_monoid_with_one S] (p : ) [char_p R p] [char_p S p] :
char_p (R × S) p

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

@[protected, instance]
def ulift.char_p (R : Type u_1) [add_monoid_with_one R] (p : ) [char_p R p] :
@[protected, instance]
def mul_opposite.char_p (R : Type u_1) [add_monoid_with_one R] (p : ) [char_p R p] :
theorem int.cast_inj_on_of_ring_char_ne_two {R : Type u_1} [non_assoc_ring R] [nontrivial R] (hR : ring_char R 2) :
set.inj_on coe {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 ne_zero.of_not_dvd (R : Type u_1) [add_monoid_with_one R] {n p : } [char_p R p] (h : ¬p n) :
theorem ne_zero.not_char_dvd (R : Type u_1) [add_monoid_with_one R] (p : ) [char_p R p] (k : ) [h : ne_zero k] :
¬p k