mathlib docs: algebra.char

source

@[class]

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

ℕ → 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

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 : ℕ} :

char_p α p → char_p α q → p = q

source

@[instance]

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

char_p α 0

Equations

_ = _

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 α] :

ℕ

Noncomuptable 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 : ℕ} :

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) :

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

source

theorem add_pow_char (α : Type u) [comm_ring α] {p : ℕ} (hp : nat.prime p) [char_p α p] (x y : α) :

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

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 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] :

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

Equations

char_p.subsingleton = _

source

theorem char_p.false_of_nonzero_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

mathlib documentation

algebra.char_p

Characteristic of semirings

General documentation

Additional documentation

Library

mathlib documentation

algebra.​char_p

Characteristic of semirings

General documentation

Additional documentation

Library

algebra.char_p