Unbundled semiring and ring homomorphisms (deprecated)

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 RingHom, 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

IsSemiringHom (deprecated), IsRingHom (deprecated)

Tags

IsSemiringHom, IsRingHom

structure IsSemiringHom {α : Type u} {β : Type v} [Semiring α] [Semiring β] (f : α → β) : Prop

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

• map_zero : f 0 = 0

  The proposition that f preserves the additive identity.

• map_one : f 1 = 1

  The proposition that f preserves the multiplicative identity.

• map_add : ∀ (x y : α), f (x + y) = f x + f y

  The proposition that f preserves addition.

• map_mul : ∀ (x y : α), f (x * y) = f x * f y

  The proposition that f preserves multiplication.

theorem IsSemiringHom.map_zero {α : Type u} {β : Type v} [Semiring α] [Semiring β] {f : α → β} (self : IsSemiringHom f) : f 0 = 0

The proposition that f preserves the additive identity.

theorem IsSemiringHom.map_one {α : Type u} {β : Type v} [Semiring α] [Semiring β] {f : α → β} (self : IsSemiringHom f) : f 1 = 1

The proposition that f preserves the multiplicative identity.

theorem IsSemiringHom.map_add {α : Type u} {β : Type v} [Semiring α] [Semiring β] {f : α → β} (self : IsSemiringHom f) (x : α) (y : α) : f (x + y) = f x + f y

The proposition that f preserves addition.

theorem IsSemiringHom.map_mul {α : Type u} {β : Type v} [Semiring α] [Semiring β] {f : α → β} (self : IsSemiringHom f) (x : α) (y : α) : f (x * y) = f x * f y

The proposition that f preserves multiplication.

theorem IsSemiringHom.id {α : Type u} [Semiring α] : IsSemiringHom id

The identity map is a semiring homomorphism.

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

The composition of two semiring homomorphisms is a semiring homomorphism.

theorem IsSemiringHom.to_isAddMonoidHom {α : Type u} {β : Type v} [Semiring α] [Semiring β] {f : α → β} (hf : IsSemiringHom f) : IsAddMonoidHom f

A semiring homomorphism is an additive monoid homomorphism.

theorem IsSemiringHom.to_isMonoidHom {α : Type u} {β : Type v} [Semiring α] [Semiring β] {f : α → β} (hf : IsSemiringHom f) : IsMonoidHom f

A semiring homomorphism is a monoid homomorphism.

structure IsRingHom {α : Type u} {β : Type v} [Ring α] [Ring β] (f : α → β) : Prop

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

• map_one : f 1 = 1

  The proposition that f preserves the multiplicative identity.

• map_mul : ∀ (x y : α), f (x * y) = f x * f y

  The proposition that f preserves multiplication.

• map_add : ∀ (x y : α), f (x + y) = f x + f y

  The proposition that f preserves addition.

theorem IsRingHom.map_one {α : Type u} {β : Type v} [Ring α] [Ring β] {f : α → β} (self : IsRingHom f) : f 1 = 1

The proposition that f preserves the multiplicative identity.

theorem IsRingHom.map_mul {α : Type u} {β : Type v} [Ring α] [Ring β] {f : α → β} (self : IsRingHom f) (x : α) (y : α) : f (x * y) = f x * f y

The proposition that f preserves multiplication.

theorem IsRingHom.map_add {α : Type u} {β : Type v} [Ring α] [Ring β] {f : α → β} (self : IsRingHom f) (x : α) (y : α) : f (x + y) = f x + f y

The proposition that f preserves addition.

theorem IsRingHom.of_semiring {α : Type u} {β : Type v} [Ring α] [Ring β] {f : α → β} (H : IsSemiringHom f) : IsRingHom f

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

theorem IsRingHom.map_zero {α : Type u} {β : Type v} [Ring α] [Ring β] {f : α → β} (hf : IsRingHom f) : f 0 = 0

Ring homomorphisms map zero to zero.

theorem IsRingHom.map_neg {α : Type u} {β : Type v} [Ring α] [Ring β] {f : α → β} {x : α} (hf : IsRingHom f) : f (-x) = -f x

Ring homomorphisms preserve additive inverses.

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

Ring homomorphisms preserve subtraction.

theorem IsRingHom.id {α : Type u} [Ring α] : IsRingHom id

The identity map is a ring homomorphism.

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

The composition of two ring homomorphisms is a ring homomorphism.

theorem IsRingHom.to_isSemiringHom {α : Type u} {β : Type v} [Ring α] [Ring β] {f : α → β} (hf : IsRingHom f) : IsSemiringHom f

A ring homomorphism is also a semiring homomorphism.

theorem IsRingHom.to_isAddGroupHom {α : Type u} {β : Type v} [Ring α] [Ring β] {f : α → β} (hf : IsRingHom f) : IsAddGroupHom f

def RingHom.of {α : Type u} {β : Type v} {rα : Semiring α} {rβ : Semiring β} {f : α → β} (hf : IsSemiringHom f) : α →+* β

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

Equations

• RingHom.of hf = let __src := MonoidHom.of ⋯; let __src := AddMonoidHom.of ⋯; { toFun := f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingHom.coe_of {α : Type u} {β : Type v} {rα : Semiring α} {rβ : Semiring β} {f : α → β} (hf : IsSemiringHom f) : ⇑(RingHom.of hf) = f

theorem RingHom.to_isSemiringHom {α : Type u} {β : Type v} {rα : Semiring α} {rβ : Semiring β} (f : α →+* β) : IsSemiringHom ⇑f

theorem RingHom.to_isRingHom {α : Type u_1} {γ : Type u_2} [Ring α] [Ring γ] (g : α →+* γ) : IsRingHom ⇑g