CharP.quotient'
theorem CharP.quotient' :
∀ {R : Type u_1} [inst : CommRing R] (p : ℕ) [inst_1 : CharP R p] (I : Ideal R),
(∀ (x : ℕ), ↑x ∈ I → ↑x = 0) → CharP (R ⧸ I) p
This theorem, named `CharP.quotient'`, states that if in a commutative ring `R` with characteristic `p`, there exists an ideal `I` that does not contain any natural number coercions, except for zero, then the quotient structure `R ⧸ I` inherits the characteristic `p` of the original ring `R`. Here, the characteristic of a ring is a property that corresponds to the number of times you must add the multiplicative identity (1) to itself to reach the additive identity (0). In the case where no such number exists, the characteristic is defined to be zero.
More concisely: If `R` is a commutative ring with characteristic `p` and `I` is an ideal of `R` that does not contain any non-zero natural number coercions, then `R/I` has characteristic `p`.
|
CharP.quotient_iff
theorem CharP.quotient_iff :
∀ {R : Type u_1} [inst : CommRing R] (n : ℕ) [inst_1 : CharP R n] (I : Ideal R),
CharP (R ⧸ I) n ↔ ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
The theorem `CharP.quotient_iff` states that for any commutative ring `R` of characteristic `n`, and any ideal `I` in `R`, the quotient ring `R/I` has characteristic `n` if and only if for every natural number `x`, if the canonical image of `x` under the natural ring homomorphism from the integers to `R` lies in `I`, then it is equal to zero. More intuitively, it says that the characteristic of the quotient ring `R/I` is the same as the characteristic of `R` if all integers in `I` map to zero.
More concisely: The characteristic of a commutative ring's quotient by an ideal is equal to the ring's characteristic if and only if every integer mapped to an element in the ideal is zero.
|
CharP.quotient_iff_le_ker_natCast
theorem CharP.quotient_iff_le_ker_natCast :
∀ {R : Type u_1} [inst : CommRing R] (n : ℕ) [inst_1 : CharP R n] (I : Ideal R),
CharP (R ⧸ I) n ↔ Ideal.comap (Nat.castRingHom R) I ≤ RingHom.ker (Nat.castRingHom R)
This theorem, named `CharP.quotient_iff_le_ker_natCast`, states that for any commutative ring `R` with characteristic `n` and any ideal `I` of `R`, the quotient ring `R ⧸ I` has characteristic `n` if and only if the preimage of `I` under the natural number casting ring homomorphism is a subset of the kernel of the natural number casting ring homomorphism into `R`. In other words, it describes a condition on the relationship between an ideal in the ring and the characteristic of the ring that ensures the same characteristic is preserved in the quotient ring.
More concisely: The characteristic of a commutative ring's quotient ring by an ideal equals the characteristic of the ring if and only if the ideal contains the image of the natural number casting homomorphism.
|