mathlib docs: algebra.char

source

@[class]

structure char_p (α : Type u) [semiring α] (p : ℕ) :

Prop

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

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

Instances

source

theorem char_p.cast_eq_zero (α : Type u) [semiring α] (p : ℕ) [char_p α p] :

↑p = 0

source

@[simp]

theorem char_p.cast_card_eq_zero (R : Type u_1) [ring R] [fintype R] :

↑(fintype.card R) = 0

source

theorem char_p.int_cast_eq_zero_iff (R : Type u) [ring R] (p : ℕ) [char_p R p] (a : ℤ) :

↑a = 0 ↔ ↑p ∣ a

source

theorem char_p.int_coe_eq_int_coe_iff (R : Type u_1) [ring R] (p : ℕ) [char_p R p] (a b : ℤ) :

↑a = ↑b ↔ a ≡ b [ZMOD ↑p]

source

theorem char_p.eq (α : Type u) [semiring α] {p q : ℕ} (c1 : char_p α p) (c2 : char_p α q) :

p = q

source

@[instance]

def char_p.of_char_zero (α : Type u) [semiring α] [char_zero α] :

char_p α 0

source

theorem char_p.exists (α : Type u) [semiring α] :

∃ (p : ℕ), char_p α p

source

theorem char_p.exists_unique (α : Type u) [semiring α] :

∃! (p : ℕ), char_p α p

source

def ring_char (α : Type u) [semiring α] :

ℕ

Noncomputable function that outputs the unique characteristic of a semiring.

Equations

ring_char α = classical.some _

source

theorem ring_char.spec (α : Type u) [semiring α] (x : ℕ) :

↑x = 0 ↔ ring_char α ∣ x

source

theorem ring_char.eq (α : Type u) [semiring α] {p : ℕ} (C : char_p α p) :

p = ring_char α

source

theorem add_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 add_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 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 (α : Type u) [comm_ring α] {p : ℕ} [fact (nat.prime p)] [char_p α p] (x y : α) :

(x + y) ^ p = x ^ p + y ^ p

source

theorem add_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 sub_pow_char (α : Type u) [comm_ring α] {p : ℕ} [fact (nat.prime p)] [char_p α p] (x y : α) :

(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_1) [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_1) [ring R] (p : ℕ) [char_p R p] [fact (2 < p)] :

-1 ≠ 1

source

def frobenius (R : Type u) [comm_ring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] :

R →+* R

The frobenius map that sends x to x^p

Equations

frobenius R p = {to_fun := λ (x : R), x ^ p, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

theorem frobenius_def {R : Type u} [comm_ring 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_ring 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_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_one {R : Type u} [comm_ring 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_ring R] {S : Type v} [comm_ring 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_ring R] {S : Type v} [comm_ring 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_ring R] {S : Type v} [comm_ring 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_ring R] {S : Type v} [comm_ring 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_ring 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_ring 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_ring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] :

⇑(frobenius R p) 0 = 0

source

theorem frobenius_add (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_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_nat_cast (R : Type u) [comm_ring R] (p : ℕ) [fact (nat.prime p)] [char_p R p] (n : ℕ) :

⇑(frobenius R p) ↑n = ↑n

source

theorem frobenius_inj (α : Type u) [integral_domain α] (p : ℕ) [fact (nat.prime p)] [char_p α p] :

function.injective ⇑(frobenius α p)

source

theorem char_p.char_p_to_char_zero (α : Type u) [ring α] [char_p α 0] :

char_zero α

source

theorem char_p.cast_eq_mod (α : Type u) [ring α] (p : ℕ) [char_p α p] (k : ℕ) :

↑k = ↑(k % p)

source

theorem char_p.char_ne_zero_of_fintype (α : Type u) [ring α] (p : ℕ) [hc : char_p α p] [fintype α] :

p ≠ 0

source

theorem char_p.char_ne_one (α : Type u) [integral_domain α] (p : ℕ) [hc : char_p α p] :

p ≠ 1

source

theorem char_p.char_is_prime_of_two_le (α : Type u) [integral_domain α] (p : ℕ) [hc : char_p α p] (hp : 2 ≤ p) :

nat.prime p

source

theorem char_p.char_is_prime_or_zero (α : Type u) [integral_domain α] (p : ℕ) [hc : char_p α p] :

nat.prime p ∨ p = 0

source

theorem char_p.char_is_prime_of_pos (α : Type u) [integral_domain α] (p : ℕ) [h : fact (0 < p)] [char_p α p] :

fact (nat.prime p)

source

theorem char_p.char_is_prime (α : Type u) [integral_domain α] [fintype α] (p : ℕ) [char_p α p] :

nat.prime p

source

@[instance]

def char_p.subsingleton {R : Type u_1} [semiring R] [char_p R 1] :

subsingleton R

source

theorem char_p.false_of_nontrivial_of_char_one {R : Type u_1} [semiring R] [nontrivial R] [char_p R 1] :

false

source

theorem char_p.ring_char_ne_one {R : Type u_1} [semiring R] [nontrivial R] :

ring_char R ≠ 1

source

theorem char_p.nontrivial_of_char_ne_one {v : ℕ} (hv : v ≠ 1) {R : Type u_1} [semiring R] [hr : char_p R v] :

nontrivial R

source

theorem char_p_of_ne_zero (n : ℕ) (R : Type u_1) [comm_ring R] [fintype R] (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_1) [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)

mathlib documentation

Characteristic of semirings