mathlib3 documentation

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 #

Notations #

Implementation notes #

Tags #

ring_hom, semiring_hom

structure non_unital_ring_hom (α : Type u_5) (β : Type u_6) [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] :
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

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

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

@[class]
structure non_unital_ring_hom_class (F : Type u_5) (α : out_param (Type u_6)) (β : out_param (Type u_7)) [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] :
Type (max u_5 u_6 u_7)

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]
Equations

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

@[protected, instance]
def non_unital_ring_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_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 non_unital_ring_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} (f : α →ₙ+* β) :
@[simp]
theorem non_unital_ring_hom.coe_mk {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} (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} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} [non_unital_ring_hom_class F α β] (f : F) :
@[simp]
@[simp]
theorem non_unital_ring_hom.coe_mul_hom_mk {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} (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_add_monoid_hom_mk {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} (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} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_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 non_unital_ring_hom.coe_copy {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} (f : α →ₙ+* β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem non_unital_ring_hom.copy_eq {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} (f : α →ₙ+* β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[ext]
theorem non_unital_ring_hom.ext {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} ⦃f g : α →ₙ+* β⦄ :
( (x : α), f x = g x) f = g
theorem non_unital_ring_hom.ext_iff {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} {f g : α →ₙ+* β} :
f = g (x : α), f x = g x
@[simp]
theorem non_unital_ring_hom.mk_coe {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} (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
@[protected]

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

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem non_unital_ring_hom.coe_zero {α : Type u_2} {β : Type u_3} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] :
0 = 0
@[simp]
theorem non_unital_ring_hom.zero_apply {α : Type u_2} {β : Type u_3} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] (x : α) :
0 x = 0
@[simp]
def non_unital_ring_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] {rγ : non_unital_non_assoc_semiring γ} (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} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] {rγ : non_unital_non_assoc_semiring γ} {δ : Type u_1} {rδ : non_unital_non_assoc_semiring δ} (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} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] {rγ : non_unital_non_assoc_semiring γ} (g : β →ₙ+* γ) (f : α →ₙ+* β) :
(g.comp f) = g f
@[simp]
theorem non_unital_ring_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] {rγ : non_unital_non_assoc_semiring γ} (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} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] {rγ : non_unital_non_assoc_semiring γ} (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} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] {rγ : non_unital_non_assoc_semiring γ} (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} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] {rγ : non_unital_non_assoc_semiring γ} (g : β →ₙ+* γ) :
g.comp 0 = 0
@[simp]
theorem non_unital_ring_hom.zero_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] {rγ : non_unital_non_assoc_semiring γ} (f : α →ₙ+* β) :
0.comp f = 0
@[simp]
theorem non_unital_ring_hom.comp_id {α : Type u_2} {β : Type u_3} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] (f : α →ₙ+* β) :
@[simp]
theorem non_unital_ring_hom.id_comp {α : Type u_2} {β : Type u_3} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] (f : α →ₙ+* β) :
@[simp]
theorem non_unital_ring_hom.mul_def {α : Type u_2} [rα : non_unital_non_assoc_semiring α] (f g : α →ₙ+* α) :
f * g = f.comp g
@[simp]
theorem non_unital_ring_hom.coe_mul {α : Type u_2} [rα : non_unital_non_assoc_semiring α] (f g : α →ₙ+* α) :
(f * g) = f g
theorem non_unital_ring_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] {rγ : non_unital_non_assoc_semiring γ} {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} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] {rγ : non_unital_non_assoc_semiring γ} {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} [non_assoc_semiring α] [non_assoc_semiring β] (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} [non_assoc_semiring α] [non_assoc_semiring β] (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} [non_assoc_semiring α] [non_assoc_semiring β] (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) [non_assoc_semiring α] [non_assoc_semiring β] :
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} [non_assoc_semiring α] [non_assoc_semiring β] (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_hom_class (F : Type u_5) (α : out_param (Type u_6)) (β : out_param (Type u_7)) [non_assoc_semiring α] [non_assoc_semiring β] [self : ring_hom_class F α β] :
@[class]
structure ring_hom_class (F : Type u_5) (α : out_param (Type u_6)) (β : out_param (Type u_7)) [non_assoc_semiring α] [non_assoc_semiring β] :
Type (max u_5 u_6 u_7)

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]
@[simp]
theorem map_bit1 {F : Type u_1} {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [non_assoc_semiring β] [ring_hom_class F α β] (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} [non_assoc_semiring α] [non_assoc_semiring β] [ring_hom_class F α β] :
has_coe_t F →+* β)
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} [ring_hom_class F α β] (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
@[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

Ring homomorphisms preserve addition.

@[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} [ring_hom_class F α β] (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} [ring_hom_class F α β] (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 set.range f = {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} [non_assoc_ring α] [non_assoc_ring β] (f : α →+* β) (x : α) :
f (-x) = -f x

Ring homomorphisms preserve additive inverse.

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

Ring homomorphisms preserve subtraction.

def ring_hom.mk' {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [non_assoc_ring β] (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
@[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]
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
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 α] :
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) :
@[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) :