algebra.hom.ring - mathlib3 docs

source

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)

to_fun : α → β
map_mul' : ∀ (x y : α), self.to_fun (x * y) = self.to_fun x * self.to_fun y
map_zero' : self.to_fun 0 = 0
map_add' : ∀ (x y : α), self.to_fun (x + y) = self.to_fun x + self.to_fun y

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

ring_equiv.has_coe_to_non_unital_ring_hom
non_unital_ring_hom.has_sizeof_inst
non_unital_ring_hom.has_coe_t
non_unital_ring_hom.non_unital_ring_hom_class
non_unital_ring_hom.has_coe_to_fun
non_unital_ring_hom.has_zero
non_unital_ring_hom.inhabited
non_unital_ring_hom.monoid_with_zero

source

def non_unital_ring_hom.to_mul_hom {α : Type u_5} {β : Type u_6} [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] (self : α →ₙ+* β) :

α →ₙ* β

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

source

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

α →+ β

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

source

@[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)) [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] [self : non_unital_ring_hom_class F α β] :

add_monoid_hom_class F α β

source

@[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)) [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] [self : non_unital_ring_hom_class F α β] :

mul_hom_class F α β

source

@[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)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective non_unital_ring_hom_class.coe
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

source

@[protected, instance]

def non_unital_ring_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] [non_unital_ring_hom_class F α β] :

has_coe_t F (α →ₙ+* β)

Equations

non_unital_ring_hom.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, map_mul' := _, map_zero' := _, map_add' := _}}

source

@[protected, instance]

def non_unital_ring_hom.non_unital_ring_hom_class {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} :

non_unital_ring_hom_class (α →ₙ+* β) α β

Equations

