deprecated.ring

# Unbundled semiring and ring homomorphisms (deprecated) #

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

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

This file defines predicates for unbundled semiring and ring homomorphisms. Instead of using this file, please use ring_hom, defined in algebra.hom.ring, with notation →+*, for morphisms between semirings or rings. For example use φ : A →+* B to represent a ring homomorphism.

## 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 α] :

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

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

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

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

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

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

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) :
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
@[simp]
theorem ring_hom.coe_of {α : Type u} {β : Type v} [rα : semiring α] [rβ : semiring β] {f : α β} (hf : is_semiring_hom f) :
theorem ring_hom.to_is_semiring_hom {α : Type u} {β : Type v} [rα : semiring α] [rβ : semiring β] (f : α →+* β) :
theorem ring_hom.to_is_ring_hom {α : Type u_1} {γ : Type u_2} [ring α] [ring γ] (g : α →+* γ) :