# 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`

.

If a ring homomorphism `R →+* A`

is injective then `A`

has the same characteristic as `R`

.

If the algebra map `R →+* A`

is injective then `A`

has the same characteristic as `R`

.

If a ring homomorphism `R →+* A`

is injective and `R`

has characteristic zero
then so does `A`

.

If the algebra map `R →+* A`

is injective and `R`

has characteristic zero then so does `A`

.

If `R →+* A`

is injective, and `A`

is of characteristic `p`

, then `R`

is also of
characteristic `p`

. Similar to `RingHom.charZero`

.

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.

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.

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.

If `R`

has characteristic `p`

, then so does `FreeAlgebra R X`

.

## Equations

- ⋯ = ⋯

If `R`

has characteristic `0`

, then so does `FreeAlgebra R X`

.

## Equations

- ⋯ = ⋯

If `R`

has characteristic `0`

, then so does Frac(R).

If `R`

has characteristic `p`

, then so does `FractionRing R`

.

## Equations

- ⋯ = ⋯

If `R`

has characteristic `0`

, then so does `FractionRing R`

.

## Equations

- ⋯ = ⋯