Mathlib.Algebra.Ring.CharZero

Nat.castEmbedding definition

: ℕ ↪ R

Full source

/-- `Nat.cast` as an embedding into monoids of characteristic `0`. -/
@[simps]
def Nat.castEmbedding : ℕℕ ↪ R := ⟨Nat.cast, cast_injective⟩

Natural number embedding into characteristic zero monoids

Informal description

The embedding of natural numbers into a monoid $ R $ of characteristic zero, given by the canonical injection $ \mathbb{N} \to R $ that maps each natural number $ n $ to its corresponding element in $ R $. This embedding is injective, meaning distinct natural numbers are mapped to distinct elements in $ R $.

CharZero.NeZero.two instance

: NeZero (2 : R)

Full source

instance CharZero.NeZero.two : NeZero (2 : R) where
  out := by rw [← Nat.cast_two, Nat.cast_ne_zero]; decide

Nonzero Property of Two in Characteristic Zero Monoids

Informal description

For any additive monoid with one $R$ of characteristic zero, the element $2$ in $R$ is nonzero.

Function.support_natCast theorem

(hn : n ≠ 0) : support (n : α → R) = univ

Full source

lemma support_natCast (hn : n ≠ 0) : support (n : α → R) = univ :=
  support_const <| Nat.cast_ne_zero.2 hn

Support of Nonzero Constant Function in Characteristic Zero Monoids is Universal Set

Informal description

For any natural number $n \neq 0$ and any function $f : \alpha \to R$ where $R$ is an additive monoid with one of characteristic zero, the support of the constant function $n$ (i.e., the set of points where $n \neq 0$) is equal to the universal set $\alpha$. In other words, $\{x \in \alpha \mid (n : R) \neq 0\} = \alpha$.

Function.mulSupport_natCast theorem

(hn : n ≠ 1) : mulSupport (n : α → R) = univ

Full source

lemma mulSupport_natCast (hn : n ≠ 1) : mulSupport (n : α → R) = univ :=
  mulSupport_const <| Nat.cast_ne_one.2 hn

Multiplicative Support of Non-One Constant Function in Characteristic Zero

Informal description

For any natural number $n \neq 1$ and any additive monoid with one $R$ of characteristic zero, the multiplicative support of the constant function $n : \alpha \to R$ is the entire domain $\alpha$. That is, $\operatorname{mulSupport} (n) = \alpha$.

RingHom.charZero theorem

(ϕ : R →+* S) [CharZero S] : CharZero R

Full source

lemma charZero (ϕ : R →+* S) [CharZero S] : CharZero R where
  cast_injective a b h := CharZero.cast_injective (R := S) <| by
    rw [← map_natCast ϕ, ← map_natCast ϕ, h]

Ring Homomorphism Preserves Characteristic Zero

Informal description

Let $R$ and $S$ be non-associative semirings, and let $\phi \colon R \to S$ be a ring homomorphism. If $S$ has characteristic zero, then $R$ also has characteristic zero.

RingHom.charZero_iff theorem

{ϕ : R →+* S} (hϕ : Injective ϕ) : CharZero R ↔ CharZero S

Full source

lemma charZero_iff {ϕ : R →+* S} (hϕ : Injective ϕ) : CharZeroCharZero R ↔ CharZero S :=
  ⟨fun hR =>
    ⟨by intro a b h; rwa [← @Nat.cast_inj R, ← hϕ.eq_iff, map_natCast ϕ, map_natCast ϕ]⟩,
    fun _ => ϕ.charZero⟩

Characterization of Characteristic Zero via Injective Ring Homomorphisms

Informal description

Let $R$ and $S$ be non-associative semirings, and let $\phi \colon R \to S$ be an injective ring homomorphism. Then $R$ has characteristic zero if and only if $S$ has characteristic zero.

RingHom.injective_nat theorem

(f : ℕ →+* R) [CharZero R] : Injective f

Full source

lemma injective_nat (f : ℕℕ →+* R) [CharZero R] : Injective f :=
  Subsingleton.elim (Nat.castRingHom _) f ▸ Nat.cast_injective

Injectivity of Natural Number Ring Homomorphisms into Characteristic Zero Rings

Informal description

For any ring homomorphism $f \colon \mathbb{N} \to R$ where $R$ is a ring of characteristic zero, the homomorphism $f$ is injective.

