doc-next-gen

Mathlib.Algebra.CharP.Algebra

Module docstring

{"# 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

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

Instances constructed from this result: - Any FreeAlgebra R X has the same characteristic as R. - The FractionRing R of an integral domain R has the same characteristic as R.

","As an application, a ℚ-algebra has characteristic zero. ","An algebra over a field has the same characteristic as the field. "}

CharP.dvd_of_ringHom theorem
{R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (p q : ℕ) [CharP R p] [CharP A q] : q ∣ p
Full source 
/-- Given `R →+* A`, then `char A ∣ char R`. -/
theorem CharP.dvd_of_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A]
    (f : R →+* A) (p q : ℕ) [CharP R p] [CharP A q] : q ∣ p := by
  refine (CharP.cast_eq_zero_iff A q p).mp ?_
  rw [← map_natCast f p, CharP.cast_eq_zero, map_zero]
Divisibility of Characteristics under Ring Homomorphisms
Informal description
Let $R$ and $A$ be non-associative semirings, and let $f \colon R \to A$ be a ring homomorphism. If $R$ has characteristic $p$ and $A$ has characteristic $q$, then $q$ divides $p$.
CharP.of_ringHom_of_ne_zero theorem
{R A : Type*} [NonAssocSemiring R] [NoZeroDivisors R] [NonAssocSemiring A] [Nontrivial A] (f : R →+* A) (p : ℕ) (hp : p ≠ 0) [CharP R p] : CharP A p
Full source 
/-- Given `R →+* A`, where `R` is a domain with `char R > 0`, then `char A = char R`. -/
theorem CharP.of_ringHom_of_ne_zero {R A : Type*} [NonAssocSemiring R] [NoZeroDivisors R]
    [NonAssocSemiring A] [Nontrivial A]
    (f : R →+* A) (p : ℕ) (hp : p ≠ 0) [CharP R p] : CharP A p := by
  have := f.domain_nontrivial
  have H := (CharP.char_is_prime_or_zero R p).resolve_right hp
  obtain ⟨q, hq⟩ := CharP.exists A
  obtain ⟨k, e⟩ := dvd_of_ringHom f p q
  have := Nat.isUnit_iff.mp ((H.2 e).resolve_left (Nat.isUnit_iff.not.mpr (char_ne_one A q)))
  rw [this, mul_one] at e
  exact e ▸ hq
Preservation of Nonzero Characteristic under Ring Homomorphisms for Semirings without Zero Divisors
Informal description
Let $R$ and $A$ be non-associative semirings, where $R$ has no zero divisors and $A$ is nontrivial. Given a ring homomorphism $f \colon R \to A$ and a nonzero natural number $p$, if $R$ has characteristic $p$, then $A$ also has characteristic $p$.
charP_of_injective_ringHom theorem
{R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A} (h : Function.Injective f) (p : ℕ) [CharP R p] : CharP A p
Full source 
/-- If a ring homomorphism `R →+* A` is injective then `A` has the same characteristic as `R`. -/
theorem charP_of_injective_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A]
    {f : R →+* A} (h : Function.Injective f) (p : ℕ) [CharP R p] : CharP A p where
  cast_eq_zero_iff x := by
    rw [← CharP.cast_eq_zero_iff R p x, ← map_natCast f x, map_eq_zero_iff f h]
Preservation of Characteristic under Injective Ring Homomorphisms
Informal description
Let $R$ and $A$ be non-associative semirings, and let $f \colon R \to A$ be an injective ring homomorphism. If $R$ has characteristic $p$, then $A$ also has characteristic $p$.
charP_of_injective_algebraMap theorem
{R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] (h : Function.Injective (algebraMap R A)) (p : ℕ) [CharP R p] : CharP A p
Full source 
/-- If the algebra map `R →+* A` is injective then `A` has the same characteristic as `R`. -/
theorem charP_of_injective_algebraMap {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    (h : Function.Injective (algebraMap R A)) (p : ℕ) [CharP R p] : CharP A p :=
  charP_of_injective_ringHom h p
Preservation of Characteristic under Injective Algebra Maps
Informal description
Let $R$ be a commutative semiring and $A$ a semiring with an algebra structure over $R$. If the algebra map $R \to A$ is injective, then for any natural number $p$, if $R$ has characteristic $p$, then $A$ also has characteristic $p$.
charP_of_injective_algebraMap' theorem
(R A : Type*) [Field R] [Semiring A] [Algebra R A] [Nontrivial A] (p : ℕ) [CharP R p] : CharP A p
Full source 
theorem charP_of_injective_algebraMap' (R A : Type*) [Field R] [Semiring A] [Algebra R A]
    [Nontrivial A] (p : ℕ) [CharP R p] : CharP A p :=
  charP_of_injective_algebraMap (algebraMap R A).injective p
Preservation of Characteristic under Field Algebra Maps
Informal description
Let $R$ be a field and $A$ a nontrivial semiring with an algebra structure over $R$. For any natural number $p$, if $R$ has characteristic $p$, then $A$ also has characteristic $p$.
charZero_of_injective_ringHom theorem
{R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A} (h : Function.Injective f) [CharZero R] : CharZero A
Full source 
/-- If a ring homomorphism `R →+* A` is injective and `R` has characteristic zero
then so does `A`. -/
theorem charZero_of_injective_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A]
    {f : R →+* A} (h : Function.Injective f) [CharZero R] : CharZero A where
  cast_injective _ _ _ := CharZero.cast_injective <| h <| by simpa only [map_natCast f]
