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

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 →ₛₗ[_root_.frobenius R p] S

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

Equations

• LinearMap.frobenius R S p = { toFun := (↑↑(frobenius S p)).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 →ₛₗ[_root_.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 = { toFun := (↑↑(iterateFrobenius S p n)).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) : (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) : (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 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