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) [Semiring R] : ℕ → Prop

The definition of the exponential characteristic of a semiring.

• zero: ∀ {R : Type u} [inst : Semiring R] [inst_1 : CharZero R], ExpChar R 1
• prime: ∀ {R : Type u} [inst : Semiring R] {q : ℕ}, Nat.Prime q → ∀ [hchar : CharP R q], ExpChar R q

instance expChar_prime (R : Type u) [Semiring R] (p : ℕ) [CharP R p] [Fact (Nat.Prime p)] : ExpChar R p

Equations

• ⋯ = ⋯

instance expChar_zero (R : Type u) [Semiring R] [CharZero R] : ExpChar R 1

Equations

• ⋯ = ⋯

instance instExpCharProdInstSemiring (R : Type u) [Semiring R] (S : Type u_1) [Semiring S] (p : ℕ) [ExpChar R p] [ExpChar S p] : ExpChar (R × S) p

Equations

• ⋯ = ⋯

theorem ExpChar.eq {R : Type u} [Semiring R] {p : ℕ} {q : ℕ} (hp : ExpChar R p) (hq : ExpChar R q) : p = q

The exponential characteristic is unique.

theorem ExpChar.congr (R : Type u) [Semiring R] {p : ℕ} (q : ℕ) [hq : ExpChar R q] (h : q = p) : ExpChar R p

noncomputable def ringExpChar (R : Type u_1) [NonAssocSemiring R] : ℕ

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

Equations

• ringExpChar R = max (ringChar R) 1

theorem ringExpChar.eq (R : Type u) [Semiring R] (q : ℕ) [h : ExpChar R q] : ringExpChar R = q

@[simp]

theorem ringExpChar.eq_one (R : Type u_1) [NonAssocSemiring R] [CharZero R] : ringExpChar R = 1

theorem expChar_one_of_char_zero (R : Type u) [Semiring R] (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) [Semiring R] (p : ℕ) (q : ℕ) [hp : CharP R p] [hq : ExpChar R q] : p = q ↔ Nat.Prime p

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

theorem char_zero_of_expChar_one (R : Type u) [Semiring R] [Nontrivial R] (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) [Semiring R] [Nontrivial R] [hq : ExpChar R 1] : CharZero R

The characteristic is zero if the exponential characteristic is one.

theorem expChar_one_iff_char_zero (R : Type u) [Semiring R] [Nontrivial R] (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) [Semiring R] [Nontrivial R] [NoZeroDivisors R] {p : ℕ} [hp : CharP R p] (p_ne_zero : p ≠ 0) : Nat.Prime p

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

theorem expChar_is_prime_or_one (R : Type u) [Semiring R] (q : ℕ) [hq : ExpChar R q] : Nat.Prime 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) [Semiring R] (q : ℕ) [ExpChar R q] : 0 < q

The exponential characteristic is positive.

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

Any power of the exponential characteristic is positive.

theorem ExpChar.exists (R : Type u) [Ring R] [IsDomain R] : ∃ (q : ℕ), ExpChar R q

theorem ExpChar.exists_unique (R : Type u) [Ring R] [IsDomain R] : ∃! q : ℕ, ExpChar R q

instance ringExpChar.expChar (R : Type u) [Ring R] [IsDomain R] : ExpChar R (ringExpChar R)

Equations

• ⋯ = ⋯

theorem ringExpChar.of_eq {R : Type u} [Ring R] [IsDomain R] {q : ℕ} (h : ringExpChar R = q) : ExpChar R q

theorem ringExpChar.eq_iff {R : Type u} [Ring R] [IsDomain R] {q : ℕ} : ringExpChar R = q ↔ ExpChar R q

theorem expChar_of_injective_ringHom {R : Type u_1} {A : Type u_2} [Semiring R] [Semiring A] {f : R →+* A} (h : Function.Injective ⇑f) (q : ℕ) [hR : ExpChar R q] : ExpChar A 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} [Semiring R] [Semiring A] (f : R →+* A) (H : Function.Injective ⇑f) (p : ℕ) [ExpChar A p] : ExpChar R 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} [Semiring R] [Semiring A] (f : R →+* A) (H : Function.Injective ⇑f) (p : ℕ) : ExpChar R p ↔ ExpChar A 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} [CommSemiring R] [Semiring A] [Algebra R A] (h : Function.Injective ⇑(algebraMap R A)) (q : ℕ) [ExpChar R q] : ExpChar A 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) [Semiring R] {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) [Semiring 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 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) [CommSemiring R] {q : ℕ} [hR : ExpChar R q] (x : R) (y : R) : (x + y) ^ q = x ^ q + y ^ q

