mathlib3 documentation

algebra.char_p.algebra

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 #

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

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

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

A nontrivial -algebra has characteristic 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.

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

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
theorem algebra.ring_char_eq (K : Type u_1) (L : Type u_2) [field K] [comm_semiring L] [nontrivial L] [algebra K L] :
@[protected, 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.

@[protected, 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} [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).

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

@[protected, instance]
def is_fraction_ring.char_p (R : Type u_1) [comm_ring R] (p : ) [is_domain R] [char_p R p] :

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

@[protected, instance]

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