mathlib3 documentation

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

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