Mathlib.Algebra.Ring.Hom.Basic

Module docstring

{"# Additional lemmas about homomorphisms of semirings and rings

These lemmas have been banished here to avoid unnecessary imports in Mathlib.Algebra.Hom.Ring.Defs.

They could be moved to more natural homes. "}

RingHom.codomain_trivial_iff_range_eq_singleton_zero theorem

: (0 : β) = 1 ↔ Set.range f = {0}

Full source

/-- `f : α →+* β` has a trivial codomain iff its range is `{0}`. -/
theorem codomain_trivial_iff_range_eq_singleton_zero : (0 : β) = 1 ↔ Set.range f = {0} :=
  f.codomain_trivial_iff_range_trivial.trans
    ⟨fun h =>
      Set.ext fun y => ⟨fun ⟨x, hx⟩ => by simp [← hx, h x], fun hy => ⟨0, by simpa using hy.symm⟩⟩,
      fun h x => Set.mem_singleton_iff.mp (h ▸ Set.mem_range_self x)⟩

Trivial Codomain Characterization for Ring Homomorphisms via Range

Informal description

For a ring homomorphism $f : \alpha \to \beta$, the codomain $\beta$ is trivial (i.e., $0 = 1$ in $\beta$) if and only if the range of $f$ is the singleton set $\{0\}$.

RingHom.map_dvd theorem

(f : α →+* β) {a b : α} : a ∣ b → f a ∣ f b

Full source

protected theorem map_dvd (f : α →+* β) {a b : α} : a ∣ b → f a ∣ f b :=
  map_dvd f

Divisibility Preservation Under Ring Homomorphisms

Informal description

Let $f \colon \alpha \to \beta$ be a ring homomorphism between semirings $\alpha$ and $\beta$. For any elements $a, b \in \alpha$, if $a$ divides $b$ in $\alpha$, then $f(a)$ divides $f(b)$ in $\beta$.

Function.Injective.isDomain theorem

 [Semiring α] [IsDomain α] [Semiring β] {F} [FunLike F β α] [MonoidWithZeroHomClass F β α] (f : F) (hf : Injective f) :
  IsDomain β

Full source

/-- Pullback `IsDomain` instance along an injective function. -/
protected theorem Function.Injective.isDomain [Semiring α] [IsDomain α] [Semiring β] {F}
    [FunLike F β α] [MonoidWithZeroHomClass F β α] (f : F) (hf : Injective f) : IsDomain β where
  __ := domain_nontrivial f (map_zero _) (map_one _)
  __ := hf.isCancelMulZero f (map_zero _) (map_mul _)

Injective Homomorphisms Preserve Domain Structure

Informal description

Let $\alpha$ and $\beta$ be semirings, with $\alpha$ being a domain (i.e., a nontrivial semiring where multiplication is cancellative for nonzero elements). Let $F$ be a type of homomorphisms from $\beta$ to $\alpha$ that preserve the multiplicative structure with zero (i.e., $F$ is a `MonoidWithZeroHomClass`). Given an injective homomorphism $f \colon \beta \to \alpha$ in $F$, then $\beta$ is also a domain.