mathlib documentation

algebra.char_p.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 fraction_ring R.

Main results #

Instances constructed from this result:

theorem char_p_of_injective_algebra_map {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (h : function.injective (algebra_map R A)) (p : ) [char_p R p] :
char_p A p

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

theorem char_zero_of_injective_algebra_map {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (h : function.injective (algebra_map R A)) [char_zero R] :

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

@[instance]
def free_algebra.char_p {R : Type u_1} {X : Type u_2} [comm_semiring R] (p : ) [char_p R p] :

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

@[instance]
def free_algebra.char_zero {R : Type u_1} {X : Type u_2} [comm_semiring R] [char_zero R] :

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

theorem is_fraction_ring.char_p_of_is_fraction_ring (R : Type u_1) {K : Type u_2} [integral_domain R] [field K] [algebra R K] [is_fraction_ring R K] (p : ) [char_p R p] :
char_p K p

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

@[instance]
def is_fraction_ring.char_p (R : Type u_1) [integral_domain R] (p : ) [char_p R p] :

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

theorem is_fraction_ring.char_zero_of_is_fraction_ring (R : Type u_1) {K : Type u_2} [integral_domain R] [field K] [algebra R K] [is_fraction_ring R K] [char_zero R] :

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

@[instance]

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