theorem add_pow_expChar_pow (R : Type u) [CommSemiring R] {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) [CommRing R] {q : ℕ} [hR : ExpChar R q] (x : R) (y : R) : (x - y) ^ q = x ^ q - y ^ q

theorem sub_pow_expChar_pow (R : Type u) [CommRing R] {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) [CommSemiring R] (p : ℕ) [ExpChar R p] : R →+* R

The frobenius map that sends x to x^p

Equations

• frobenius R p = let __spread.0 := powMonoidHom p; { toMonoidHom := __spread.0, map_zero' := ⋯, map_add' := ⋯ }

def iterateFrobenius (R : Type u) [CommSemiring R] (p : ℕ) (n : ℕ) [ExpChar R p] : R →+* R

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

Equations

• iterateFrobenius R p n = let __spread.0 := powMonoidHom (p ^ n); { toMonoidHom := __spread.0, map_zero' := ⋯, map_add' := ⋯ }

theorem frobenius_def {R : Type u} [CommSemiring R] (p : ℕ) [ExpChar R p] (x : R) : (frobenius R p) x = x ^ p

theorem iterateFrobenius_def {R : Type u} [CommSemiring R] (p : ℕ) (n : ℕ) [ExpChar R p] (x : R) : (iterateFrobenius R p n) x = x ^ p ^ n

theorem iterate_frobenius {R : Type u} [CommSemiring R] (p : ℕ) (n : ℕ) [ExpChar R p] (x : R) : (⇑(frobenius R p))^[n] x = x ^ p ^ n

theorem coe_iterateFrobenius (R : Type u) [CommSemiring R] (p : ℕ) (n : ℕ) [ExpChar R p] : ⇑(iterateFrobenius R p n) = (⇑(frobenius R p))^[n]

theorem iterateFrobenius_one_apply (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] (x : R) : (iterateFrobenius R p 1) x = x ^ p

@[simp]

theorem iterateFrobenius_one (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] : iterateFrobenius R p 1 = frobenius R p

theorem iterateFrobenius_zero_apply (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] (x : R) : (iterateFrobenius R p 0) x = x

@[simp]

theorem iterateFrobenius_zero (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] : iterateFrobenius R p 0 = RingHom.id R

theorem iterateFrobenius_add_apply (R : Type u) [CommSemiring R] (p : ℕ) (m : ℕ) (n : ℕ) [ExpChar R p] (x : R) : (iterateFrobenius R p (m + n)) x = (iterateFrobenius R p m) ((iterateFrobenius R p n) x)

theorem iterateFrobenius_add (R : Type u) [CommSemiring R] (p : ℕ) (m : ℕ) (n : ℕ) [ExpChar R p] : iterateFrobenius R p (m + n) = RingHom.comp (iterateFrobenius R p m) (iterateFrobenius R p n)

theorem iterateFrobenius_mul_apply (R : Type u) [CommSemiring R] (p : ℕ) (m : ℕ) (n : ℕ) [ExpChar R p] (x : R) : (iterateFrobenius R p (m * n)) x = (⇑(iterateFrobenius R p m))^[n] x

theorem coe_iterateFrobenius_mul (R : Type u) [CommSemiring R] (p : ℕ) (m : ℕ) (n : ℕ) [ExpChar R p] : ⇑(iterateFrobenius R p (m * n)) = (⇑(iterateFrobenius R p m))^[n]

theorem frobenius_mul {R : Type u} [CommSemiring R] (p : ℕ) [ExpChar R p] (x : R) (y : R) : (frobenius R p) (x * y) = (frobenius R p) x * (frobenius R p) y

theorem frobenius_one {R : Type u} [CommSemiring R] (p : ℕ) [ExpChar R p] : (frobenius R p) 1 = 1

theorem MonoidHom.map_frobenius {R : Type u} [CommSemiring R] {S : Type u_1} [CommSemiring S] (f : R →* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) : f ((frobenius R p) x) = (frobenius S p) (f x)

theorem RingHom.map_frobenius {R : Type u} [CommSemiring R] {S : Type u_1} [CommSemiring S] (g : R →+* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) : g ((frobenius R p) x) = (frobenius S p) (g x)

theorem MonoidHom.map_iterate_frobenius {R : Type u} [CommSemiring R] {S : Type u_1} [CommSemiring S] (f : R →* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) (n : ℕ) : f ((⇑(frobenius R p))^[n] x) = (⇑(frobenius S p))^[n] (f x)

theorem RingHom.map_iterate_frobenius {R : Type u} [CommSemiring R] {S : Type u_1} [CommSemiring S] (g : R →+* S) (p : ℕ) [ExpChar R p] [ExpChar S p] (x : R) (n : ℕ) : g ((⇑(frobenius R p))^[n] x) = (⇑(frobenius S p))^[n] (g x)

