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 β] (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).

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 β] (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).

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 : α →+* γ) :