HepLean Documentation

Mathlib.Algebra.CharZero.Defs

Characteristic zero #

A ring R is called of characteristic zero if every natural number n is non-zero when considered as an element of R. Since this definition doesn't mention the multiplicative structure of R except for the existence of 1 in this file characteristic zero is defined for additive monoids with 1.

Main definition #

CharZero is the typeclass of an additive monoid with one such that the natural homomorphism from the natural numbers into it is injective.

TODO #

source
class CharZero (R : Type u_1) [AddMonoidWithOne R] :
Prop

Typeclass for monoids with characteristic zero. (This is usually stated on fields but it makes sense for any additive monoid with 1.)

Warning: for a semiring R, CharZero R and CharP R 0 need not coincide.

  • CharZero R requires an injection ℕ ↪ R;
  • CharP R 0 asks that only 0 : ℕ maps to 0 : R under the map ℕ → R. For instance, endowing {0, 1} with addition given by max (i.e. 1 is absorbing), shows that CharZero {0, 1} does not hold and yet CharP {0, 1} 0 does. This example is formalized in Counterexamples/CharPZeroNeCharZero.lean.
  • cast_injective : Function.Injective Nat.cast

    An additive monoid with one has characteristic zero if the canonical map ℕ → R is injective.

Instances
    source
    theorem charZero_of_inj_zero {R : Type u_1} [AddGroupWithOne R] (H : ∀ (n : ℕ), ↑n = 0 → n = 0) :
    CharZero R
    source
    theorem Nat.cast_injective {R : Type u_1} [AddMonoidWithOne R] [CharZero R] :
    Function.Injective Nat.cast
    source
    @[simp]
    theorem Nat.cast_inj {R : Type u_1} [AddMonoidWithOne R] [CharZero R] {m n : ℕ} :
    ↑m = ↑n ↔ m = n
    source
    @[simp]
    theorem Nat.cast_eq_zero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] {n : ℕ} :
    ↑n = 0 ↔ n = 0
    source
    theorem Nat.cast_ne_zero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] {n : ℕ} :
    ↑n ≠ 0 ↔ n ≠ 0
    source
    theorem Nat.cast_add_one_ne_zero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] (n : ℕ) :
    ↑n + 1 ≠ 0
    source
    @[simp]
    theorem Nat.cast_eq_one {R : Type u_1} [AddMonoidWithOne R] [CharZero R] {n : ℕ} :
    ↑n = 1 ↔ n = 1
    source
    theorem Nat.cast_ne_one {R : Type u_1} [AddMonoidWithOne R] [CharZero R] {n : ℕ} :
    ↑n ≠ 1 ↔ n ≠ 1
    source
    @[instance 100]
    instance Nat.AtLeastTwo.toNeZero (n : ℕ) [n.AtLeastTwo] :
    NeZero n
    Equations
    • ⋯ = ⋯
    source
    @[simp]
    theorem OfNat.ofNat_ne_zero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] (n : ℕ) [n.AtLeastTwo] :
    OfNat.ofNat n ≠ 0
    source
    @[simp]
    theorem OfNat.zero_ne_ofNat {R : Type u_1} [AddMonoidWithOne R] [CharZero R] (n : ℕ) [n.AtLeastTwo] :
    0 ≠ OfNat.ofNat n
    source
    @[simp]
    theorem OfNat.ofNat_ne_one {R : Type u_1} [AddMonoidWithOne R] [CharZero R] (n : ℕ) [n.AtLeastTwo] :
    OfNat.ofNat n ≠ 1
    source
    @[simp]
    theorem OfNat.one_ne_ofNat {R : Type u_1} [AddMonoidWithOne R] [CharZero R] (n : ℕ) [n.AtLeastTwo] :
    1 ≠ OfNat.ofNat n
    source
    @[simp]
    theorem OfNat.ofNat_eq_ofNat {R : Type u_1} [AddMonoidWithOne R] [CharZero R] {m n : ℕ} [m.AtLeastTwo] [n.AtLeastTwo] :
    OfNat.ofNat m = OfNat.ofNat n ↔ OfNat.ofNat m = OfNat.ofNat n
    source
    instance NeZero.charZero {M : Type u_2} {n : ℕ} [NeZero n] [AddMonoidWithOne M] [CharZero M] :
    NeZero ↑n
    Equations
    • ⋯ = ⋯
    source
    instance NeZero.charZero_one {M : Type u_2} [AddMonoidWithOne M] [CharZero M] :
    NeZero 1
    Equations
    • ⋯ = ⋯
    source
    instance NeZero.charZero_ofNat {M : Type u_2} {n : ℕ} [n.AtLeastTwo] [AddMonoidWithOne M] [CharZero M] :
    NeZero (OfNat.ofNat n)
    Equations
    • ⋯ = ⋯