mathlib documentation

deprecated.ring

Unbundled semiring and ring homomorphisms (deprecated) #

This file defines structures for unbundled semiring and ring homomorphisms. Though bundled morphisms are now preferred, the unbundled structures are still occasionally used in mathlib, and probably will not go away before Lean 4 because Lean 3 often fails to coerce a bundled homomorphism to a function.

Main Definitions #

is_semiring_hom (deprecated), is_ring_hom (deprecated)

Tags #

is_semiring_hom, is_ring_hom

structure is_semiring_hom {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α → β) :

Prop

map_zero : f 0 = 0
map_one : f 1 = 1
map_add : ∀ {x y : α}, f (x + y) = f x + f y
map_mul : ∀ {x y : α}, f (x * y) = (f x) * f y

Predicate for semiring homomorphisms (deprecated -- use the bundled ring_hom version).

theorem is_semiring_hom.id {α : Type u} [semiring α] :

is_semiring_hom id

The identity map is a semiring homomorphism.

theorem is_semiring_hom.comp {α : Type u} {β : Type v} [semiring α] [semiring β] {f : α → β} (hf : is_semiring_hom f) {γ : Type u_1} [semiring γ] {g : β → γ} (hg : is_semiring_hom g) :

is_semiring_hom (g ∘ f)

The composition of two semiring homomorphisms is a semiring homomorphism.

theorem is_semiring_hom.to_is_add_monoid_hom {α : Type u} {β : Type v} [semiring α] [semiring β] {f : α → β} (hf : is_semiring_hom f) :

is_add_monoid_hom f

A semiring homomorphism is an additive monoid homomorphism.

theorem is_semiring_hom.to_is_monoid_hom {α : Type u} {β : Type v} [semiring α] [semiring β] {f : α → β} (hf : is_semiring_hom f) :

is_monoid_hom f

A semiring homomorphism is a monoid homomorphism.

structure is_ring_hom {α : Type u} {β : Type v} [ring α] [ring β] (f : α → β) :

Prop

map_one : f 1 = 1
map_mul : ∀ {x y : α}, f (x * y) = (f x) * f y
map_add : ∀ {x y : α}, f (x + y) = f x + f y

Predicate for ring homomorphisms (deprecated -- use the bundled ring_hom version).

theorem is_ring_hom.of_semiring {α : Type u} {β : Type v} [ring α] [ring β] {f : α → β} (H : is_semiring_hom f) :

A map of rings that is a semiring homomorphism is also a ring homomorphism.

theorem is_ring_hom.map_zero {α : Type u} {β : Type v} [ring α] [ring β] {f : α → β} (hf : is_ring_hom f) :

f 0 = 0

Ring homomorphisms map zero to zero.

theorem is_ring_hom.map_neg {α : Type u} {β : Type v} [ring α] [ring β] {f : α → β} {x : α} (hf : is_ring_hom f) :

f (-x) = -f x

Ring homomorphisms preserve additive inverses.

theorem is_ring_hom.map_sub {α : Type u} {β : Type v} [ring α] [ring β] {f : α → β} {x y : α} (hf : is_ring_hom f) :

f (x - y) = f x - f y

Ring homomorphisms preserve subtraction.

theorem is_ring_hom.id {α : Type u} [ring α] :

The identity map is a ring homomorphism.

theorem is_ring_hom.comp {α : Type u} {β : Type v} [ring α] [ring β] {f : α → β} (hf : is_ring_hom f) {γ : Type u_1} [ring γ] {g : β → γ} (hg : is_ring_hom g) :

is_ring_hom (g ∘ f)

The composition of two ring homomorphisms is a ring homomorphism.

theorem is_ring_hom.to_is_semiring_hom {α : Type u} {β : Type v} [ring α] [ring β] {f : α → β} (hf : is_ring_hom f) :

is_semiring_hom f

A ring homomorphism is also a semiring homomorphism.

theorem is_ring_hom.to_is_add_group_hom {α : Type u} {β : Type v} [ring α] [ring β] {f : α → β} (hf : is_ring_hom f) :

is_add_group_hom f

def ring_hom.of {α : Type u} {β : Type v} [rα : semiring α] [rβ : semiring β] {f : α → β} (hf : is_semiring_hom f) :

α →+* β

Interpret f : α → β with is_semiring_hom f as a ring homomorphism.

Equations

ring_hom.of hf = {to_fun := f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[simp]

theorem ring_hom.coe_of {α : Type u} {β : Type v} [rα : semiring α] [rβ : semiring β] {f : α → β} (hf : is_semiring_hom f) :

⇑(ring_hom.of hf) = f

theorem ring_hom.to_is_semiring_hom {α : Type u} {β : Type v} [rα : semiring α] [rβ : semiring β] (f : α →+* β) :

is_semiring_hom ⇑f

theorem ring_hom.to_is_ring_hom {α : Type u_1} {γ : Type u_2} [ring α] [ring γ] (g : α →+* γ) :

is_ring_hom ⇑g