# Exponential characteristic #

This file defines the exponential characteristic, which is defined to be 1 for a ring with characteristic 0 and the same as the ordinary characteristic, if the ordinary characteristic is prime. This concept is useful to simplify some theorem statements. This file establishes a few basic results relating it to the (ordinary characteristic). The definition is stated for a semiring, but the actual results are for nontrivial rings (as far as exponential characteristic one is concerned), respectively a ring without zero-divisors (for prime characteristic).

## Main results #

• ExpChar: the definition of exponential characteristic
• expChar_is_prime_or_one: the exponential characteristic is a prime or one
• char_eq_expChar_iff: the characteristic equals the exponential characteristic iff the characteristic is prime

## Tags #

exponential characteristic, characteristic

class inductive ExpChar (R : Type u) [] :

The definition of the exponential characteristic of a semiring.

Instances
instance expChar_prime (R : Type u) [] (p : ) [CharP R p] [Fact ()] :
Equations
• =
instance expChar_zero (R : Type u) [] [] :
Equations
• =
instance instExpCharProd (R : Type u) [] (S : Type u_1) [] (p : ) [ExpChar R p] [ExpChar S p] :
ExpChar (R × S) p
Equations
• =
theorem ExpChar.eq {R : Type u} [] {p : } {q : } (hp : ExpChar R p) (hq : ExpChar R q) :
p = q

The exponential characteristic is unique.

theorem ExpChar.congr (R : Type u) [] {p : } (q : ) [hq : ExpChar R q] (h : q = p) :
noncomputable def ringExpChar (R : Type u_1) [] :

Noncomputable function that outputs the unique exponential characteristic of a semiring.

Equations
Instances For
theorem ringExpChar.eq (R : Type u) [] (q : ) [h : ExpChar R q] :
= q
@[simp]
theorem ringExpChar.eq_one (R : Type u_1) [] [] :
= 1
theorem expChar_one_of_char_zero (R : Type u) [] (q : ) [hp : CharP R 0] [hq : ExpChar R q] :
q = 1

The exponential characteristic is one if the characteristic is zero.

theorem char_eq_expChar_iff (R : Type u) [] (p : ) (q : ) [hp : CharP R p] [hq : ExpChar R q] :
p = q

The characteristic equals the exponential characteristic iff the former is prime.

theorem char_zero_of_expChar_one (R : Type u) [] [] (p : ) [hp : CharP R p] [hq : ExpChar R 1] :
p = 0

The exponential characteristic is one if the characteristic is zero.

theorem charZero_of_expChar_one' (R : Type u) [] [] [hq : ExpChar R 1] :

The characteristic is zero if the exponential characteristic is one.

theorem expChar_one_iff_char_zero (R : Type u) [] [] (p : ) (q : ) [CharP R p] [ExpChar R q] :
q = 1 p = 0

The exponential characteristic is one iff the characteristic is zero.

theorem char_prime_of_ne_zero (R : Type u) [] [] [] {p : } [hp : CharP R p] (p_ne_zero : p 0) :

A helper lemma: the characteristic is prime if it is non-zero.

theorem expChar_is_prime_or_one (R : Type u) [] (q : ) [hq : ExpChar R q] :
q = 1

The exponential characteristic is a prime number or one. See also CharP.char_is_prime_or_zero.

theorem expChar_pos (R : Type u) [] (q : ) [ExpChar R q] :
0 < q

The exponential characteristic is positive.

theorem expChar_pow_pos (R : Type u) [] (q : ) [ExpChar R q] (n : ) :
0 < q ^ n

Any power of the exponential characteristic is positive.

theorem ExpChar.exists (R : Type u) [Ring R] [] :
∃ (q : ), ExpChar R q
theorem ExpChar.exists_unique (R : Type u) [Ring R] [] :
∃! q : , ExpChar R q
instance ringExpChar.expChar (R : Type u) [Ring R] [] :
ExpChar R ()
Equations
• =
theorem ringExpChar.of_eq {R : Type u} [Ring R] [] {q : } (h : = q) :
theorem ringExpChar.eq_iff {R : Type u} [Ring R] [] {q : } :
= q ExpChar R q
theorem expChar_of_injective_ringHom {R : Type u_1} {A : Type u_2} [] [] {f : R →+* A} (h : ) (q : ) [hR : ExpChar R q] :

If a ring homomorphism R →+* A is injective then A has the same exponential characteristic as R.

theorem RingHom.expChar {R : Type u_1} {A : Type u_2} [] [] (f : R →+* A) (H : ) (p : ) [ExpChar A p] :

If R →+* A is injective, and A is of exponential characteristic p, then R is also of exponential characteristic p. Similar to RingHom.charZero.

theorem RingHom.expChar_iff {R : Type u_1} {A : Type u_2} [] [] (f : R →+* A) (H : ) (p : ) :