Injective Ring Homomorphism Preserves Characteristic Zero
Informal description
Let $R$ and $A$ be non-associative semirings, and let $f \colon R \to A$ be an injective ring homomorphism. If $R$ has characteristic zero, then $A$ also has characteristic zero.
charZero_of_injective_algebraMap theorem
{R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] (h : Function.Injective (algebraMap R A)) [CharZero R] : CharZero A
Full source 
/-- If the algebra map `R →+* A` is injective and `R` has characteristic zero then so does `A`. -/
theorem charZero_of_injective_algebraMap {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    (h : Function.Injective (algebraMap R A)) [CharZero R] : CharZero A :=
  charZero_of_injective_ringHom h
Injective Algebra Map Preserves Characteristic Zero
Informal description
Let $R$ be a commutative semiring and $A$ a semiring with an algebra structure over $R$. If the algebra map $R \to A$ is injective and $R$ has characteristic zero, then $A$ also has characteristic zero.
RingHom.charP theorem
{R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (H : Function.Injective f) (p : ℕ) [CharP A p] : CharP R p
Full source 
/-- 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 {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
    (H : Function.Injective f) (p : ℕ) [CharP A p] : CharP R p := by
  obtain ⟨q, h⟩ := CharP.exists R
  exact CharP.eq _ (charP_of_injective_ringHom H q) ‹CharP A p› ▸ h
Injective Ring Homomorphism Reflects Characteristic
Informal description
Let $R$ and $A$ be non-associative semirings, and let $f \colon R \to A$ be an injective ring homomorphism. If $A$ has characteristic $p$, then $R$ also has characteristic $p$.
RingHom.charP_iff theorem
{R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (H : Function.Injective f) (p : ℕ) : CharP R p ↔ CharP A p
Full source 
/-- 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`. -/
protected theorem RingHom.charP_iff {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A]
    (f : R →+* A) (H : Function.Injective f) (p : ℕ) : CharPCharP R p ↔ CharP A p :=
  ⟨fun _ ↦ charP_of_injective_ringHom H p, fun _ ↦ f.charP H p⟩
Characteristic Equivalence under Injective Ring Homomorphisms
Informal description
Let $R$ and $A$ be non-associative semirings, and let $f \colon R \to A$ be an injective ring homomorphism. For any natural number $p$, the semiring $R$ has characteristic $p$ if and only if $A$ has characteristic $p$.
expChar_of_injective_ringHom theorem
{R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A} (h : Function.Injective f) (q : ℕ) [hR : ExpChar R q] : ExpChar A q
Full source 
/-- If a ring homomorphism `R →+* A` is injective then `A` has the same exponential characteristic
as `R`. -/
lemma expChar_of_injective_ringHom {R A : Type*}
    [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A} (h : Function.Injective f)
    (q : ℕ) [hR : ExpChar R q] : ExpChar A q := by
  rcases hR with _ | hprime
  · haveI := charZero_of_injective_ringHom h; exact .zero
  haveI := charP_of_injective_ringHom h q; exact .prime hprime
Injective Ring Homomorphism Preserves Exponential Characteristic
Informal description
Let $R$ and $A$ be non-associative semirings, and let $f \colon R \to A$ be an injective ring homomorphism. If $R$ has exponential characteristic $q$, then $A$ also has exponential characteristic $q$.
RingHom.expChar theorem
{R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (H : Function.Injective f) (p : ℕ) [ExpChar A p] : ExpChar R p
Full source 
/-- If `R →+* A` is injective, and `A` is of exponential characteristic `p`, then `R` is also of
exponential characteristic `p`. Similar to `RingHom.charZero`. -/
lemma RingHom.expChar {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
    (H : Function.Injective f) (p : ℕ) [ExpChar A p] : ExpChar R p := by
  cases ‹ExpChar A p› with
  | zero => haveI := f.charZero; exact .zero
  | prime hp => haveI := f.charP H p; exact .prime hp
Injective Ring Homomorphism Reflects Exponential Characteristic
Informal description
Let $R$ and $A$ be non-associative semirings, and let $f \colon R \to A$ be an injective ring homomorphism. If $A$ has exponential characteristic $p$, then $R$ also has exponential characteristic $p$.
RingHom.expChar_iff theorem
{R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (H : Function.Injective f) (p : ℕ) : ExpChar R p ↔ ExpChar A p
Full source 
/-- If `R →+* A` is injective, then `R` is of exponential characteristic `p` if and only if `A` is
also of exponential characteristic `p`. Similar to `RingHom.charZero_iff`. -/
lemma RingHom.expChar_iff {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
    (H : Function.Injective f) (p : ℕ) : ExpCharExpChar R p ↔ ExpChar A p :=
  ⟨fun _ ↦ expChar_of_injective_ringHom H p, fun _ ↦ f.expChar H p⟩
Injective Ring Homomorphism Preserves and Reflects Exponential Characteristic
Informal description
Let $R$ and $A$ be non-associative semirings, and let $f \colon R \to A$ be an injective ring homomorphism. For any natural number $p$, the semiring $R$ has exponential characteristic $p$ if and only if $A$ has exponential characteristic $p$.
expChar_of_injective_algebraMap theorem
{R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] (h : Function.Injective (algebraMap R A)) (q : ℕ) [ExpChar R q] : ExpChar A q
Full source 
/-- If the algebra map `R →+* A` is injective then `A` has the same exponential characteristic
as `R`. -/
lemma expChar_of_injective_algebraMap {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    (h : Function.Injective (algebraMap R A)) (q : ℕ) [ExpChar R q] : ExpChar A q :=
  expChar_of_injective_ringHom h q
Injective algebra map preserves exponential characteristic
Informal description
Let $R$ be a commutative semiring and $A$ a semiring with an algebra structure over $R$. If the algebra map $R \to A$ is injective, then $A$ has the same exponential characteristic as $R$. That is, if $R$ has exponential characteristic $q$, then $A$ also has exponential characteristic $q$.
algebraRat.charP_zero theorem
[Semiring R] [Algebra ℚ R] : CharP R 0
Full source 
/-- 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.charP_zero [Semiring R] [Algebra ℚ R] : CharP R 0 :=
  charP_of_injective_algebraMap (algebraMap ℚ R).injective 0
Characteristic Zero of $\mathbb{Q}$-Algebras
Informal description
For any semiring $R$ with an algebra structure over the rational numbers $\mathbb{Q}$, the characteristic of $R$ is zero.
algebraRat.charZero theorem
[Ring R] [Algebra ℚ R] : CharZero R
Full source 
/-- 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.
-/
theorem algebraRat.charZero [Ring R] [Algebra ℚ R] : CharZero R :=
  @CharP.charP_to_charZero R _ (algebraRat.charP_zero R)
Characteristic Zero of Nontrivial $\mathbb{Q}$-Algebras
Informal description
For any nontrivial ring $R$ with an algebra structure over the rational numbers $\mathbb{Q}$, the canonical map from the natural numbers $\mathbb{N}$ to $R$ is injective (i.e., $R$ has characteristic zero).
RingHom.charP_iff_charP theorem
{K L : Type*} [DivisionRing K] [NonAssocSemiring L] [Nontrivial L] (f : K →+* L) (p : ℕ) : CharP K p ↔ CharP L p
Full source 
lemma RingHom.charP_iff_charP {K L : Type*} [DivisionRing K] [NonAssocSemiring L] [Nontrivial L]
    (f : K →+* L) (p : ℕ) : CharPCharP K p ↔ CharP L p := by
  simp only [charP_iff, ← f.injective.eq_iff, map_natCast f, map_zero f]
Characteristic Equivalence under Ring Homomorphisms from Division Rings to Nontrivial Semirings
Informal description
Let $K$ be a division ring and $L$ a nontrivial non-associative semiring. For any ring homomorphism $f \colon K \to L$ and any natural number $p$, the characteristic of $K$ is $p$ if and only if the characteristic of $L$ is $p$.
Algebra.charP_iff theorem
(p : ℕ) : CharP K p ↔ CharP L p
Full source 
protected theorem Algebra.charP_iff (p : ℕ) : CharPCharP K p ↔ CharP L p :=
  (algebraMap K L).charP_iff_charP p
Characteristic Equivalence for Field Algebras: $\text{char}(K) = p \leftrightarrow \text{char}(L) = p$
Informal description
Let $K$ and $L$ be fields with $K$ being a $L$-algebra. For any natural number $p$, the characteristic of $K$ is $p$ if and only if the characteristic of $L$ is $p$.
Algebra.ringChar_eq theorem
: ringChar K = ringChar L
Full source 
theorem Algebra.ringChar_eq : ringChar K = ringChar L := by
  rw [ringChar.eq_iff, Algebra.charP_iff K L]
  apply ringChar.charP
Characteristic Equality for Field Algebras: $\text{char}(K) = \text{char}(L)$
Informal description
Let $K$ be a field and $L$ a $K$-algebra. Then the characteristic of $K$ equals the characteristic of $L$, i.e., $\text{char}(K) = \text{char}(L)$.
FreeAlgebra.charP instance
[CharP R p] : CharP (FreeAlgebra R X) p
Full source 
/-- If `R` has characteristic `p`, then so does `FreeAlgebra R X`. -/
instance charP [CharP R p] : CharP (FreeAlgebra R X) p :=
  charP_of_injective_algebraMap FreeAlgebra.algebraMap_leftInverse.injective p
Characteristic of Free Algebra Matches Base Ring
Informal description
For any commutative semiring $R$ with characteristic $p$ and any type $X$, the free algebra $\text{FreeAlgebra}\, R\, X$ also has characteristic $p$.
FreeAlgebra.charZero instance
[CharZero R] : CharZero (FreeAlgebra R X)
Full source 
/-- If `R` has characteristic `0`, then so does `FreeAlgebra R X`. -/
instance charZero [CharZero R] : CharZero (FreeAlgebra R X) :=
  charZero_of_injective_algebraMap FreeAlgebra.algebraMap_leftInverse.injective
Characteristic Zero of Free Algebras
Informal description
For any commutative semiring $R$ with characteristic zero and any type $X$, the free algebra $\text{FreeAlgebra}\, R\, X$ also has characteristic zero.
IsFractionRing.charP_of_isFractionRing theorem
[CharP R p] : CharP K p
Full source 
/-- If `R` has characteristic `p`, then so does Frac(R). -/
theorem charP_of_isFractionRing [CharP R p] : CharP K p :=
  charP_of_injective_algebraMap (IsFractionRing.injective R K) p
Preservation of Characteristic in Fraction Fields: $\text{char}(K) = \text{char}(R)$
Informal description
Let $R$ be a commutative ring and $K$ a field of fractions of $R$. If $R$ has characteristic $p$, then $K$ also has characteristic $p$.
IsFractionRing.charZero_of_isFractionRing theorem
[CharZero R] : CharZero K
Full source 
/-- If `R` has characteristic `0`, then so does Frac(R). -/
theorem charZero_of_isFractionRing [CharZero R] : CharZero K :=
  @CharP.charP_to_charZero K _ (charP_of_isFractionRing R 0)
Characteristic Zero Preservation in Fraction Fields
Informal description
If $R$ is a commutative ring of characteristic zero and $K$ is a field of fractions of $R$, then $K$ also has characteristic zero.
IsFractionRing.charP instance
[CharP R p] : CharP (FractionRing R) p
Full source 
/-- If `R` has characteristic `p`, then so does `FractionRing R`. -/
instance charP [CharP R p] : CharP (FractionRing R) p :=
  charP_of_isFractionRing R p
Characteristic of Fraction Ring Matches Base Ring
Informal description
If a commutative ring $R$ has characteristic $p$, then its fraction ring $\mathrm{Frac}(R)$ also has characteristic $p$.
IsFractionRing.charZero instance
[CharZero R] : CharZero (FractionRing R)
Full source 
/-- If `R` has characteristic `0`, then so does `FractionRing R`. -/
instance charZero [CharZero R] : CharZero (FractionRing R) :=
  charZero_of_isFractionRing R
Characteristic Zero Preservation in Fraction Rings
Informal description
If a commutative ring $R$ has characteristic zero, then its fraction ring $\mathrm{Frac}(R)$ also has characteristic zero.