non_unital_ring_hom.non_unital_ring_hom_class = {coe := non_unital_ring_hom.to_fun rβ, coe_injective' := _, map_mul := _, map_add := _, map_zero := _}

source

@[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

non_unital_ring_hom.has_coe_to_fun = {coe := non_unital_ring_hom.to_fun rβ}

source

@[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 : α →ₙ+* β) :

f.to_fun = ⇑f

source

@[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

source

@[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) :

⇑↑f = ⇑f

source

@[simp]

theorem non_unital_ring_hom.coe_to_mul_hom {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} (f : α →ₙ+* β) :

⇑(f.to_mul_hom) = ⇑f

source

@[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₁}

source

@[simp]

theorem non_unital_ring_hom.coe_to_add_monoid_hom {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} (f : α →ₙ+* β) :

⇑(f.to_add_monoid_hom) = ⇑f

source

@[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₃}

source

@[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

f.copy f' h = {to_fun := (f.to_mul_hom.copy f' h).to_fun, map_mul' := _, map_zero' := _, map_add' := _}

source

@[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'

source

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

source

@[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

source

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

source

@[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

source

theorem non_unital_ring_hom.coe_add_monoid_hom_injective {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} :

function.injective coe

source

theorem non_unital_ring_hom.coe_mul_hom_injective {α : Type u_2} {β : Type u_3} {rα : non_unital_non_assoc_semiring α} {rβ : non_unital_non_assoc_semiring β} :

function.injective coe

source

@[protected]

def non_unital_ring_hom.id (α : Type u_1) [non_unital_non_assoc_semiring α] :

α →ₙ+* α

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

Equations

non_unital_ring_hom.id α = {to_fun := id α, map_mul' := _, map_zero' := _, map_add' := _}

source

@[protected, instance]

def non_unital_ring_hom.has_zero {α : Type u_2} {β : Type u_3} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] :

has_zero (α →ₙ+* β)

Equations

non_unital_ring_hom.has_zero = {zero := {to_fun := 0, map_mul' := _, map_zero' := _, map_add' := _}}

source

@[protected, instance]

def non_unital_ring_hom.inhabited {α : Type u_2} {β : Type u_3} [rα : non_unital_non_assoc_semiring α] [rβ : non_unital_non_assoc_semiring β] :

inhabited (α →ₙ+* β)

Equations

non_unital_ring_hom.inhabited = {default := 0}

source

@[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

source

@[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

source

@[simp]

theorem non_unital_ring_hom.id_apply {α : Type u_2} [rα : non_unital_non_assoc_semiring α] (x : α) :

⇑(non_unital_ring_hom.id α) x = x

source

@[simp]

theorem non_unital_ring_hom.coe_add_monoid_hom_id {α : Type u_2} [rα : non_unital_non_assoc_semiring α] :

↑(non_unital_ring_hom.id α) = add_monoid_hom.id α

source

@[simp]

theorem non_unital_ring_hom.coe_mul_hom_id {α : Type u_2} [rα : non_unital_non_assoc_semiring α] :

↑(non_unital_ring_hom.id α) = mul_hom.id α

source

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

g.comp f = {to_fun := (g.to_mul_hom.comp f.to_mul_hom).to_fun, map_mul' := _, map_zero' := _, map_add' := _}

source

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.

source

@[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

source

@[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)

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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 : α →ₙ+* β) :

f.comp (non_unital_ring_hom.id α) = f

source

@[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 : α →ₙ+* β) :

(non_unital_ring_hom.id β).comp f = f

source

@[protected, instance]

def non_unital_ring_hom.monoid_with_zero {α : Type u_2} [rα : non_unital_non_assoc_semiring α] :

monoid_with_zero (α →ₙ+* α)

Equations

non_unital_ring_hom.monoid_with_zero = {mul := non_unital_ring_hom.comp rα, mul_assoc := _, one := non_unital_ring_hom.id α rα, one_mul := _, mul_one := _, npow := monoid.npow._default (non_unital_ring_hom.id α) non_unital_ring_hom.comp non_unital_ring_hom.id_comp non_unital_ring_hom.comp_id, npow_zero' := _, npow_succ' := _, zero := 0, zero_mul := _, mul_zero := _}

source

theorem non_unital_ring_hom.one_def {α : Type u_2} [rα : non_unital_non_assoc_semiring α] :

1 = non_unital_ring_hom.id α

source

@[simp]

theorem non_unital_ring_hom.coe_one {α : Type u_2} [rα : non_unital_non_assoc_semiring α] :

⇑1 = id

source

theorem non_unital_ring_hom.mul_def {α : Type u_2} [rα : non_unital_non_assoc_semiring α] (f g : α →ₙ+* α) :

f * g = f.comp g

source

@[simp]

theorem non_unital_ring_hom.coe_mul {α : Type u_2} [rα : non_unital_non_assoc_semiring α] (f g : α →ₙ+* α) :

⇑(f * g) = ⇑f ∘ ⇑g

source

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₂

source

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₂

source

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 : α →+ β).

source

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 : α →* β).

source

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 : α →ₙ+* β).

source

structure ring_hom (α : Type u_5) (β : Type u_6) [non_assoc_semiring α] [non_assoc_semiring β] :

Type (max u_5 u_6)

to_fun : α → β
map_one' : self.to_fun 1 = 1
map_mul' : ∀ (x y : α), self.to_fun (x * y) = self.to_fun x * self.to_fun y
map_zero' : self.to_fun 0 = 0
map_add' : ∀ (x y : α), self.to_fun (x + y) = self.to_fun x + self.to_fun y

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

source

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 : α →*₀ β).

source

@[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)) [non_assoc_semiring α] [non_assoc_semiring β] [self : ring_hom_class F α β] :

monoid_with_zero_hom_class F α β

source

@[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 α β] :

monoid_hom_class F α β

source

@[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)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective ring_hom_class.coe
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

source

@[instance]

def ring_hom_class.to_add_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 α β] :

add_monoid_hom_class F α β

source

@[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.

source

@[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

ring_hom.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}}

source

@[protected, instance]

def ring_hom_class.to_non_unital_ring_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [non_assoc_semiring α] [non_assoc_semiring β] [ring_hom_class F α β] :

non_unital_ring_hom_class F α β

Equations

ring_hom_class.to_non_unital_ring_hom_class = {coe := ring_hom_class.coe _inst_3, coe_injective' := _, map_mul := _, map_add := _, map_zero := _}

source

@[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

ring_hom.ring_hom_class = {coe := ring_hom.to_fun rβ, coe_injective' := _, map_mul := _, map_one := _, map_add := _, map_zero := _}

source

@[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

ring_hom.has_coe_to_fun = {coe := ring_hom.to_fun rβ}

source

@[simp]

theorem ring_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :

f.to_fun = ⇑f

source

@[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

source

@[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) :

⇑↑f = ⇑f

source

@[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

ring_hom.has_coe_monoid_hom = {coe := ring_hom.to_monoid_hom rβ}

source

@[simp, norm_cast]

theorem ring_hom.coe_monoid_hom {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :

⇑↑f = ⇑f

source

@[simp]

theorem ring_hom.to_monoid_hom_eq_coe {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :

f.to_monoid_hom = ↑f

source

@[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 : α →+* β) :

⇑(f.to_monoid_with_zero_hom) = ⇑f

source

@[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₂}

source

@[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 : α →+* β) :

⇑↑f = ⇑f

source

@[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 : α →+* β) :

f.to_add_monoid_hom = ↑f

source

@[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₄}

source

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

f.copy f' h = {to_fun := (f.to_monoid_with_zero_hom.copy f' h).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[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'

source

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

source

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

source

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

source

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

source

@[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

source

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

source

@[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

source

theorem ring_hom.coe_add_monoid_hom_injective {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :

function.injective coe

source

theorem ring_hom.coe_monoid_hom_injective {α : Type u_2} {β : Type u_3} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :

function.injective coe

source

@[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.

source

@[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.

source

@[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.

source

@[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.

source

@[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.

source

@[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.

source

@[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

source

@[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

source

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.

source

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.

source

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}.

source

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

source

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

nontrivial α

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

source

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

subsingleton β

source

@[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.

source

@[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.

source

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

ring_hom.mk' f map_add = {to_fun := (add_monoid_hom.mk' ⇑f map_add).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

theorem ring_hom.is_unit_map {α : Type u_2} {β : Type u_3} [semiring α] [semiring β] (f : α →+* β) {a : α} :

is_unit a → is_unit (⇑f a)

source

@[protected]

theorem ring_hom.map_dvd {α : Type u_2} {β : Type u_3} [semiring α] [semiring β] (f : α →+* β) {a b : α} :

a ∣ b → ⇑f a ∣ ⇑f b

source

def ring_hom.id (α : Type u_1) [non_assoc_semiring α] :

α →+* α

The identity ring homomorphism from a semiring to itself.

Equations

ring_hom.id α = {to_fun := id α, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

Instances for ring_hom.id

source

@[protected, instance]

def ring_hom.inhabited {α : Type u_2} [rα : non_assoc_semiring α] :

inhabited (α →+* α)

Equations

ring_hom.inhabited = {default := ring_hom.id α rα}

source

@[simp]

theorem ring_hom.id_apply {α : Type u_2} [rα : non_assoc_semiring α] (x : α) :

⇑(ring_hom.id α) x = x

source

@[simp]

theorem ring_hom.coe_add_monoid_hom_id {α : Type u_2} [rα : non_assoc_semiring α] :

↑(ring_hom.id α) = add_monoid_hom.id α

source

@[simp]

theorem ring_hom.coe_monoid_hom_id {α : Type u_2} [rα : non_assoc_semiring α] :

↑(ring_hom.id α) = monoid_hom.id α

source

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

g.comp f = {to_fun := ⇑g ∘ ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

Instances for ring_hom.comp

is_local_ring_hom_comp

source

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.

source

@[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

source

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)

source

@[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

source

@[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

source

@[protected, instance]

def ring_hom.monoid {α : Type u_2} [rα : non_assoc_semiring α] :

monoid (α →+* α)

Equations

ring_hom.monoid = {mul := ring_hom.comp rα, mul_assoc := _, one := ring_hom.id α rα, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (α →+* α)), npow_zero' := _, npow_succ' := _}

source

theorem ring_hom.one_def {α : Type u_2} [rα : non_assoc_semiring α] :

1 = ring_hom.id α

source

theorem ring_hom.mul_def {α : Type u_2} [rα : non_assoc_semiring α] (f g : α →+* α) :

f * g = f.comp g

source

@[simp]

theorem ring_hom.coe_one {α : Type u_2} [rα : non_assoc_semiring α] :

⇑1 = id

source

@[simp]

theorem ring_hom.coe_mul {α : Type u_2} [rα : non_assoc_semiring α] (f g : α →+* α) :

⇑(f * g) = ⇑f ∘ ⇑g

source

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₂

source

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₂

source

@[protected]

theorem function.injective.is_domain {α : Type u_2} {β : Type u_3} [ring α] [is_domain α] [ring β] (f : β →+* α) (hf : function.injective ⇑f) :

is_domain β

Pullback is_domain instance along an injective function.

source

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

f.mk_ring_hom_of_mul_self_of_two_ne_zero h h_two h_one = {to_fun := f.to_fun, map_one' := h_one, map_mul' := _, map_zero' := _, map_add' := _}

source

@[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) :

⇑(f.mk_ring_hom_of_mul_self_of_two_ne_zero h h_two h_one) = ⇑f

source

@[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) :

↑(f.mk_ring_hom_of_mul_self_of_two_ne_zero h h_two h_one) = f

mathlib3 documentation

Homomorphisms of semirings and rings #

Main definitions #

Notations #

Implementation notes #

Tags #