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:

source
theorem charP_of_injective_ringHom {R : Type u_1} {A : Type u_2} [Semiring R] [Semiring 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.

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

source
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
source
theorem charZero_of_injective_ringHom {R : Type u_1} {A : Type u_2} [Semiring R] [Semiring A] {f : R →+* A} (h : Function.Injective ⇑f) [CharZero R] :
CharZero A

If a ring homomorphism R →+* A is injective and R has characteristic zero then so does A.

source
theorem charZero_of_injective_algebraMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (h : Function.Injective ⇑(algebraMap R A)) [CharZero R] :
CharZero 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 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 algebraRat. It's probably easier to go the other way: prove CharZero R and automatically receive an Algebra ℚ R instance.

source
theorem algebraRat.charZero (R : Type u_1) [Nontrivial R] [Ring R] [Algebra ℚ R] :
CharZero R

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.

source
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
source
theorem Algebra.ringChar_eq (K : Type u_1) (L : Type u_2) [Field K] [CommSemiring L] [Nontrivial L] [Algebra K L] :
ringChar K = ringChar L
source
instance FreeAlgebra.charP {R : Type u_1} {X : Type u_2} [CommSemiring R] (p : ℕ) [CharP R p] :
CharP (FreeAlgebra R X) p

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

Equations
source
instance FreeAlgebra.charZero {R : Type u_1} {X : Type u_2} [CommSemiring R] [CharZero R] :
CharZero (FreeAlgebra R X)

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

Equations
source
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).

source
theorem IsFractionRing.charZero_of_isFractionRing (R : Type u_1) {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [CharZero R] :
CharZero K

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

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

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

Equations
source
instance IsFractionRing.charZero (R : Type u_1) [CommRing R] [IsDomain R] [CharZero R] :
CharZero (FractionRing R)

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

Equations