algebra.hom.ring

Homomorphisms of semirings and rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines bundled homomorphisms of (non-unital) semirings and rings. As with monoid and groups, we use the same structure `ring_hom a β`, a.k.a. `α →+* β`, for both types of homomorphisms.

The unbundled homomorphisms are defined in `deprecated.ring`. They are deprecated and the plan is to slowly remove them from mathlib.

Main definitions #

• `non_unital_ring_hom`: Non-unital (semi)ring homomorphisms. Additive monoid homomorphism which preserve multiplication.
• `ring_hom`: (Semi)ring homomorphisms. Monoid homomorphisms which are also additive monoid homomorphism.

Notations #

• `→ₙ+*`: Non-unital (semi)ring homs
• `→+*`: (Semi)ring homs

Implementation notes #

• There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

• There is no `semiring_hom` -- the idea is that `ring_hom` is used. The constructor for a `ring_hom` between semirings needs a proof of `map_zero`, `map_one` and `map_add` as well as `map_mul`; a separate constructor `ring_hom.mk'` will construct ring homs between rings from monoid homs given only a proof that addition is preserved.

Tags #

`ring_hom`, `semiring_hom`

structure non_unital_ring_hom (α : Type u_5) (β : Type u_6)  :
Type (max u_5 u_6)

Bundled non-unital semiring homomorphisms `α →ₙ+* β`; use this for bundled non-unital ring homomorphisms too.

When possible, instead of parametrizing results over `(f : α →ₙ+* β)`, you should parametrize over `(F : Type*) [non_unital_ring_hom_class F α β] (f : F)`.

When you extend this structure, make sure to extend `non_unital_ring_hom_class`.

Instances for `non_unital_ring_hom`
def non_unital_ring_hom.to_mul_hom {α : Type u_5} {β : Type u_6} (self : α →ₙ+* β) :
α →ₙ* β

Reinterpret a non-unital ring homomorphism `f : α →ₙ+* β` as a semigroup homomorphism `α →ₙ* β`. The `simp`-normal form is `(f : α →ₙ* β)`.

def non_unital_ring_hom.to_add_monoid_hom {α : Type u_5} {β : Type u_6} (self : α →ₙ+* β) :
α →+ β

Reinterpret a non-unital ring homomorphism `f : α →ₙ+* β` as an additive monoid homomorphism `α →+ β`. The `simp`-normal form is `(f : α →+ β)`.

@[instance]
def non_unital_ring_hom_class.to_add_monoid_hom_class (F : Type u_5) (α : out_param (Type u_6)) (β : out_param (Type u_7)) [self : β] :
β
@[instance]
def non_unital_ring_hom_class.to_mul_hom_class (F : Type u_5) (α : out_param (Type u_6)) (β : out_param (Type u_7)) [self : β] :
β
@[class]
structure non_unital_ring_hom_class (F : Type u_5) (α : out_param (Type u_6)) (β : out_param (Type u_7))  :
Type (max u_5 u_6 u_7)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_mul : (f : F) (x y : α), f (x * y) = f x * f y
• map_add : (f : F) (x y : α), f (x + y) = f x + f y
• map_zero : (f : F), f 0 = 0

`non_unital_ring_hom_class F α β` states that `F` is a type of non-unital (semi)ring homomorphisms. You should extend this class when you extend `non_unital_ring_hom`.

Instances of this typeclass
Instances of other typeclasses for `non_unital_ring_hom_class`
• non_unital_ring_hom_class.has_sizeof_inst
@[protected, instance]
def non_unital_ring_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] :
→ₙ+* β)
Equations

Throughout this section, some `semiring` arguments are specified with `{}` instead of `[]`. See note [implicit instance arguments].

