mathlib documentation

deprecated.ring

Unbundled semiring and ring homomorphisms (deprecated)

This file defines typeclasses for unbundled semiring and ring homomorphisms. Though these classes are deprecated, they are still widely 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

@[class]
structure is_semiring_hom {α : Type u} {β : Type v} [semiring α] [semiring β] :
(α → β) → 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).

Instances
@[instance]
def 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 : α → β) [is_semiring_hom f] {γ : Type u_1} [semiring γ] (g : β → γ) [is_semiring_hom g] :

The composition of two semiring homomorphisms is a semiring homomorphism.

@[instance]
def is_semiring_hom.is_add_monoid_hom {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α → β) [is_semiring_hom f] :

A semiring homomorphism is an additive monoid homomorphism.

@[instance]
def is_semiring_hom.is_monoid_hom {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α → β) [is_semiring_hom f] :

A semiring homomorphism is a monoid homomorphism.

@[class]
structure is_ring_hom {α : Type u} {β : Type v} [ring α] [ring β] :
(α → β) → 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).

Instances
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 : α → β) [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 : α → β) [is_ring_hom f] {x : α} :
f (-x) = -f x

Ring homomorphisms preserve additive inverses.

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

Ring homomorphisms preserve subtraction.

@[instance]
def 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 : α → β) [is_ring_hom f] {γ : Type u_1} [ring γ] (g : β → γ) [is_ring_hom g] :

The composition of two ring homomorphisms is a ring homomorphism.

@[instance]
def is_ring_hom.is_semiring_hom {α : Type u} {β : Type v} [ring α] [ring β] (f : α → β) [is_ring_hom f] :

A ring homomorphism is also a semiring homomorphism.

@[instance]
def is_ring_hom.is_add_group_hom {α : Type u} {β : Type v} [ring α] [ring β] (f : α → β) [is_ring_hom f] :

def ring_hom.of {α : Type u} {β : Type v} [rα : semiring α] [rβ : semiring β] (f : α → β) [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 : α → β) [is_semiring_hom f] :

@[instance]
def ring_hom.is_semiring_hom {α : Type u} {β : Type v} [rα : semiring α] [rβ : semiring β] (f : α →+* β) :

@[instance]
def ring_hom.is_ring_hom {α : Type u_1} {γ : Type u_2} [ring α] [ring γ] (g : α →+* γ) :