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 #

Instances constructed from this result:

theorem charP_of_injective_ringHom {R : Type u_1} {A : Type u_2} [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A} (h : Function.Injective f) (p : ) [CharP R p] :
CharP A p

If a ring homomorphism 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} [CommSemiring R] [Semiring A] [Algebra R A] (h : Function.Injective (algebraMap R A)) (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) [Field R] [Semiring A] [Algebra R A] [Nontrivial A] (p : ) [CharP R p] :
CharP A p
theorem charZero_of_injective_ringHom {R : Type u_1} {A : Type u_2} [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A} (h : Function.Injective f) [CharZero 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.

theorem RingHom.charP {R : Type u_1} {A : Type u_2} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (H : Function.Injective f) (p : ) [CharP A p] :
CharP R p

If R →+* A is injective, and A is of characteristic p, then R is also of characteristic p. Similar to RingHom.charZero.

theorem RingHom.charP_iff {R : Type u_1} {A : Type u_2} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (H : Function.Injective f) (p : ) :
CharP R p CharP A p

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.

theorem algebraRat.charP_zero (R : Type u_1) [Nontrivial R] [Semiring R] [Algebra R] :
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 DivisionRing.toRatAlgebra. 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) [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 DivisionRing.toRatAlgebra. 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) [Field K] [CommSemiring L] [Nontrivial L] [Algebra K L] (p : ) :
CharP K p CharP L p
theorem Algebra.ringChar_eq (K : Type u_1) (L : Type u_2) [Field K] [CommSemiring L] [Nontrivial L] [Algebra K L] :
instance FreeAlgebra.charP {R : Type u_1} {X : Type u_2} [CommSemiring R] (p : ) [CharP R p] :

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

Equations
  • =
instance FreeAlgebra.charZero {R : Type u_1} {X : Type u_2} [CommSemiring R] [CharZero R] :

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

Equations
  • =
theorem IsFractionRing.charP_of_isFractionRing (R : Type u_1) {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] (p : ) [CharP R p] :
CharP K p

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

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

instance IsFractionRing.charP (R : Type u_1) [CommRing R] (p : ) [IsDomain R] [CharP R p] :

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

Equations
  • =

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

Equations
  • =