@[protected, instance]
def non_unital_ring_hom.non_unital_ring_hom_class {α : Type u_2} {β : Type u_3}  :
α β
Equations
@[protected, instance]
def non_unital_ring_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3}  :
has_coe_to_fun →ₙ+* β) (λ (_x : α →ₙ+* β), α β)

Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun` directly.

Equations
@[simp]
theorem non_unital_ring_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) :
@[simp]
theorem non_unital_ring_hom.coe_mk {α : Type u_2} {β : Type u_3} (f : α β) (h₁ : (x y : α), f (x * y) = f x * f y) (h₂ : f 0 = 0) (h₃ : (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃} = f
@[simp]
theorem non_unital_ring_hom.coe_coe {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F) :
@[simp]
theorem non_unital_ring_hom.coe_to_mul_hom {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) :
@[simp]
theorem non_unital_ring_hom.coe_mul_hom_mk {α : Type u_2} {β : Type u_3} (f : α β) (h₁ : (x y : α), f (x * y) = f x * f y) (h₂ : f 0 = 0) (h₃ : (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃} = {to_fun := f, map_mul' := h₁}
@[simp]
theorem non_unital_ring_hom.coe_to_add_monoid_hom {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) :
@[simp]
theorem non_unital_ring_hom.coe_add_monoid_hom_mk {α : Type u_2} {β : Type u_3} (f : α β) (h₁ : (x y : α), f (x * y) = f x * f y) (h₂ : f 0 = 0) (h₃ : (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃} = {to_fun := f, map_zero' := h₂, map_add' := h₃}
@[protected]
def non_unital_ring_hom.copy {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) (f' : α β) (h : f' = f) :
α →ₙ+* β

Copy of a `ring_hom` with a new `to_fun` equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem non_unital_ring_hom.coe_copy {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem non_unital_ring_hom.copy_eq {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[ext]
theorem non_unital_ring_hom.ext {α : Type u_2} {β : Type u_3} ⦃f g : α →ₙ+* β⦄ :
( (x : α), f x = g x) f = g
theorem non_unital_ring_hom.ext_iff {α : Type u_2} {β : Type u_3} {f g : α →ₙ+* β} :
f = g (x : α), f x = g x
@[simp]
theorem non_unital_ring_hom.mk_coe {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) (h₁ : (x y : α), f (x * y) = f x * f y) (h₂ : f 0 = 0) (h₃ : (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃} = f
theorem non_unital_ring_hom.coe_mul_hom_injective {α : Type u_2} {β : Type u_3}  :
@[protected]
def non_unital_ring_hom.id (α : Type u_1)  :
α →ₙ+* α

The identity non-unital ring homomorphism from a non-unital semiring to itself.

Equations
@[protected, instance]
def non_unital_ring_hom.has_zero {α : Type u_2} {β : Type u_3}  :
Equations
@[protected, instance]
def non_unital_ring_hom.inhabited {α : Type u_2} {β : Type u_3}  :
Equations
@[simp]
theorem non_unital_ring_hom.coe_zero {α : Type u_2} {β : Type u_3}  :
0 = 0
@[simp]
theorem non_unital_ring_hom.zero_apply {α : Type u_2} {β : Type u_3} (x : α) :
0 x = 0
@[simp]
theorem non_unital_ring_hom.id_apply {α : Type u_2} (x : α) :
= x
@[simp]
@[simp]
theorem non_unital_ring_hom.coe_mul_hom_id {α : Type u_2}  :
def non_unital_ring_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β →ₙ+* γ) (f : α →ₙ+* β) :
α →ₙ+* γ

Composition of non-unital ring homomorphisms is a non-unital ring homomorphism.

Equations
theorem non_unital_ring_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_1} (f : α →ₙ+* β) (g : β →ₙ+* γ) (h : γ →ₙ+* δ) :
(h.comp g).comp f = h.comp (g.comp f)

Composition of non-unital ring homomorphisms is associative.

@[simp]
theorem non_unital_ring_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β →ₙ+* γ) (f : α →ₙ+* β) :
(g.comp f) = g f
@[simp]
theorem non_unital_ring_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α) :
(g.comp f) x = g (f x)
@[simp]
theorem non_unital_ring_hom.coe_comp_add_monoid_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β →ₙ+* γ) (f : α →ₙ+* β) :
(g.comp f) = g.comp f
@[simp]
theorem non_unital_ring_hom.coe_comp_mul_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β →ₙ+* γ) (f : α →ₙ+* β) :
(g.comp f) = g.comp f
@[simp]
theorem non_unital_ring_hom.comp_zero {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β →ₙ+* γ) :
g.comp 0 = 0
@[simp]
theorem non_unital_ring_hom.zero_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (f : α →ₙ+* β) :
0.comp f = 0
@[simp]
theorem non_unital_ring_hom.comp_id {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) :
= f
@[simp]
theorem non_unital_ring_hom.id_comp {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) :
= f
theorem non_unital_ring_hom.one_def {α : Type u_2}  :
@[simp]
theorem non_unital_ring_hom.coe_one {α : Type u_2}  :
theorem non_unital_ring_hom.mul_def {α : Type u_2} (f g : α →ₙ+* α) :
f * g = f.comp g
@[simp]
theorem non_unital_ring_hom.coe_mul {α : Type u_2} (f g : α →ₙ+* α) :
(f * g) = f g
theorem non_unital_ring_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} {g₁ g₂ : β →ₙ+* γ} {f : α →ₙ+* β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem non_unital_ring_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} {g : β →ₙ+* γ} {f₁ f₂ : α →ₙ+* β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
def ring_hom.to_add_monoid_hom {α : Type u_5} {β : Type u_6} (self : α →+* β) :
α →+ β

Reinterpret a ring homomorphism `f : α →+* β` as an additive monoid homomorphism `α →+ β`. The `simp`-normal form is `(f : α →+ β)`.

def ring_hom.to_monoid_hom {α : Type u_5} {β : Type u_6} (self : α →+* β) :
α →* β

Reinterpret a ring homomorphism `f : α →+* β` as a monoid homomorphism `α →* β`. The `simp`-normal form is `(f : α →* β)`.

def ring_hom.to_non_unital_ring_hom {α : Type u_5} {β : Type u_6} (self : α →+* β) :
α →ₙ+* β

Reinterpret a ring homomorphism `f : α →+* β` as a non-unital ring homomorphism `α →ₙ+* β`. The `simp`-normal form is `(f : α →ₙ+* β)`.

structure ring_hom (α : Type u_5) (β : Type u_6)  :
Type (max u_5 u_6)

Bundled semiring homomorphisms; use this for bundled ring homomorphisms too.

This extends from both `monoid_hom` and `monoid_with_zero_hom` in order to put the fields in a sensible order, even though `monoid_with_zero_hom` already extends `monoid_hom`.

Instances for `ring_hom`
def ring_hom.to_monoid_with_zero_hom {α : Type u_5} {β : Type u_6} (self : α →+* β) :
α →*₀ β

Reinterpret a ring homomorphism `f : α →+* β` as a monoid with zero homomorphism `α →*₀ β`. The `simp`-normal form is `(f : α →*₀ β)`.

@[instance]
def ring_hom_class.to_monoid_with_zero_hom_class (F : Type u_5) (α : out_param (Type u_6)) (β : out_param (Type u_7)) [self : β] :
@[instance]
def ring_hom_class.to_monoid_hom_class (F : Type u_5) (α : out_param (Type u_6)) (β : out_param (Type u_7)) [self : β] :
β
@[class]
structure ring_hom_class (F : Type u_5) (α : out_param (Type u_6)) (β : out_param (Type u_7))  :
Type (max u_5 u_6 u_7)
• coe : F Π (a : α), (λ (_x : α), β) a
• coe_injective' :
• map_mul : (f : F) (x y : α), f (x * y) = f x * f y
• map_one : (f : F), f 1 = 1
• map_add : (f : F) (x y : α), f (x + y) = f x + f y
• map_zero : (f : F), f 0 = 0

`ring_hom_class F α β` states that `F` is a type of (semi)ring homomorphisms. You should extend this class when you extend `ring_hom`.

This extends from both `monoid_hom_class` and `monoid_with_zero_hom_class` in order to put the fields in a sensible order, even though `monoid_with_zero_hom_class` already extends `monoid_hom_class`.

Instances of this typeclass
Instances of other typeclasses for `ring_hom_class`
• ring_hom_class.has_sizeof_inst
@[instance]
def ring_hom_class.to_add_monoid_hom_class (F : Type u_5) (α : out_param (Type u_6)) (β : out_param (Type u_7)) [self : β] :
β
@[simp]
theorem map_bit1 {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] (f : F) (a : α) :
f (bit1 a) = bit1 (f a)

Ring homomorphisms preserve `bit1`.

@[protected, instance]
def ring_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] :
→+* β)
Equations
@[protected, instance]
def ring_hom_class.to_non_unital_ring_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] :
Equations

Throughout this section, some `semiring` arguments are specified with `{}` instead of `[]`. See note [implicit instance arguments].

@[protected, instance]
def ring_hom.ring_hom_class {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
ring_hom_class →+* β) α β
Equations
@[protected, instance]
def ring_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
has_coe_to_fun →+* β) (λ (_x : α →+* β), α β)

Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun` directly.

