Characteristics of algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

Instances constructed from this result:

Any free_algebra R X has the same characteristic as R.
The fraction_ring R of an integral domain R has the same characteristic as R.

source

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.

source

theorem char_p_of_injective_algebra_map' (R : Type u_1) (A : Type u_2) [field R] [semiring A] [algebra R A] [nontrivial A] (p : ℕ) [char_p R p] :

char_p A p

source

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] :

char_zero A

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.

source

theorem algebra_rat.char_p_zero (R : Type u_1) [nontrivial R] [semiring R] [algebra ℚ R] :

char_p R 0

A nontrivial ℚ-algebra has char_p equal to zero.

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

source

theorem algebra_rat.char_zero (R : Type u_1) [nontrivial R] [ring R] [algebra ℚ R] :

char_zero R

A nontrivial ℚ-algebra has characteristic zero.

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

source

theorem algebra.char_p_iff (K : Type u_1) (L : Type u_2) [field K] [comm_semiring L] [nontrivial L] [algebra K L] (p : ℕ) :

char_p K p ↔ char_p L p

source

theorem algebra.ring_char_eq (K : Type u_1) (L : Type u_2) [field K] [comm_semiring L] [nontrivial L] [algebra K L] :

ring_char K = ring_char L

source

@[protected, instance]

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

char_p (free_algebra R X) p

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

source

@[protected, instance]

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

char_zero (free_algebra R X)

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

source

theorem is_fraction_ring.char_p_of_is_fraction_ring (R : Type u_1) {K : Type u_2} [comm_ring 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).

source

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

char_zero K

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

source

@[protected, instance]

def is_fraction_ring.char_p (R : Type u_1) [comm_ring R] (p : ℕ) [is_domain R] [char_p R p] :

char_p (fraction_ring R) p

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

source

@[protected, instance]

def is_fraction_ring.char_zero (R : Type u_1) [comm_ring R] [is_domain R] [char_zero R] :

char_zero (fraction_ring R)

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