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
    Instances For
      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 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_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 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
      • frobenius R p = let __spread.0 := powMonoidHom p; { toMonoidHom := __spread.0, map_zero' := , map_add' := }
      Instances For
        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
        Instances For
          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
          Instances For
            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
            Instances For
              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