charP_of_injective_algebraMap
theorem charP_of_injective_algebraMap :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
Function.Injective ⇑(algebraMap R A) → ∀ (p : ℕ) [inst : CharP R p], CharP A p
The theorem `charP_of_injective_algebraMap` states that for any types `R` and `A`, where `R` is a commutative semiring and `A` is a semiring with an algebra structure over `R`, if the algebra map from `R` to `A` (which is a map induced by the ring homomorphism defined by the Algebra structure) is injective, then whenever `R` has a certain characteristic `p`, `A` will also have the same characteristic `p`. In mathematical terms, the characteristic of a ring is the smallest number of times you need to add the multiplicative identity, 1, together to get the additive identity, 0. If no such number exists, we say the ring has characteristic 0. Therefore, this theorem is stating a property about how the characteristics of rings are preserved under injective ring homomorphisms.
More concisely: If `R` is a commutative semiring with characteristic `p`, `A` is a semiring with an algebra structure over `R`, and the algebra map from `R` to `A` is injective, then `A` also has characteristic `p`.
|
IsFractionRing.charP_of_isFractionRing
theorem IsFractionRing.charP_of_isFractionRing :
∀ (R : Type u_1) {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K] (p : ℕ) [inst : CharP R p], CharP K p
The theorem `IsFractionRing.charP_of_isFractionRing` states that if an integral domain `R` has a characteristic `p`, then the field of fractions of `R`, denoted as `Frac(R)`, also has the characteristic `p`. In other words, if a prime number `p` is characteristic of an integral domain (meaning that multiplication by `p` acts like zero), then the same prime `p` is also characteristic of the field generated by the fractions of that domain.
More concisely: If an integral domain has characteristic `p`, then the field of fractions of that domain also has characteristic `p`.
|
IsFractionRing.charZero_of_isFractionRing
theorem IsFractionRing.charZero_of_isFractionRing :
∀ (R : Type u_1) {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K] [inst : CharZero R], CharZero K
The theorem `IsFractionRing.charZero_of_isFractionRing` states that if an integral domain `R` has characteristic `0`, then so does the field of fractions of `R`, denoted by `Frac(R)`. Here, characteristic `0` of a ring means that no positive integer multiplied by one in the ring equals zero. The field of fractions of an integral domain is a type of field extension where the elements are fractions of elements from the integral domain. This theorem is essentially saying that the property of having characteristic `0` is preserved when we go from an integral domain to its field of fractions.
More concisely: If an integral domain has characteristic 0, then so does its field of fractions.
|
charP_of_injective_ringHom
theorem charP_of_injective_ringHom :
∀ {R : Type u_1} {A : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring A] {f : R →+* A},
Function.Injective ⇑f → ∀ (p : ℕ) [inst : CharP R p], CharP A p
The theorem `charP_of_injective_ringHom` states that for any two types `R` and `A` that are both instances of a `NonAssocSemiring` (which is a particular type of mathematical structure), if there is an injective ring homomorphism `f` from `R` to `A`, then the characteristic of `A` is the same as the characteristic of `R`. Here, the characteristic of a ring is a nonnegative integer `p` (denoted `CharP R p` for `R` and `CharP A p` for `A`) that is defined such that all multiples of `p` are zero in the ring. An injective ring homomorphism is a function that preserves the ring structure and has the property that different inputs produce different outputs.
More concisely: If `f` is an injective homomorphism from a NonAssocSemiring `R` to a NonAssocSemiring `A`, then `CharP A (CharP R)` holds.
|
algebraRat.charZero
theorem algebraRat.charZero :
∀ (R : Type u_1) [inst : Nontrivial R] [inst : Ring R] [inst_1 : Algebra ℚ R], CharZero R
This theorem states that any nontrivial algebra over the rational numbers, denoted by `ℚ`, has characteristic zero. In other words, the minimum number of times you have to add the number one to itself to get zero (the characteristic of the ring) is zero. An important caveat is that this cannot be a (local) instance because it would immediately form a loop with the `algebraRat` instance. Instead, it's suggested to prove `CharZero R` to automatically receive an `Algebra ℚ R` instance. Note that `R` in this context is a ring, and `CharZero` is a property that a ring may possess, meaning that multiplication by any natural number is injective.
More concisely: Any nontrivial algebra over the rational numbers has characteristic 0. (In other words, the characteristic of a nontrivial algebra of rational numbers is 0.)
|
algebraRat.charP_zero
theorem algebraRat.charP_zero :
∀ (R : Type u_1) [inst : Nontrivial R] [inst : Semiring R] [inst_1 : Algebra ℚ R], CharP R 0
The theorem `algebraRat.charP_zero` states that for any type `R`, given that `R` is nontrivial, is a semiring, and is a ℚ-algebra, the characteristic of `R` is zero. This theorem can't be used as a (local) instance because it would create a loop with the `algebraRat` instance. A more straightforward approach might be to prove `CharZero R` and get an `Algebra ℚ R` instance automatically.
More concisely: If `R` is a nontrivial, semiring, and ℚ-algebra type, then the characteristic of `R` is zero.
|
charZero_of_injective_ringHom
theorem charZero_of_injective_ringHom :
∀ {R : Type u_1} {A : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring A] {f : R →+* A},
Function.Injective ⇑f → ∀ [inst : CharZero R], CharZero A
The theorem `charZero_of_injective_ringHom` states that for any two types `R` and `A`, with `R` being a non-associative semiring and `A` also being a non-associative semiring, and given a ring homomorphism `f` from `R` to `A`, if this ring homomorphism `f` is injective (which means that if `f(x) = f(y)` then `x = y`), and if `R` has characteristic zero (denoted by `CharZero R`), then `A` also has characteristic zero. In other words, the injectivity of a ring homomorphism preserves the characteristic zero property from the domain to the codomain.
More concisely: If `f` is an injective ring homomorphism from the non-associative semiring `R` of characteristic zero to the non-associative semiring `A`, then `A` also has characteristic zero.
|
Algebra.charP_iff
theorem Algebra.charP_iff :
∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : CommSemiring L] [inst_2 : Nontrivial L]
[inst_3 : Algebra K L] (p : ℕ), CharP K p ↔ CharP L p
The theorem `Algebra.charP_iff` states that for any two types `K` and `L`, where `K` is a field, `L` is a commutative semiring, and `L` is nontrivial and also an algebra over `K`, a natural number `p` is the characteristic of `K` if and only if `p` is the characteristic of `L`. The characteristic of a ring is the smallest positive integer such that multiplying the ring's multiplicative identity by this integer results in the ring's additive identity, if such an integer exists. Otherwise, the characteristic is defined to be zero.
More concisely: The characteristic of a field `K` is equal to the characteristic of a commutative semiring `L` that is an algebra over `K`, if `L` is a nontrivial commutative semiring.
|
charZero_of_injective_algebraMap
theorem charZero_of_injective_algebraMap :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
Function.Injective ⇑(algebraMap R A) → ∀ [inst : CharZero R], CharZero A
The theorem `charZero_of_injective_algebraMap` states that if the algebra map (`algebraMap`) from a commutative semiring `R` to a semiring `A` is injective (meaning that it preserves distinctness: if `f(x) = f(y)`, then `x = y`), and the commutative semiring `R` has characteristic zero (meaning that the number `n` in `R` such that `n * 1_R = 0_R` is `0`), then the semiring `A` also has characteristic zero.
More concisely: If `R` is a commutative semiring with characteristic zero and `algebraMap : R -> A` is an injective algebra homomorphism, then `A` has characteristic zero.
|