doc-next-gen

Mathlib.Algebra.CharZero.Defs

Module docstring

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

  • Unify with CharP (possibly using an out-parameter) "}
CharZero structure
(R) [AddMonoidWithOne R]
Full source 
/-- 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`.
-/
class CharZero (R) [AddMonoidWithOne R] : Prop where
  /-- An additive monoid with one has characteristic zero if the canonical map `ℕ → R` is
  injective. -/
  cast_injective : Function.Injective (Nat.cast : ℕ → R)
Characteristic zero monoid
Informal description
A structure representing an additive monoid with one \( R \) such that the canonical map from the natural numbers \( \mathbb{N} \) to \( R \) is injective. This means that for any natural number \( n \), if \( n \) is mapped to the zero element of \( R \), then \( n \) must be zero.
charZero_of_inj_zero theorem
[AddGroupWithOne R] (H : ∀ n : ℕ, (n : R) = 0 → n = 0) : CharZero R
Full source 
theorem charZero_of_inj_zero [AddGroupWithOne R] (H : ∀ n : ℕ, (n : R) = 0 → n = 0) :
    CharZero R :=
  ⟨@fun m n h => by
    induction m generalizing n with
    | zero => rw [H n]; rw [← h, Nat.cast_zero]
    | succ m ih =>
      cases n
      · apply H; rw [h, Nat.cast_zero]
      · simp only [Nat.cast_succ, add_right_cancel_iff] at h; rwa [ih]⟩
Characteristic Zero Criterion for Additive Groups with One
Informal description
Let $R$ be an additive group with one. If for every natural number $n$, the condition $(n : R) = 0$ implies $n = 0$, then $R$ has characteristic zero.
Nat.cast_injective theorem
: Function.Injective (Nat.cast : ℕ → R)
Full source 
theorem cast_injective : Function.Injective (Nat.cast : ℕ → R) :=
  CharZero.cast_injective
Injectivity of Natural Number Cast in Characteristic Zero Monoids
Informal description
The canonical map from the natural numbers $\mathbb{N}$ to an additive monoid with one $R$ of characteristic zero is injective. That is, for any natural numbers $m$ and $n$, if $m$ and $n$ have the same image in $R$, then $m = n$.
Nat.cast_inj theorem
{m n : ℕ} : (m : R) = n ↔ m = n
Full source 
@[simp, norm_cast]
theorem cast_inj {m n : ℕ} : (m : R) = n ↔ m = n :=
  cast_injective.eq_iff
Injectivity of Natural Number Cast in Characteristic Zero Monoids
Informal description
For any natural numbers $m$ and $n$ and any additive monoid with one $R$ of characteristic zero, the canonical images of $m$ and $n$ in $R$ are equal if and only if $m = n$ in $\mathbb{N}$. That is, $(m : R) = (n : R) \leftrightarrow m = n$.
Nat.cast_eq_zero theorem
{n : ℕ} : (n : R) = 0 ↔ n = 0
Full source 
@[simp, norm_cast]
theorem cast_eq_zero {n : ℕ} : (n : R) = 0 ↔ n = 0 := by rw [← cast_zero, cast_inj]
Characterization of Zero Image in Characteristic Zero Monoids
Informal description
For any natural number $n$ and any additive monoid with one $R$ of characteristic zero, the canonical image of $n$ in $R$ is equal to zero if and only if $n = 0$ in $\mathbb{N}$. That is, $(n : R) = 0 \leftrightarrow n = 0$.
Nat.cast_ne_zero theorem
{n : ℕ} : (n : R) ≠ 0 ↔ n ≠ 0
Full source 
@[norm_cast]
theorem cast_ne_zero {n : ℕ} : (n : R) ≠ 0(n : R) ≠ 0 ↔ n ≠ 0 :=
  not_congr cast_eq_zero
Nonzero Characterization in Characteristic Zero Monoids
Informal description
For any natural number $n$ and any additive monoid with one $R$ of characteristic zero, the canonical image of $n$ in $R$ is nonzero if and only if $n$ is nonzero in $\mathbb{N}$. That is, $(n : R) \neq 0 \leftrightarrow n \neq 0$.
Nat.cast_add_one_ne_zero theorem
(n : ℕ) : (n + 1 : R) ≠ 0
Full source 
theorem cast_add_one_ne_zero (n : ℕ) : (n + 1 : R) ≠ 0 :=
  mod_cast n.succ_ne_zero
Nonzero Image of Successor in Characteristic Zero Monoid
Informal description
For any natural number $n$, the image of $n + 1$ in a characteristic zero additive monoid with one $R$ is nonzero, i.e., $(n + 1 : R) \neq 0$.
Nat.cast_eq_one theorem
{n : ℕ} : (n : R) = 1 ↔ n = 1
Full source 
@[simp, norm_cast]
theorem cast_eq_one {n : ℕ} : (n : R) = 1 ↔ n = 1 := by rw [← cast_one, cast_inj]
Characterization of One in Characteristic Zero Monoids
Informal description
For any natural number $n$ and any additive monoid with one $R$ of characteristic zero, the canonical image of $n$ in $R$ is equal to $1$ if and only if $n = 1$ in $\mathbb{N}$. That is, $(n : R) = 1 \leftrightarrow n = 1$.
Nat.cast_ne_one theorem
{n : ℕ} : (n : R) ≠ 1 ↔ n ≠ 1
Full source 
@[norm_cast]
theorem cast_ne_one {n : ℕ} : (n : R) ≠ 1(n : R) ≠ 1 ↔ n ≠ 1 :=
  cast_eq_one.not
Non-One Characterization in Characteristic Zero Monoids: $(n : R) \neq 1 \leftrightarrow n \neq 1$
Informal description
For any natural number $n$ and any additive monoid with one $R$ of characteristic zero, the canonical image of $n$ in $R$ is not equal to $1$ if and only if $n \neq 1$ in $\mathbb{N}$. That is, $(n : R) \neq 1 \leftrightarrow n \neq 1$.
OfNat.ofNat_ne_zero theorem
(n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R) ≠ 0
Full source 
@[simp] lemma ofNat_ne_zero (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R) ≠ 0 :=
  Nat.cast_ne_zero.2 (NeZero.ne n)
Nonzero Property of Natural Numbers $\geq 2$ in Characteristic Zero Monoids
Informal description
For any natural number $n \geq 2$ and any additive monoid with one $R$ of characteristic zero, the canonical image of $n$ in $R$ is nonzero, i.e., $(n : R) \neq 0$.
OfNat.zero_ne_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : 0 ≠ (ofNat(n) : R)
Full source 
@[simp] lemma zero_ne_ofNat (n : ℕ) [n.AtLeastTwo] : 0 ≠ (ofNat(n) : R) :=
  (ofNat_ne_zero n).symm
Nonzero Property of Canonical Images in Characteristic Zero Monoids: $0 \neq (n : R)$ for $n \geq 2$
Informal description
For any natural number $n \geq 2$ and any additive monoid with one $R$ of characteristic zero, the zero element of $R$ is not equal to the canonical image of $n$ in $R$, i.e., $0 \neq (n : R)$.
OfNat.ofNat_ne_one theorem
(n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R) ≠ 1
Full source 
@[simp] lemma ofNat_ne_one (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R) ≠ 1 :=
  Nat.cast_ne_one.2 (Nat.AtLeastTwo.ne_one)
Non-Identity of Canonical Images for Numbers ≥ 2 in Characteristic Zero Monoids
Informal description
For any natural number $n \geq 2$ and any additive monoid with one $R$ of characteristic zero, the canonical image of $n$ in $R$ is not equal to $1$. That is, $(n : R) \neq 1$.
OfNat.one_ne_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : (1 : R) ≠ ofNat(n)
Full source 
@[simp] lemma one_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (1 : R) ≠ ofNat(n) :=
  (ofNat_ne_one n).symm
Multiplicative Identity Distinct from Canonical Images of Numbers ≥ 2 in Characteristic Zero Monoids
Informal description
For any natural number $n \geq 2$ and any additive monoid with one $R$ of characteristic zero, the multiplicative identity $1$ in $R$ is not equal to the canonical image of $n$ in $R$. That is, $1 \neq (n : R)$.
OfNat.ofNat_eq_ofNat theorem
{m n : ℕ} [m.AtLeastTwo] [n.AtLeastTwo] : (ofNat(m) : R) = ofNat(n) ↔ (ofNat m : ℕ) = ofNat n
Full source 
@[simp] lemma ofNat_eq_ofNat {m n : ℕ} [m.AtLeastTwo] [n.AtLeastTwo] :
    (ofNat(m) : R) = ofNat(n) ↔ (ofNat m : ℕ) = ofNat n :=
  Nat.cast_inj
Equality of Canonical Images in Characteristic Zero Monoids for Numbers ≥ 2
Informal description
For any natural numbers $m$ and $n$ (both at least 2) and any additive monoid with one $R$ of characteristic zero, the canonical images of $m$ and $n$ in $R$ are equal if and only if $m = n$ in $\mathbb{N}$. That is, $(m : R) = (n : R) \leftrightarrow m = n$.
NeZero.charZero instance
{M} {n : ℕ} [NeZero n] [AddMonoidWithOne M] [CharZero M] : NeZero (n : M)
Full source 
instance charZero {M} {n : ℕ} [NeZero n] [AddMonoidWithOne M] [CharZero M] : NeZero (n : M) :=
  ⟨Nat.cast_ne_zero.mpr out⟩
Nonzero Natural Numbers Remain Nonzero in Characteristic Zero Monoids
Informal description
For any additive monoid with one $M$ of characteristic zero and any nonzero natural number $n$, the canonical image of $n$ in $M$ is also nonzero.
NeZero.charZero_one instance
{M} [AddMonoidWithOne M] [CharZero M] : NeZero (1 : M)
Full source 
instance charZero_one {M} [AddMonoidWithOne M] [CharZero M] : NeZero (1 : M) where
  out := by
    rw [← Nat.cast_one, Nat.cast_ne_zero]
    trivial
Nonzero Image of One in Characteristic Zero Monoids
Informal description
For any additive monoid with one $M$ of characteristic zero, the canonical image of $1$ in $M$ is nonzero.
NeZero.charZero_ofNat instance
{M} {n : ℕ} [n.AtLeastTwo] [AddMonoidWithOne M] [CharZero M] : NeZero (OfNat.ofNat n : M)
Full source 
instance charZero_ofNat {M} {n : ℕ} [n.AtLeastTwo] [AddMonoidWithOne M] [CharZero M] :
    NeZero (OfNat.ofNat n : M) :=
  ⟨OfNat.ofNat_ne_zero n⟩
Nonzero Images of Natural Numbers $\geq 2$ in Characteristic Zero Monoids
Informal description
For any additive monoid with one $M$ of characteristic zero and any natural number $n \geq 2$, the canonical image of $n$ in $M$ is nonzero.