Equations
@[simp]
theorem ring_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.coe_mk {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α β) (h₁ : f 1 = 1) (h₂ : (x y : α), f (x * y) = f x * f y) (h₃ : f 0 = 0) (h₄ : (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄} = f
@[simp]
theorem ring_hom.coe_coe {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} {F : Type u_1} [ β] (f : F) :
@[protected, instance]
def ring_hom.has_coe_monoid_hom {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
has_coe →+* β) →* β)
Equations
@[simp, norm_cast]
theorem ring_hom.coe_monoid_hom {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.to_monoid_hom_eq_coe {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.to_monoid_with_zero_hom_eq_coe {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.coe_monoid_hom_mk {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α β) (h₁ : f 1 = 1) (h₂ : (x y : α), f (x * y) = f x * f y) (h₃ : f 0 = 0) (h₄ : (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄} = {to_fun := f, map_one' := h₁, map_mul' := h₂}
@[simp, norm_cast]
theorem ring_hom.coe_add_monoid_hom {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.to_add_monoid_hom_eq_coe {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.coe_add_monoid_hom_mk {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α β) (h₁ : f 1 = 1) (h₂ : (x y : α), f (x * y) = f x * f y) (h₃ : f 0 = 0) (h₄ : (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄} = {to_fun := f, map_zero' := h₃, map_add' := h₄}
def ring_hom.copy {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (f' : α β) (h : f' = f) :
α →+* β

Copy of a `ring_hom` with a new `to_fun` equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem ring_hom.coe_copy {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem ring_hom.copy_eq {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (f' : α β) (h : f' = f) :
f.copy f' h = f
theorem ring_hom.congr_fun {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} {f g : α →+* β} (h : f = g) (x : α) :
f x = g x
theorem ring_hom.congr_arg {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) {x y : α} (h : x = y) :
f x = f y
theorem ring_hom.coe_inj {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} ⦃f g : α →+* β⦄ (h : f = g) :
f = g
@[ext]
theorem ring_hom.ext {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} ⦃f g : α →+* β⦄ :
( (x : α), f x = g x) f = g
theorem ring_hom.ext_iff {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} {f g : α →+* β} :
f = g (x : α), f x = g x
@[simp]
theorem ring_hom.mk_coe {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (h₁ : f 1 = 1) (h₂ : (x y : α), f (x * y) = f x * f y) (h₃ : f 0 = 0) (h₄ : (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄} = f
theorem ring_hom.coe_add_monoid_hom_injective {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
theorem ring_hom.coe_monoid_hom_injective {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
@[protected]
theorem ring_hom.map_zero {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
f 0 = 0

Ring homomorphisms map zero to zero.

@[protected]
theorem ring_hom.map_one {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
f 1 = 1

Ring homomorphisms map one to one.

@[protected]
theorem ring_hom.map_add {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (a b : α) :
f (a + b) = f a + f b

@[protected]
theorem ring_hom.map_mul {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (a b : α) :
f (a * b) = f a * f b

Ring homomorphisms preserve multiplication.

@[protected]
theorem ring_hom.map_bit0 {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (a : α) :
f (bit0 a) = bit0 (f a)

Ring homomorphisms preserve `bit0`.

@[protected]
theorem ring_hom.map_bit1 {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (a : α) :
f (bit1 a) = bit1 (f a)

Ring homomorphisms preserve `bit1`.

@[simp]
theorem ring_hom.map_ite_zero_one {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} {F : Type u_1} [ β] (f : F) (p : Prop) [decidable p] :
f (ite p 0 1) = ite p 0 1
@[simp]
theorem ring_hom.map_ite_one_zero {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} {F : Type u_1} [ β] (f : F) (p : Prop) [decidable p] :
f (ite p 1 0) = ite p 1 0
theorem ring_hom.codomain_trivial_iff_map_one_eq_zero {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
0 = 1 f 1 = 0

`f : α →+* β` has a trivial codomain iff `f 1 = 0`.

theorem ring_hom.codomain_trivial_iff_range_trivial {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
0 = 1 (x : α), f x = 0

`f : α →+* β` has a trivial codomain iff it has a trivial range.

theorem ring_hom.codomain_trivial_iff_range_eq_singleton_zero {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
0 = 1 = {0}

`f : α →+* β` has a trivial codomain iff its range is `{0}`.

theorem ring_hom.map_one_ne_zero {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) [nontrivial β] :
f 1 0

`f : α →+* β` doesn't map `1` to `0` if `β` is nontrivial

theorem ring_hom.domain_nontrivial {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) [nontrivial β] :

If there is a homomorphism `f : α →+* β` and `β` is nontrivial, then `α` is nontrivial.

theorem ring_hom.codomain_trivial {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) [h : subsingleton α] :
@[protected]
theorem ring_hom.map_neg {α : Type u_2} {β : Type u_3} (f : α →+* β) (x : α) :
f (-x) = -f x

@[protected]
theorem ring_hom.map_sub {α : Type u_2} {β : Type u_3} (f : α →+* β) (x y : α) :
f (x - y) = f x - f y

Ring homomorphisms preserve subtraction.

def ring_hom.mk' {α : Type u_2} {β : Type u_3} (f : α →* β) (map_add : (a b : α), f (a + b) = f a + f b) :
α →+* β

Makes a ring homomorphism from a monoid homomorphism of rings which preserves addition.

Equations
theorem ring_hom.is_unit_map {α : Type u_2} {β : Type u_3} [semiring α] [semiring β] (f : α →+* β) {a : α} :
@[protected]
theorem ring_hom.map_dvd {α : Type u_2} {β : Type u_3} [semiring α] [semiring β] (f : α →+* β) {a b : α} :
a b f a f b
def ring_hom.id (α : Type u_1)  :
α →+* α

The identity ring homomorphism from a semiring to itself.

Equations
Instances for `ring_hom.id`
@[protected, instance]
def ring_hom.inhabited {α : Type u_2} [rα : non_assoc_semiring α] :
Equations
@[simp]
theorem ring_hom.id_apply {α : Type u_2} [rα : non_assoc_semiring α] (x : α) :
(ring_hom.id α) x = x
@[simp]
theorem ring_hom.coe_add_monoid_hom_id {α : Type u_2} [rα : non_assoc_semiring α] :
@[simp]
theorem ring_hom.coe_monoid_hom_id {α : Type u_2} [rα : non_assoc_semiring α] :
def ring_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} (g : β →+* γ) (f : α →+* β) :
α →+* γ

Composition of ring homomorphisms is a ring homomorphism.

Equations
Instances for `ring_hom.comp`
theorem ring_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} {δ : Type u_1} {rδ : non_assoc_semiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ) :
(h.comp g).comp f = h.comp (g.comp f)

Composition of semiring homomorphisms is associative.

@[simp]
theorem ring_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} (hnp : β →+* γ) (hmn : α →+* β) :
(hnp.comp hmn) = hnp hmn
theorem ring_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} (hnp : β →+* γ) (hmn : α →+* β) (x : α) :
(hnp.comp hmn) x = hnp (hmn x)
@[simp]
theorem ring_hom.comp_id {α : Type u_2} {β : Type u_3} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] (f : α →+* β) :
f.comp (ring_hom.id α) = f
@[simp]
theorem ring_hom.id_comp {α : Type u_2} {β : Type u_3} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] (f : α →+* β) :
(ring_hom.id β).comp f = f
@[protected, instance]
def ring_hom.monoid {α : Type u_2} [rα : non_assoc_semiring α] :
monoid →+* α)
Equations
theorem ring_hom.one_def {α : Type u_2} [rα : non_assoc_semiring α] :
1 =
theorem ring_hom.mul_def {α : Type u_2} [rα : non_assoc_semiring α] (f g : α →+* α) :
f * g = f.comp g
@[simp]
theorem ring_hom.coe_one {α : Type u_2} [rα : non_assoc_semiring α] :
@[simp]
theorem ring_hom.coe_mul {α : Type u_2} [rα : non_assoc_semiring α] (f g : α →+* α) :
(f * g) = f g
theorem ring_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} {g₁ g₂ : β →+* γ} {f : α →+* β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem ring_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} {g : β →+* γ} {f₁ f₂ : α →+* β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected]
theorem function.injective.is_domain {α : Type u_2} {β : Type u_3} [ring α] [is_domain α] [ring β] (f : β →+* α) (hf : function.injective f) :

Pullback `is_domain` instance along an injective function.

def add_monoid_hom.mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u_2} {β : Type u_3} [comm_ring α] [is_domain α] [comm_ring β] (f : β →+ α) (h : (x : β), f (x * x) = f x * f x) (h_two : 2 0) (h_one : f 1 = 1) :
β →+* α

Make a ring homomorphism from an additive group homomorphism from a commutative ring to an integral domain that commutes with self multiplication, assumes that two is nonzero and `1` is sent to `1`.

Equations
@[simp]
theorem add_monoid_hom.coe_fn_mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u_2} {β : Type u_3} [comm_ring α] [is_domain α] [comm_ring β] (f : β →+ α) (h : (x : β), f (x * x) = f x * f x) (h_two : 2 0) (h_one : f 1 = 1) :
h_two h_one) = f
@[simp]
theorem add_monoid_hom.coe_add_monoid_hom_mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u_2} {β : Type u_3} [comm_ring α] [is_domain α] [comm_ring β] (f : β →+ α) (h : (x : β), f (x * x) = f x * f x) (h_two : 2 0) (h_one : f 1 = 1) :
h_two h_one) = f