# Documentation

Mathlib.Algebra.CharP.Algebra

# 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_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_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.

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.

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

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

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.

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

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