# 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} [] [] {f : R →+* A} (h : ) (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} [] [] [Algebra R A] (h : Function.Injective ()) (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) [] [] [Algebra R A] [] (p : ) [CharP R p] :
CharP A p
theorem charZero_of_injective_ringHom {R : Type u_1} {A : Type u_2} [] [] {f : R →+* A} (h : ) [] :

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} [] [] [Algebra R A] (h : Function.Injective ()) [] :

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} [] [] (f : R →+* A) (H : ) (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} [] [] (f : R →+* A) (H : ) (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.

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

theorem algebraRat.charP_zero (R : Type u_1) [] [] [] :
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 algebraRat. 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) [] [Ring R] [] :

A nontrivial ℚ-algebra has characteristic zero.

This cannot be a (local) instance because it would immediately form a loop with the instance algebraRat. 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) [] [] [] [Algebra K L] (p : ) :
CharP K p CharP L p
theorem Algebra.ringChar_eq (K : Type u_1) (L : Type u_2) [] [] [] [Algebra K L] :
instance FreeAlgebra.charP {R : Type u_1} {X : Type u_2} [] (p : ) [CharP R p] :
CharP () p

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

Equations
• =
instance FreeAlgebra.charZero {R : Type u_1} {X : Type u_2} [] [] :

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

Equations
• =
theorem IsFractionRing.charP_of_isFractionRing (R : Type u_1) {K : Type u_2} [] [] [Algebra 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} [] [] [Algebra R K] [] [] :

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

instance IsFractionRing.charP (R : Type u_1) [] (p : ) [] [CharP R p] :
CharP () p

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

Equations
• =
instance IsFractionRing.charZero (R : Type u_1) [] [] [] :

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

Equations
• =