If R →+* A is injective, then R is of exponential characteristic p if and only if A is also of exponential characteristic p. Similar to RingHom.charZero_iff.

theorem expChar_of_injective_algebraMap {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (h : Function.Injective ()) (q : ) [ExpChar R q] :

If the algebra map R →+* A is injective then A has the same exponential characteristic as R.

theorem add_pow_expChar_of_commute (R : Type u) [] {q : } [hR : ExpChar R q] (x : R) (y : R) (h : Commute x y) :
(x + y) ^ q = x ^ q + y ^ q
theorem add_pow_expChar_pow_of_commute (R : Type u) [] {q : } [hR : ExpChar R q] {n : } (x : R) (y : R) (h : Commute x y) :
(x + y) ^ q ^ n = x ^ q ^ n + y ^ q ^ n
theorem sub_pow_expChar_of_commute (R : Type u) [Ring R] {q : } [hR : ExpChar R q] (x : R) (y : R) (h : Commute x y) :
(x - y) ^ q = x ^ q - y ^ q
theorem sub_pow_expChar_pow_of_commute (R : Type u) [Ring R] {q : } [hR : ExpChar R q] {n : } (x : R) (y : R) (h : Commute x y) :
(x - y) ^ q ^ n = x ^ q ^ n - y ^ q ^ n
theorem add_pow_expChar (R : Type u) [] {q : } [hR : ExpChar R q] (x : R) (y : R) :
(x + y) ^ q = x ^ q + y ^ q
theorem add_pow_expChar_pow (R : Type u) [] {q : } [hR : ExpChar R q] {n : } (x : R) (y : R) :
(x + y) ^ q ^ n = x ^ q ^ n + y ^ q ^ n
theorem sub_pow_expChar (R : Type u) [] {q : } [hR : ExpChar R q] (x : R) (y : R) :
(x - y) ^ q = x ^ q - y ^ q
theorem sub_pow_expChar_pow (R : Type u) [] {q : } [hR : ExpChar R q] {n : } (x : R) (y : R) :
(x - y) ^ q ^ n = x ^ q ^ n - y ^ q ^ n
theorem ExpChar.neg_one_pow_expChar (R : Type u) [Ring R] (q : ) [hR : ExpChar R q] :
(-1) ^ q = -1
theorem ExpChar.neg_one_pow_expChar_pow (R : Type u) [Ring R] (q : ) (n : ) [hR : ExpChar R q] :
(-1) ^ q ^ n = -1
def frobenius (R : Type u) [] (p : ) [ExpChar R p] :
R →+* R

The frobenius map that sends x to x^p

Equations
Instances For
def iterateFrobenius (R : Type u) [] (p : ) (n : ) [ExpChar R p] :
R →+* R

The iterated frobenius map sending x to x^p^n

Equations
• = let __spread.0 := powMonoidHom (p ^ n); { toMonoidHom := __spread.0, map_zero' := , map_add' := }
Instances For
theorem frobenius_def {R : Type u} [] (p : ) [ExpChar R p] (x : R) :
() x = x ^ p
theorem iterateFrobenius_def {R : Type u} [] (p : ) (n : ) [ExpChar R p] (x : R) :
() x = x ^ p ^ n
theorem iterate_frobenius {R : Type u} [] (p : ) (n : ) [ExpChar R p] (x : R) :
(())^[n] x = x ^ p ^ n
theorem coe_iterateFrobenius (R : Type u) [] (p : ) (n : ) [ExpChar R p] :
() = (())^[n]
theorem iterateFrobenius_one_apply (R : Type u) [] (p : ) [ExpChar R p] (x : R) :
() x = x ^ p
@[simp]
theorem iterateFrobenius_one (R : Type u) [] (p : ) [ExpChar R p] :
=
theorem iterateFrobenius_zero_apply (R : Type u) [] (p : ) [ExpChar R p] (x : R) :
() x = x
@[simp]
theorem iterateFrobenius_zero (R : Type u) [] (p : ) [ExpChar R p] :
=
theorem iterateFrobenius_add_apply (R : Type u) [] (p : ) (m : ) (n : ) [ExpChar R p] (x : R) :
(iterateFrobenius R p (m + n)) x = () (() x)
theorem iterateFrobenius_add (R : Type u) [] (p : ) (m : ) (n : ) [ExpChar R p] :
iterateFrobenius R p (m + n) = ().comp ()
theorem iterateFrobenius_mul_apply (R : Type u) [] (p : ) (m : ) (n : ) [ExpChar R p] (x : R) :
(iterateFrobenius R p (m * n)) x = (())^[n] x
theorem coe_iterateFrobenius_mul (R : Type u) [] (p : ) (m : ) (n : ) [ExpChar R p] :
(iterateFrobenius R p (m * n)) = (())^[n]
theorem frobenius_mul {R : Type u} [] (p : ) [ExpChar R p] (x : R) (y : R) :
() (x * y) = () x * () y
theorem frobenius_one {R : Type u} [] (p : ) [ExpChar R p] :
() 1 = 1
theorem MonoidHom.map_frobenius {R : Type u} [] {S : Type u_1} [] (f : R →* S) (p : ) [ExpChar R p] [ExpChar S p] (x : R) :
f (() x) = () (f x)
theorem RingHom.map_frobenius {R : Type u} [] {S : Type u_1} [] (g : R →+* S) (p : ) [ExpChar R p] [ExpChar S p] (x : R) :
g (() x) = () (g x)
theorem MonoidHom.map_iterate_frobenius {R : Type u} [] {S : Type u_1} [] (f : R →* S) (p : ) [ExpChar R p] [ExpChar S p] (x : R) (n : ) :
f ((())^[n] x) = (())^[n] (f x)
theorem RingHom.map_iterate_frobenius {R : Type u} [] {S : Type u_1} [] (g : R →+* S) (p : ) [ExpChar R p] [ExpChar S p] (x : R) (n : ) :
g ((())^[n] x) = (())^[n] (g x)
theorem MonoidHom.iterate_map_frobenius {R : Type u} [] (x : R) (f : R →* R) (p : ) [ExpChar R p] (n : ) :
(f)^[n] (() x) = () ((f)^[n] x)
theorem RingHom.iterate_map_frobenius {R : Type u} [] (x : R) (f : R →+* R) (p : ) [ExpChar R p] (n : ) :
(f)^[n] (() x) = () ((f)^[n] x)
def LinearMap.frobenius (R : Type u) [] (S : Type u_1) [] (p : ) [ExpChar R p] [ExpChar S p] [Algebra R S] :

The frobenius map of an algebra as a frobenius-semilinear map.

Equations
Instances For
def LinearMap.iterateFrobenius (R : Type u) [] (S : Type u_1) [] (p : ) (n : ) [ExpChar R p] [ExpChar S p] [Algebra R S] :

The iterated frobenius map of an algebra as a iterated-frobenius-semilinear map.

Equations
Instances For
theorem LinearMap.frobenius_def (R : Type u) [] (S : Type u_1) [] (p : ) [ExpChar R p] [ExpChar S p] [Algebra R S] (x : S) :
() x = x ^ p
theorem LinearMap.iterateFrobenius_def (R : Type u) [] (S : Type u_1) [] (p : ) [ExpChar R p] [ExpChar S p] [Algebra R S] (n : ) (x : S) :
() x = x ^ p ^ n
theorem frobenius_zero (R : Type u) [] (p : ) [ExpChar R p] :
() 0 = 0
theorem frobenius_add (R : Type u) [] (p : ) [ExpChar R p] (x : R) (y : R) :
() (x + y) = () x + () y
theorem frobenius_natCast (R : Type u) [] (p : ) [ExpChar R p] (n : ) :
() n = n
@[deprecated frobenius_natCast]
theorem frobenius_nat_cast (R : Type u) [] (p : ) [ExpChar R p] (n : ) :
() n = n

Alias of frobenius_natCast.

theorem list_sum_pow_char {R : Type u} [] (p : ) [ExpChar R p] (l : List R) :
l.sum ^ p = (List.map (fun (x : R) => x ^ p) l).sum
theorem multiset_sum_pow_char {R : Type u} [] (p : ) [ExpChar R p] (s : ) :
s.sum ^ p = (Multiset.map (fun (x : R) => x ^ p) s).sum
theorem sum_pow_char {R : Type u} [] (p : ) [ExpChar R p] {ι : Type u_2} (s : ) (f : ιR) :
(is, f i) ^ p = is, f i ^ p
theorem list_sum_pow_char_pow {R : Type u} [] (p : ) [ExpChar R p] (n : ) (l : List R) :
l.sum ^ p ^ n = (List.map (fun (x : R) => x ^ p ^ n) l).sum
theorem multiset_sum_pow_char_pow {R : Type u} [] (p : ) [ExpChar R p] (n : ) (s : ) :
s.sum ^ p ^ n = (Multiset.map (fun (x : R) => x ^ p ^ n) s).sum
theorem sum_pow_char_pow {R : Type u} [] (p : ) [ExpChar R p] (n : ) {ι : Type u_2} (s : ) (f : ιR) :
(is, f i) ^ p ^ n = is, f i ^ p ^ n
theorem frobenius_neg (R : Type u) [] (p : ) [ExpChar R p] (x : R) :
() (-x) = -() x
theorem frobenius_sub (R : Type u) [] (p : ) [ExpChar R p] (x : R) (y : R) :
() (x - y) = () x - () y