mathlib documentation

algebra.char_p.basic

Characteristic of semirings #

source
@[class]
structure char_p (R : Type u) [add_monoid R] [has_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
source
theorem char_p.cast_eq_zero (R : Type u) [add_monoid R] [has_one R] (p : ℕ) [char_p R p] :
↑p = 0
source
@[simp]
theorem char_p.cast_card_eq_zero (R : Type u) [add_group R] [has_one R] [fintype R] :
↑(fintype.card R) = 0
source
theorem char_p.int_cast_eq_zero_iff (R : Type u) [add_group R] [has_one R] (p : ℕ) [char_p R p] (a : ℤ) :
↑a = 0 ↔ ↑p ∣ a
source
theorem char_p.int_coe_eq_int_coe_iff (R : Type u) [add_group R] [has_one R] (p : ℕ) [char_p R p] (a b : ℤ) :
↑a = ↑b ↔ a ≡ b [ZMOD ↑p]
source
theorem char_p.eq (R : Type u) [add_monoid R] [has_one R] {p q : ℕ} (c1 : char_p R p) (c2 : char_p R q) :
p = q
source
@[protected, instance]
def char_p.of_char_zero (R : Type u) [add_monoid R] [has_one R] [char_zero R] :
char_p R 0
source
theorem char_p.exists (R : Type u) [non_assoc_semiring R] :
∃ (p : ℕ), char_p R p
source
theorem char_p.exists_unique (R : Type u) [non_assoc_semiring R] :
∃! (p : ℕ), char_p R p
source
theorem char_p.congr {R : Type u} [add_monoid R] [has_one R] {p : ℕ} (q : ℕ) [hq : char_p R q] (h : q = p) :
char_p R p
source
noncomputable def ring_char (R : Type u) [non_assoc_semiring R] :
ℕ

Noncomputable function that outputs the unique characteristic of a semiring.

Equations
source
theorem ring_char.spec (R : Type u) [non_assoc_semiring R] (x : ℕ) :
↑x = 0 ↔ ring_char R ∣ x
source
theorem ring_char.eq (R : Type u) [non_assoc_semiring R] (p : ℕ) [C : char_p R p] :
ring_char R = p
source
@[protected, instance]
def ring_char.char_p (R : Type u) [non_assoc_semiring R] :
char_p R (ring_char R)
source
theorem ring_char.of_eq {R : Type u} [non_assoc_semiring R] {p : ℕ} (h : ring_char R = p) :
char_p R p
source
theorem ring_char.eq_iff {R : Type u} [non_assoc_semiring R] {p : ℕ} :
ring_char R = p ↔ char_p R p
source
theorem ring_char.dvd {R : Type u} [non_assoc_semiring R] {x : ℕ} (hx : ↑x = 0) :
ring_char R ∣ x
source
@[simp]
theorem ring_char.eq_zero {R : Type u} [non_assoc_semiring R] [char_zero R] :
ring_char R = 0
source
theorem add_pow_char_of_commute (R : Type u) [semiring R] {p : ℕ} [fact (nat.prime p)] [char_p R p] (x y : R) (h : commute x y) :
(x + y) ^ p = x ^ p + y ^ p
source
theorem add_pow_char_pow_of_commute (R : Type u) [semiring 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
source
theorem sub_pow_char_of_commute (R : Type u) [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
source
theorem sub_pow_char_pow_of_commute (R : Type u) [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
source
theorem add_pow_char (R : Type u) [comm_semiring R] {p : ℕ} [fact (nat.prime p)] [char_p R p] (x y : R) :
(x + y) ^ p = x ^ p + y ^ p
source
theorem add_pow_char_pow (R : Type u) [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
source
theorem sub_pow_char (R : Type u) [comm_ring R] {p : ℕ} [fact (nat.prime p)] [char_p R p] (x y : R) :
(x - y) ^ p = x ^ p - y ^ p
source
theorem sub_pow_char_pow (R : Type u) [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
source
theorem eq_iff_modeq_int (R : Type u) [ring R] (p : ℕ) [char_p R p] (a b : ℤ) :
↑a = ↑b ↔ a ≡ b [ZMOD ↑p]
source
theorem char_p.neg_one_ne_one (R : Type u) [ring R] (p : ℕ) [char_p R p] [fact (2 < p)] :
-1 ≠ 1
source
theorem char_p.neg_one_pow_char (R : Type u) [comm_ring R] (p : ℕ) [char_p R p] [fact (nat.prime p)] :
(-1) ^ p = -1
source
theorem char_p.neg_one_pow_char_pow (R : Type u) [comm_ring R] (p n : ℕ) [char_p R p] [fact (nat.prime p)] :
(-1) ^ p ^ n = -1
source
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
source
def frobenius (R : Type u) [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] :
R →+* R

The frobenius map that sends x to x^p

Equations
source
theorem frobenius_def {R : Type u} [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] (x : R) :
⇑(frobenius R p) x = x ^ p
source
theorem iterate_frobenius {R : Type u} [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] (x : R) (n : ℕ) :
⇑(frobenius R p)^[n] x = x ^ p ^ n
source
theorem frobenius_mul {R : Type u} [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
source
theorem frobenius_one {R : Type u} [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] :
⇑(frobenius R p) 1 = 1
source
theorem monoid_hom.map_frobenius {R : Type u} [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)
source
theorem ring_hom.map_frobenius {R : Type u} [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)
source
theorem monoid_hom.map_iterate_frobenius {R : Type u} [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)
source
theorem ring_hom.map_iterate_frobenius {R : Type u} [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)
source
theorem monoid_hom.iterate_map_frobenius {R : Type u} [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)
source
theorem ring_hom.iterate_map_frobenius {R : Type u} [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)
source
theorem frobenius_zero (R : Type u) [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] :
⇑(frobenius R p) 0 = 0
source
theorem frobenius_add (R : Type u) [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
source
theorem frobenius_nat_cast (R : Type u) [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] (n : ℕ) :
⇑(frobenius R p) ↑n = ↑n
source
theorem list_sum_pow_char {R : Type u} [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
source
theorem multiset_sum_pow_char {R : Type u} [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
source
theorem sum_pow_char {R : Type u} [comm_semiring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] {ι : Type u_1} (s : finset ι) (f : ι → R) :
(∑ (i : ι) in s, f i) ^ p = ∑ (i : ι) in s, f i ^ p
source
theorem frobenius_neg (R : Type u) [comm_ring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] (x : R) :
⇑(frobenius R p) (-x) = -⇑(frobenius R p) x
source
theorem frobenius_sub (R : Type u) [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
source
theorem frobenius_inj (R : Type u) [comm_ring R] [is_reduced R] (p : ℕ) [fact (nat.prime p)] [char_p R p] :
function.injective ⇑(frobenius R p)
source
theorem char_p.char_p_to_char_zero (R : Type u_1) [add_left_cancel_monoid R] [has_one R] [char_p R 0] :
char_zero R
source
theorem char_p.cast_eq_mod (R : Type u) [ring R] (p : ℕ) [char_p R p] (k : ℕ) :
↑k = ↑(k % p)
source
theorem char_p.char_ne_zero_of_fintype (R : Type u) [ring R] (p : ℕ) [hc : char_p R p] [fintype R] :
p ≠ 0
source
theorem char_p.char_ne_one (R : Type u) [non_assoc_semiring R] [nontrivial R] (p : ℕ) [hc : char_p R p] :
p ≠ 1
source
theorem char_p.char_is_prime_of_two_le (R : Type u) [non_assoc_semiring R] [no_zero_divisors R] (p : ℕ) [hc : char_p R p] (hp : 2 ≤ p) :
nat.prime p
source
theorem char_p.char_is_prime_or_zero (R : Type u) [non_assoc_semiring R] [no_zero_divisors R] [nontrivial R] (p : ℕ) [hc : char_p R p] :
nat.prime p ∨ p = 0
source
theorem char_p.char_is_prime_of_pos (R : Type u) [non_assoc_semiring R] [no_zero_divisors R] [nontrivial R] (p : ℕ) [h : fact (0 < p)] [char_p R p] :
fact (nat.prime p)
source
theorem char_p.char_is_prime (R : Type u) [ring R] [no_zero_divisors R] [nontrivial R] [fintype R] (p : ℕ) [char_p R p] :
nat.prime p
source
@[protected, instance]
def char_p.subsingleton {R : Type u} [non_assoc_semiring R] [char_p R 1] :
subsingleton R
source
theorem char_p.false_of_nontrivial_of_char_one {R : Type u} [non_assoc_semiring R] [nontrivial R] [char_p R 1] :
false
source
theorem char_p.ring_char_ne_one {R : Type u} [non_assoc_semiring R] [nontrivial R] :
ring_char R ≠ 1
source
theorem char_p.nontrivial_of_char_ne_one {R : Type u} [non_assoc_semiring R] {v : ℕ} (hv : v ≠ 1) [hr : char_p R v] :
nontrivial R
source
theorem char_p.ring_char_of_prime_eq_zero {R : Type u} [non_assoc_semiring R] [nontrivial R] {p : ℕ} (hprime : nat.prime p) (hp0 : ↑p = 0) :
ring_char R = p
source
theorem char_p_of_ne_zero (R : Type u) [comm_ring R] [fintype R] (n : ℕ) (hn : fintype.card R = n) (hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0) :
char_p R n
source
theorem char_p_of_prime_pow_injective (R : Type u) [comm_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)
source
@[protected, instance]
def nat.lcm.char_p (R : Type u) (S : Type v) [semiring R] [semiring 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.

source
@[protected, instance]
def prod.char_p (R : Type u) (S : Type v) [semiring R] [semiring 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