add_self_eq_zero theorem

{a : R} : a + a = 0 ↔ a = 0

Full source

@[simp]
theorem add_self_eq_zero {a : R} : a + a = 0 ↔ a = 0 := by
  simp only [(two_mul a).symm, mul_eq_zero, two_ne_zero, false_or]

Characterization of Additive Self-Inverse Elements in Characteristic Zero Rings: $a + a = 0 \leftrightarrow a = 0$

Informal description

For any element $a$ in a ring $R$ of characteristic zero, the equation $a + a = 0$ holds if and only if $a = 0$.

Nat.cast_pow_eq_one theorem

{a : ℕ} (hn : n ≠ 0) : (a : R) ^ n = 1 ↔ a = 1

Full source

@[simp] lemma Nat.cast_pow_eq_one {a : ℕ} (hn : n ≠ 0) : (a : R) ^ n = 1 ↔ a = 1 := by
  simp [← cast_pow, cast_eq_one, hn]

Characterization of Natural Number Powers Equal to One in Characteristic Zero Semirings: $(a : R)^n = 1 \leftrightarrow a = 1$ for $n \neq 0$

Informal description

Let $R$ be a semiring of characteristic zero. For any natural number $a$ and any nonzero natural number $n$, the cast of $a$ to $R$ satisfies $(a : R)^n = 1$ if and only if $a = 1$.

CharZero.neg_eq_self_iff theorem

{a : R} : -a = a ↔ a = 0

Full source

@[scoped simp] theorem CharZero.neg_eq_self_iff {a : R} : -a = a ↔ a = 0 :=
  neg_eq_iff_add_eq_zero.trans add_self_eq_zero

Negation Equals Self iff Zero in Characteristic Zero Rings: $-a = a \leftrightarrow a = 0$

Informal description

For any element $a$ in a ring $R$ of characteristic zero, the equation $-a = a$ holds if and only if $a = 0$.

nat_mul_inj theorem

{n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) : n = 0 ∨ a = b

Full source

theorem nat_mul_inj {n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) : n = 0 ∨ a = b := by
  rw [← sub_eq_zero, ← mul_sub, mul_eq_zero, sub_eq_zero] at h
  exact mod_cast h

Injectivity of Natural Multiplication in Characteristic Zero Rings: $n \cdot a = n \cdot b \Rightarrow n = 0 \lor a = b$

Informal description

For any natural number $n$ and elements $a, b$ in a characteristic zero ring $R$, if $n \cdot a = n \cdot b$ (where $n$ is interpreted in $R$ via the canonical map), then either $n = 0$ or $a = b$.

nat_mul_inj' theorem

{n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) (w : n ≠ 0) : a = b

Full source

theorem nat_mul_inj' {n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) (w : n ≠ 0) : a = b := by
  simpa [w] using nat_mul_inj h

Cancellation of Natural Multiplication in Characteristic Zero Rings: $n \cdot a = n \cdot b \Rightarrow a = b$ for $n \neq 0$

Informal description

For any natural number $n \neq 0$ and elements $a, b$ in a characteristic zero ring $R$, if $n \cdot a = n \cdot b$ (where $n$ is interpreted in $R$ via the canonical map), then $a = b$.

units_ne_neg_self theorem

(u : Rˣ) : u ≠ -u

Full source

@[simp]
theorem units_ne_neg_self (u : Rˣ) : u ≠ -u := by
  simp_rw [ne_eq, Units.ext_iff, Units.val_neg, eq_neg_iff_add_eq_zero, ← two_mul,
    Units.mul_left_eq_zero, two_ne_zero, not_false_iff]

Units are not equal to their negatives in characteristic zero rings

Informal description

For any unit $u$ in the group of units $R^\times$ of a ring $R$ of characteristic zero, $u$ is not equal to $-u$.

neg_units_ne_self theorem

(u : Rˣ) : -u ≠ u

Full source

@[simp]
theorem neg_units_ne_self (u : Rˣ) : -u ≠ u := (units_ne_neg_self u).symm

Negation of Units is Not Equal to Original in Characteristic Zero Rings

Informal description

For any unit $u$ in the group of units $R^\times$ of a ring $R$ of characteristic zero, $-u$ is not equal to $u$.