Characteristics of algebras

In this file we describe the characteristic of R-algebras.

In particular we are interested in the characteristic of free algebras over R and the fraction field FractionRing R.

Main results

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

Instances constructed from this result:

• Any FreeAlgebra R X has the same characteristic as R.
• The FractionRing R of an integral domain R has the same characteristic as R.

theorem charP_of_injective_ringHom {R : Type u_1} {A : Type u_2} [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A} (h : Function.Injective ⇑f) (p : ℕ) [CharP R p] : CharP A p

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

theorem charP_of_injective_algebraMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (h : Function.Injective ⇑(algebraMap R A)) (p : ℕ) [CharP R p] : CharP A p

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

theorem charP_of_injective_algebraMap' (R : Type u_1) (A : Type u_2) [Field R] [Semiring A] [Algebra R A] [Nontrivial A] (p : ℕ) [CharP R p] : CharP A p

theorem charZero_of_injective_ringHom {R : Type u_1} {A : Type u_2} [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A} (h : Function.Injective ⇑f) [CharZero R] : CharZero A

If a ring homomorphism R →+* A is injective and R has characteristic zero then so does A.

theorem charZero_of_injective_algebraMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (h : Function.Injective ⇑(algebraMap R A)) [CharZero R] : CharZero A

If the algebra map R →+* A is injective and R has characteristic zero then so does A.

theorem RingHom.charP {R : Type u_1} {A : Type u_2} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (H : Function.Injective ⇑f) (p : ℕ) [CharP A p] : CharP R p

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

theorem RingHom.charP_iff {R : Type u_1} {A : Type u_2} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (H : Function.Injective ⇑f) (p : ℕ) : CharP R p ↔ CharP A p

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

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.

As an application, a ℚ-algebra has characteristic zero.

theorem algebraRat.charP_zero (R : Type u_1) [Nontrivial R] [Semiring R] [Algebra ℚ R] : CharP R 0

A nontrivial ℚ-algebra has CharP equal to zero.

This cannot be a (local) instance because it would immediately form a loop with the instance DivisionRing.toRatAlgebra. It's probably easier to go the other way: prove CharZero R and automatically receive an Algebra ℚ R instance.

theorem algebraRat.charZero (R : Type u_1) [Nontrivial R] [Ring R] [Algebra ℚ R] : CharZero R

A nontrivial ℚ-algebra has characteristic zero.

This cannot be a (local) instance because it would immediately form a loop with the instance DivisionRing.toRatAlgebra. It's probably easier to go the other way: prove CharZero R and automatically receive an Algebra ℚ R instance.

An algebra over a field has the same characteristic as the field.

theorem Algebra.charP_iff (K : Type u_1) (L : Type u_2) [Field K] [CommSemiring L] [Nontrivial L] [Algebra K L] (p : ℕ) : CharP K p ↔ CharP L p

theorem Algebra.ringChar_eq (K : Type u_1) (L : Type u_2) [Field K] [CommSemiring L] [Nontrivial L] [Algebra K L] : ringChar K = ringChar L

instance FreeAlgebra.charP {R : Type u_1} {X : Type u_2} [CommSemiring R] (p : ℕ) [CharP R p] : CharP (FreeAlgebra R X) p

If R has characteristic p, then so does FreeAlgebra R X.

instance FreeAlgebra.charZero {R : Type u_1} {X : Type u_2} [CommSemiring R] [CharZero R] : CharZero (FreeAlgebra R X)

If R has characteristic 0, then so does FreeAlgebra R X.

theorem IsFractionRing.charP_of_isFractionRing (R : Type u_1) {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] (p : ℕ) [CharP R p] : CharP K p

If R has characteristic p, then so does Frac(R).

theorem IsFractionRing.charZero_of_isFractionRing (R : Type u_1) {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [CharZero R] : CharZero K

If R has characteristic 0, then so does Frac(R).

instance IsFractionRing.charP (R : Type u_1) [CommRing R] (p : ℕ) [IsDomain R] [CharP R p] : CharP (FractionRing R) p

If R has characteristic p, then so does FractionRing R.

instance IsFractionRing.charZero (R : Type u_1) [CommRing R] [IsDomain R] [CharZero R] : CharZero (FractionRing R)

If R has characteristic 0, then so does FractionRing R.