Documentation

Mathlib.Algebra.CharP.ExpChar

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 #

Tags #

exponential characteristic, characteristic

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

The definition of the exponential characteristic of a semiring.

Instances
    instance expChar_prime (R : Type u) [Semiring R] (p : ) [CharP R p] [Fact (Nat.Prime p)] :
    Equations
    • =
    instance expChar_zero (R : Type u) [Semiring R] [CharZero R] :
    Equations
    • =
    instance instExpCharProd (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) :
    noncomputable def ringExpChar (R : Type u_1) [NonAssocSemiring R] :

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

    Equations
    theorem ringExpChar.eq (R : Type u) [Semiring R] (q : ) [h : ExpChar R q] :
    @[simp]
    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] :

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

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

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

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

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

    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] :
    Equations
    • =
    theorem ringExpChar.of_eq {R : Type u} [Ring R] [IsDomain R] {q : } (h : ringExpChar R = q) :
    theorem ringExpChar.eq_iff {R : Type u} [Ring R] [IsDomain 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] :

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

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

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

    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
    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
    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] :
    theorem iterateFrobenius_zero_apply (R : Type u) [CommSemiring R] (p : ) [ExpChar R p] (x : R) :
    (iterateFrobenius R p 0) x = x
    @[simp]
    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) = (iterateFrobenius R p m).comp (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] :

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

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

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

    Equations
    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
    @[deprecated frobenius_natCast]
    theorem frobenius_nat_cast (R : Type u) [CommSemiring R] (p : ) [ExpChar R p] (n : ) :
    (frobenius R p) n = n

    Alias of frobenius_natCast.

    theorem list_sum_pow_char {R : Type u} [CommSemiring R] (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} [CommSemiring R] (p : ) [ExpChar R p] (s : Multiset R) :
    s.sum ^ p = (Multiset.map (fun (x : R) => x ^ p) s).sum
    theorem sum_pow_char {R : Type u} [CommSemiring R] (p : ) [ExpChar R p] {ι : Type u_2} (s : Finset ι) (f : ιR) :
    (∑ is, f i) ^ p = is, f i ^ p
    theorem list_sum_pow_char_pow {R : Type u} [CommSemiring R] (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} [CommSemiring R] (p : ) [ExpChar R p] (n : ) (s : Multiset R) :
    s.sum ^ p ^ n = (Multiset.map (fun (x : R) => x ^ p ^ n) s).sum
    theorem sum_pow_char_pow {R : Type u} [CommSemiring R] (p : ) [ExpChar R p] (n : ) {ι : Type u_2} (s : Finset ι) (f : ιR) :
    (∑ is, f i) ^ p ^ n = is, 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