theorem MonoidHom.iterate_map_frobenius {R : Type u} [CommSemiring R] (x : R) (f : R →* R) (p : ℕ) [ExpChar R p] (n : ℕ) : (⇑f)^[n] ((frobenius R p) x) = (frobenius R p) ((⇑f)^[n] x)

theorem RingHom.iterate_map_frobenius {R : Type u} [CommSemiring R] (x : R) (f : R →+* R) (p : ℕ) [ExpChar R p] (n : ℕ) : (⇑f)^[n] ((frobenius R p) x) = (frobenius R p) ((⇑f)^[n] x)

def LinearMap.frobenius (R : Type u) [CommSemiring R] (S : Type u_1) [CommSemiring S] (p : ℕ) [ExpChar R p] [ExpChar S p] [Algebra R S] : S →ₛₗ[frobenius R p] S

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

Equations

• LinearMap.frobenius R S p = let __spread.0 := frobenius S p; { toAddHom := { toFun := __spread.0.toFun, map_add' := ⋯ }, map_smul' := ⋯ }

def LinearMap.iterateFrobenius (R : Type u) [CommSemiring R] (S : Type u_1) [CommSemiring S] (p : ℕ) (n : ℕ) [ExpChar R p] [ExpChar S p] [Algebra R S] : S →ₛₗ[iterateFrobenius R p n] S

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

Equations

• LinearMap.iterateFrobenius R S p n = let __spread.0 := iterateFrobenius S p n; { toAddHom := { toFun := __spread.0.toFun, map_add' := ⋯ }, map_smul' := ⋯ }

theorem LinearMap.frobenius_def (R : Type u) [CommSemiring R] (S : Type u_1) [CommSemiring S] (p : ℕ) [ExpChar R p] [ExpChar S p] [Algebra R S] (x : S) : (LinearMap.frobenius R S p) x = x ^ p

theorem LinearMap.iterateFrobenius_def (R : Type u) [CommSemiring R] (S : Type u_1) [CommSemiring S] (p : ℕ) [ExpChar R p] [ExpChar S p] [Algebra R S] (n : ℕ) (x : S) : (LinearMap.iterateFrobenius R S p n) x = x ^ p ^ n

theorem frobenius_zero (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] : (frobenius R p) 0 = 0

theorem frobenius_add (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] (x : R) (y : R) : (frobenius R p) (x + y) = (frobenius R p) x + (frobenius R p) y

theorem frobenius_natCast (R : Type u) [CommSemiring R] (p : ℕ) [ExpChar R p] (n : ℕ) : (frobenius R p) ↑n = ↑n

theorem list_sum_pow_char {R : Type u} [CommSemiring R] (p : ℕ) [ExpChar R p] (l : List R) : List.sum l ^ p = List.sum (List.map (fun (x : R) => x ^ p) l)

theorem multiset_sum_pow_char {R : Type u} [CommSemiring R] (p : ℕ) [ExpChar R p] (s : Multiset R) : Multiset.sum s ^ p = Multiset.sum (Multiset.map (fun (x : R) => x ^ p) s)

theorem sum_pow_char {R : Type u} [CommSemiring R] (p : ℕ) [ExpChar R p] {ι : Type u_2} (s : Finset ι) (f : ι → R) : (Finset.sum s fun (i : ι) => f i) ^ p = Finset.sum s fun (i : ι) => f i ^ p

theorem list_sum_pow_char_pow {R : Type u} [CommSemiring R] (p : ℕ) [ExpChar R p] (n : ℕ) (l : List R) : List.sum l ^ p ^ n = List.sum (List.map (fun (x : R) => x ^ p ^ n) l)

theorem multiset_sum_pow_char_pow {R : Type u} [CommSemiring R] (p : ℕ) [ExpChar R p] (n : ℕ) (s : Multiset R) : Multiset.sum s ^ p ^ n = Multiset.sum (Multiset.map (fun (x : R) => x ^ p ^ n) s)

theorem sum_pow_char_pow {R : Type u} [CommSemiring R] (p : ℕ) [ExpChar R p] (n : ℕ) {ι : Type u_2} (s : Finset ι) (f : ι → R) : (Finset.sum s fun (i : ι) => f i) ^ p ^ n = Finset.sum s fun (i : ι) => f i ^ p ^ n

theorem frobenius_neg (R : Type u) [CommRing R] (p : ℕ) [ExpChar R p] (x : R) : (frobenius R p) (-x) = -(frobenius R p) x

theorem frobenius_sub (R : Type u) [CommRing R] (p : ℕ) [ExpChar R p] (x : R) (y : R) : (frobenius R p) (x - y) = (frobenius R p) x - (frobenius R p) y