Homomorphisms of semirings and rings

This file defines bundled homomorphisms of (non-unital) semirings and rings. As with monoid and groups, we use the same structure RingHom a β, a.k.a. α →+* β, for both types of homomorphisms.

Main definitions

• NonUnitalRingHom: Non-unital (semi)ring homomorphisms. Additive monoid homomorphism which preserve multiplication.
• RingHom: (Semi)ring homomorphisms. Monoid homomorphisms which are also additive monoid homomorphism.

Notations

• →ₙ+*: Non-unital (semi)ring homs
• →+*: (Semi)ring homs

Implementation notes

• There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

• There is no SemiringHom -- the idea is that RingHom is used. The constructor for a RingHom between semirings needs a proof of map_zero, map_one and map_add as well as map_mul; a separate constructor RingHom.mk' will construct ring homs between rings from monoid homs given only a proof that addition is preserved.

Tags

RingHom, SemiringHom

structure NonUnitalRingHom (α : Type u_5) (β : Type u_6) [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] extends α →ₙ* β, α →+ β : Type (max u_5 u_6)

Bundled non-unital semiring homomorphisms α →ₙ+* β; use this for bundled non-unital ring homomorphisms too.

When possible, instead of parametrizing results over (f : α →ₙ+* β), you should parametrize over (F : Type*) [NonUnitalRingHomClass F α β] (f : F).

When you extend this structure, make sure to extend NonUnitalRingHomClass.

• toFun : α → β
• map_mul' : ∀ (x y : α), self.toFun (x * y) = self.toFun x * self.toFun y
• map_zero' : self.toFun 0 = 0
• map_add' : ∀ (x y : α), self.toFun (x + y) = self.toFun x + self.toFun y

def «term_→ₙ+*_» : Lean.TrailingParserDescr

α →ₙ+* β denotes the type of non-unital ring homomorphisms from α to β.

Equations

• «term_→ₙ+*_» = Lean.ParserDescr.trailingNode `«term_→ₙ+*_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₙ+* ") (Lean.ParserDescr.cat `term 25))

class NonUnitalRingHomClass (F : Type u_5) (α : outParam (Type u_6)) (β : outParam (Type u_7)) [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [FunLike F α β] extends MulHomClass F α β, AddMonoidHomClass F α β : Prop

NonUnitalRingHomClass F α β states that F is a type of non-unital (semi)ring homomorphisms. You should extend this class when you extend NonUnitalRingHom.

• map_mul : ∀ (f : F) (x y : α), f (x * y) = f x * f y
• map_add : ∀ (f : F) (x y : α), f (x + y) = f x + f y
• map_zero : ∀ (f : F), f 0 = 0

def NonUnitalRingHomClass.toNonUnitalRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [FunLike F α β] [NonUnitalRingHomClass F α β] (f : F) : α →ₙ+* β

Turn an element of a type F satisfying NonUnitalRingHomClass F α β into an actual NonUnitalRingHom. This is declared as the default coercion from F to α →ₙ+* β.

Equations

• ↑f = { toMulHom := ↑f, map_zero' := ⋯, map_add' := ⋯ }

instance instCoeTCNonUnitalRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [FunLike F α β] [NonUnitalRingHomClass F α β] : CoeTC F (α →ₙ+* β)

Any type satisfying NonUnitalRingHomClass can be cast into NonUnitalRingHom via NonUnitalRingHomClass.toNonUnitalRingHom.

Equations

• instCoeTCNonUnitalRingHom = { coe := NonUnitalRingHomClass.toNonUnitalRingHom }

instance NonUnitalRingHom.instFunLike {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : FunLike (α →ₙ+* β) α β

Equations

• NonUnitalRingHom.instFunLike = { coe := fun (f : α →ₙ+* β) => f.toFun, coe_injective' := ⋯ }

instance NonUnitalRingHom.instNonUnitalRingHomClass {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : NonUnitalRingHomClass (α →ₙ+* β) α β

Equations

• ⋯ = ⋯

@[simp]

theorem NonUnitalRingHom.coe_toMulHom {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) : ⇑f.toMulHom = ⇑f

@[simp]

theorem NonUnitalRingHom.coe_mulHom_mk {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α → β) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : { toFun := f, map_mul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : α), { toFun := f, map_mul' := h₁ }.toFun (x + y) = { toFun := f, map_mul' := h₁ }.toFun x + { toFun := f, map_mul' := h₁ }.toFun y) : ↑{ toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = { toFun := f, map_mul' := h₁ }

theorem NonUnitalRingHom.coe_toAddMonoidHom {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) : ⇑f.toAddMonoidHom = ⇑f

@[simp]

theorem NonUnitalRingHom.coe_addMonoidHom_mk {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α → β) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : { toFun := f, map_mul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : α), { toFun := f, map_mul' := h₁ }.toFun (x + y) = { toFun := f, map_mul' := h₁ }.toFun x + { toFun := f, map_mul' := h₁ }.toFun y) : ↑{ toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = { toFun := f, map_zero' := h₂, map_add' := h₃ }

def NonUnitalRingHom.copy {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (f' : α → β) (h : f' = ⇑f) : α →ₙ+* β

Copy of a RingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

• f.copy f' h = { toMulHom := f.copy f' h, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem NonUnitalRingHom.coe_copy {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem NonUnitalRingHom.copy_eq {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

theorem NonUnitalRingHom.ext {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] ⦃f g : α →ₙ+* β⦄ : (∀ (x : α), f x = g x) → f = g

@[simp]

theorem NonUnitalRingHom.mk_coe {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : α), { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) = { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y) : { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = f

theorem NonUnitalRingHom.coe_addMonoidHom_injective {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : Function.Injective fun (f : α →ₙ+* β) => ↑f

theorem NonUnitalRingHom.coe_mulHom_injective {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : Function.Injective fun (f : α →ₙ+* β) => ↑f

def NonUnitalRingHom.id (α : Type u_5) [NonUnitalNonAssocSemiring α] : α →ₙ+* α

The identity non-unital ring homomorphism from a non-unital semiring to itself.

Equations

• NonUnitalRingHom.id α = { toFun := id, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

instance NonUnitalRingHom.instZero {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : Zero (α →ₙ+* β)

Equations

• NonUnitalRingHom.instZero = { zero := { toFun := 0, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } }

instance NonUnitalRingHom.instInhabited {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : Inhabited (α →ₙ+* β)

Equations

• NonUnitalRingHom.instInhabited = { default := 0 }

@[simp]

theorem NonUnitalRingHom.coe_zero {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : ⇑0 = 0

@[simp]

theorem NonUnitalRingHom.zero_apply {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (x : α) : 0 x = 0

@[simp]

theorem NonUnitalRingHom.id_apply {α : Type u_2} [NonUnitalNonAssocSemiring α] (x : α) : (NonUnitalRingHom.id α) x = x

@[simp]

theorem NonUnitalRingHom.coe_addMonoidHom_id {α : Type u_2} [NonUnitalNonAssocSemiring α] : ↑(NonUnitalRingHom.id α) = AddMonoidHom.id α

@[simp]

theorem NonUnitalRingHom.coe_mulHom_id {α : Type u_2} [NonUnitalNonAssocSemiring α] : ↑(NonUnitalRingHom.id α) = MulHom.id α

def NonUnitalRingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) : α →ₙ+* γ

Composition of non-unital ring homomorphisms is a non-unital ring homomorphism.

Equations

• g.comp f = { toMulHom := g.comp f.toMulHom, map_zero' := ⋯, map_add' := ⋯ }

theorem NonUnitalRingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] {δ : Type u_5} {x✝ : NonUnitalNonAssocSemiring δ} (f : α →ₙ+* β) (g : β →ₙ+* γ) (h : γ →ₙ+* δ) : (h.comp g).comp f = h.comp (g.comp f)

Composition of non-unital ring homomorphisms is associative.

@[simp]

theorem NonUnitalRingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) : ⇑(g.comp f) = ⇑g ∘ ⇑f

@[simp]

theorem NonUnitalRingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α) : (g.comp f) x = g (f x)

@[simp]

theorem NonUnitalRingHom.coe_comp_addMonoidHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) : { toFun := ⇑g ∘ ⇑f, map_zero' := ⋯, map_add' := ⋯ } = (↑g).comp ↑f

@[simp]

theorem NonUnitalRingHom.coe_comp_mulHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) : { toFun := ⇑g ∘ ⇑f, map_mul' := ⋯ } = (↑g).comp ↑f

@[simp]

theorem NonUnitalRingHom.comp_zero {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) : g.comp 0 = 0

@[simp]

theorem NonUnitalRingHom.zero_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (f : α →ₙ+* β) : NonUnitalRingHom.comp 0 f = 0

@[simp]

theorem NonUnitalRingHom.comp_id {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) : f.comp (NonUnitalRingHom.id α) = f

@[simp]

theorem NonUnitalRingHom.id_comp {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) : (NonUnitalRingHom.id β).comp f = f

instance NonUnitalRingHom.instMonoidWithZero {α : Type u_2} [NonUnitalNonAssocSemiring α] : MonoidWithZero (α →ₙ+* α)

Equations

• NonUnitalRingHom.instMonoidWithZero = MonoidWithZero.mk ⋯ ⋯

theorem NonUnitalRingHom.one_def {α : Type u_2} [NonUnitalNonAssocSemiring α] : 1 = NonUnitalRingHom.id α

@[simp]

theorem NonUnitalRingHom.coe_one {α : Type u_2} [NonUnitalNonAssocSemiring α] : ⇑1 = id

theorem NonUnitalRingHom.mul_def {α : Type u_2} [NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α) : f * g = f.comp g

@[simp]

theorem NonUnitalRingHom.coe_mul {α : Type u_2} [NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α) : ⇑(f * g) = ⇑f ∘ ⇑g

@[simp]

theorem NonUnitalRingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] {g₁ g₂ : β →ₙ+* γ} {f : α →ₙ+* β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem NonUnitalRingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] {g : β →ₙ+* γ} {f₁ f₂ : α →ₙ+* β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

structure RingHom (α : Type u_5) (β : Type u_6) [NonAssocSemiring α] [NonAssocSemiring β] extends α →* β, α →+ β, α →ₙ+* β, α →*₀ β : Type (max u_5 u_6)

Bundled semiring homomorphisms; use this for bundled ring homomorphisms too.

This extends from both MonoidHom and MonoidWithZeroHom in order to put the fields in a sensible order, even though MonoidWithZeroHom already extends MonoidHom.

• toFun : α → β
• map_one' : (↑↑self).toFun 1 = 1
• map_mul' : ∀ (x y : α), (↑↑self).toFun (x * y) = (↑↑self).toFun x * (↑↑self).toFun y
• map_zero' : (↑↑self).toFun 0 = 0
• map_add' : ∀ (x y : α), (↑↑self).toFun (x + y) = (↑↑self).toFun x + (↑↑self).toFun y

def «term_→+*_» : Lean.TrailingParserDescr

α →+* β denotes the type of ring homomorphisms from α to β.

Equations

• «term_→+*_» = Lean.ParserDescr.trailingNode `«term_→+*_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →+* ") (Lean.ParserDescr.cat `term 25))

class RingHomClass (F : Type u_5) (α : outParam (Type u_6)) (β : outParam (Type u_7)) [NonAssocSemiring α] [NonAssocSemiring β] [FunLike F α β] extends MonoidHomClass F α β, AddMonoidHomClass F α β, MonoidWithZeroHomClass F α β : Prop

RingHomClass F α β states that F is a type of (semi)ring homomorphisms. You should extend this class when you extend RingHom.

This extends from both MonoidHomClass and MonoidWithZeroHomClass in order to put the fields in a sensible order, even though MonoidWithZeroHomClass already extends MonoidHomClass.

• map_mul : ∀ (f : F) (x y : α), f (x * y) = f x * f y
• map_one : ∀ (f : F), f 1 = 1
• map_add : ∀ (f : F) (x y : α), f (x + y) = f x + f y
• map_zero : ∀ (f : F), f 0 = 0

def RingHomClass.toRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} [RingHomClass F α β] (f : F) : α →+* β

Turn an element of a type F satisfying RingHomClass F α β into an actual RingHom. This is declared as the default coercion from F to α →+* β.

Equations

• ↑f = { toMonoidHom := ↑f, map_zero' := ⋯, map_add' := ⋯ }

instance instCoeTCRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} [RingHomClass F α β] : CoeTC F (α →+* β)

Any type satisfying RingHomClass can be cast into RingHom via RingHomClass.toRingHom.

Equations

• instCoeTCRingHom = { coe := RingHomClass.toRingHom }

@[instance 100]

instance RingHomClass.toNonUnitalRingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} [RingHomClass F α β] : NonUnitalRingHomClass F α β

Equations

• ⋯ = ⋯

Throughout this section, some Semiring arguments are specified with {} instead of []. See note [implicit instance arguments].

instance RingHom.instFunLike {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} : FunLike (α →+* β) α β

Equations

• RingHom.instFunLike = { coe := fun (f : α →+* β) => (↑↑f).toFun, coe_injective' := ⋯ }

instance RingHom.instRingHomClass {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} : RingHomClass (α →+* β) α β

Equations

• ⋯ = ⋯

theorem RingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) : (↑↑f).toFun = ⇑f

@[simp]

theorem RingHom.coe_mk {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →* β) (h₁ : (↑f).toFun 0 = 0) (h₂ : ∀ (x y : α), (↑f).toFun (x + y) = (↑f).toFun x + (↑f).toFun y) : ⇑{ toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = ⇑f

@[simp]

theorem RingHom.coe_coe {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} {F : Type u_5} [FunLike F α β] [RingHomClass F α β] (f : F) : ⇑↑f = ⇑f

instance RingHom.coeToMonoidHom {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} : Coe (α →+* β) (α →* β)

Equations

• RingHom.coeToMonoidHom = { coe := RingHom.toMonoidHom }

@[simp]

theorem RingHom.toMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) : ↑f = ↑f

theorem RingHom.toMonoidWithZeroHom_eq_coe {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) : ⇑f.toMonoidWithZeroHom = ⇑f

@[simp]

theorem RingHom.coe_monoidHom_mk {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →* β) (h₁ : (↑f).toFun 0 = 0) (h₂ : ∀ (x y : α), (↑f).toFun (x + y) = (↑f).toFun x + (↑f).toFun y) : ↑{ toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = f

@[simp]

theorem RingHom.toAddMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) : f.toAddMonoidHom = ↑f

@[simp]

theorem RingHom.coe_addMonoidHom_mk {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α → β) (h₁ : f 1 = 1) (h₂ : ∀ (x y : α), { toFun := f, map_one' := h₁ }.toFun (x * y) = { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y) (h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x y : α), (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x + (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y) : ↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ } = { toFun := f, map_zero' := h₃, map_add' := h₄ }

def RingHom.copy {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) (f' : α → β) (h : f' = ⇑f) : α →+* β

Copy of a RingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

• f.copy f' h = { toMonoidHom := f.toMonoidWithZeroHom.copy f' h, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingHom.coe_copy {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem RingHom.copy_eq {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

theorem RingHom.congr_fun {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} {f g : α →+* β} (h : f = g) (x : α) : f x = g x

theorem RingHom.congr_arg {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) {x y : α} (h : x = y) : f x = f y

theorem RingHom.coe_inj {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} ⦃f g : α →+* β⦄ (h : ⇑f = ⇑g) : f = g

theorem RingHom.ext {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} ⦃f g : α →+* β⦄ : (∀ (x : α), f x = g x) → f = g

@[simp]

theorem RingHom.mk_coe {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) (h₁ : f 1 = 1) (h₂ : ∀ (x y : α), { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) = { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y) (h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x y : α), (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x + (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y) : { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ } = f

theorem RingHom.coe_addMonoidHom_injective {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} : Function.Injective fun (f : α →+* β) => ↑f

theorem RingHom.coe_monoidHom_injective {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} : Function.Injective fun (f : α →+* β) => ↑f

theorem RingHom.map_zero {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) : f 0 = 0

Ring homomorphisms map zero to zero.

theorem RingHom.map_one {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) : f 1 = 1

Ring homomorphisms map one to one.

theorem RingHom.map_add {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) (a b : α) : f (a + b) = f a + f b

Ring homomorphisms preserve addition.

theorem RingHom.map_mul {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) (a b : α) : f (a * b) = f a * f b

Ring homomorphisms preserve multiplication.

@[simp]

theorem RingHom.map_ite_zero_one {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} {F : Type u_5} [FunLike F α β] [RingHomClass F α β] (f : F) (p : Prop) [Decidable p] : f (if p then 0 else 1) = if p then 0 else 1

@[simp]

theorem RingHom.map_ite_one_zero {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} {F : Type u_5} [FunLike F α β] [RingHomClass F α β] (f : F) (p : Prop) [Decidable p] : f (if p then 1 else 0) = if p then 1 else 0

theorem RingHom.codomain_trivial_iff_map_one_eq_zero {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) : 0 = 1 ↔ f 1 = 0

f : α →+* β has a trivial codomain iff f 1 = 0.

theorem RingHom.codomain_trivial_iff_range_trivial {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) : 0 = 1 ↔ ∀ (x : α), f x = 0

f : α →+* β has a trivial codomain iff it has a trivial range.

theorem RingHom.map_one_ne_zero {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) [Nontrivial β] : f 1 ≠ 0

f : α →+* β doesn't map 1 to 0 if β is nontrivial

theorem RingHom.domain_nontrivial {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) [Nontrivial β] : Nontrivial α

If there is a homomorphism f : α →+* β and β is nontrivial, then α is nontrivial.

theorem RingHom.codomain_trivial {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) [h : Subsingleton α] : Subsingleton β

theorem RingHom.map_neg {α : Type u_2} {β : Type u_3} [NonAssocRing α] [NonAssocRing β] (f : α →+* β) (x : α) : f (-x) = -f x

Ring homomorphisms preserve additive inverse.

theorem RingHom.map_sub {α : Type u_2} {β : Type u_3} [NonAssocRing α] [NonAssocRing β] (f : α →+* β) (x y : α) : f (x - y) = f x - f y

Ring homomorphisms preserve subtraction.

def RingHom.mk' {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [NonAssocRing β] (f : α →* β) (map_add : ∀ (a b : α), f (a + b) = f a + f b) : α →+* β

Makes a ring homomorphism from a monoid homomorphism of rings which preserves addition.

Equations

• RingHom.mk' f map_add = { toFun := (↑(AddMonoidHom.mk' (⇑f) map_add)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def RingHom.id (α : Type u_5) [NonAssocSemiring α] : α →+* α

The identity ring homomorphism from a semiring to itself.

Equations

• RingHom.id α = { toFun := id, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

instance RingHom.instInhabited {α : Type u_2} {x✝ : NonAssocSemiring α} : Inhabited (α →+* α)

Equations

• RingHom.instInhabited = { default := RingHom.id α }

@[simp]

theorem RingHom.id_apply {α : Type u_2} {x✝ : NonAssocSemiring α} (x : α) : (RingHom.id α) x = x

@[simp]

theorem RingHom.coe_addMonoidHom_id {α : Type u_2} {x✝ : NonAssocSemiring α} : ↑(RingHom.id α) = AddMonoidHom.id α

@[simp]

theorem RingHom.coe_monoidHom_id {α : Type u_2} {x✝ : NonAssocSemiring α} : ↑(RingHom.id α) = MonoidHom.id α

def RingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} {x✝² : NonAssocSemiring γ} (g : β →+* γ) (f : α →+* β) : α →+* γ

Composition of ring homomorphisms is a ring homomorphism.

Equations

• g.comp f = { toFun := ⇑g ∘ ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem RingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} {x✝² : NonAssocSemiring γ} {δ : Type u_5} {x✝³ : NonAssocSemiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ) : (h.comp g).comp f = h.comp (g.comp f)

Composition of semiring homomorphisms is associative.

@[simp]

theorem RingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} {x✝² : NonAssocSemiring γ} (hnp : β →+* γ) (hmn : α →+* β) : ⇑(hnp.comp hmn) = ⇑hnp ∘ ⇑hmn

theorem RingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} {x✝² : NonAssocSemiring γ} (hnp : β →+* γ) (hmn : α →+* β) (x : α) : (hnp.comp hmn) x = hnp (hmn x)

@[simp]

theorem RingHom.comp_id {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) : f.comp (RingHom.id α) = f

@[simp]

theorem RingHom.id_comp {α : Type u_2} {β : Type u_3} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) : (RingHom.id β).comp f = f

instance RingHom.instOne {α : Type u_2} {x✝ : NonAssocSemiring α} : One (α →+* α)

Equations

• RingHom.instOne = { one := RingHom.id α }

instance RingHom.instMul {α : Type u_2} {x✝ : NonAssocSemiring α} : Mul (α →+* α)

Equations

• RingHom.instMul = { mul := RingHom.comp }

theorem RingHom.one_def {α : Type u_2} {x✝ : NonAssocSemiring α} : 1 = RingHom.id α

theorem RingHom.mul_def {α : Type u_2} {x✝ : NonAssocSemiring α} (f g : α →+* α) : f * g = f.comp g

@[simp]

theorem RingHom.coe_one {α : Type u_2} {x✝ : NonAssocSemiring α} : ⇑1 = id

@[simp]

theorem RingHom.coe_mul {α : Type u_2} {x✝ : NonAssocSemiring α} (f g : α →+* α) : ⇑(f * g) = ⇑f ∘ ⇑g

instance RingHom.instMonoid {α : Type u_2} {x✝ : NonAssocSemiring α} : Monoid (α →+* α)

Equations

• RingHom.instMonoid = Monoid.mk ⋯ ⋯ (fun (n : ℕ) (f : α →+* α) => (npowRec n f).copy (⇑f)^[n] ⋯) ⋯ ⋯

@[simp]

theorem RingHom.coe_pow {α : Type u_2} {x✝ : NonAssocSemiring α} (f : α →+* α) (n : ℕ) : ⇑(f ^ n) = (⇑f)^[n]

@[simp]

theorem RingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} {x✝² : NonAssocSemiring γ} {g₁ g₂ : β →+* γ} {f : α →+* β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem RingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} {x✝² : NonAssocSemiring γ} {g : β →+* γ} {f₁ f₂ : α →+* β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

theorem RingHom.map_pow {α : Type u_2} {β : Type u_3} [Semiring α] [Semiring β] (f : α →+* β) (a : α) (n : ℕ) : f (a ^ n) = f a ^ n

def AddMonoidHom.mkRingHomOfMulSelfOfTwoNeZero {α : Type u_2} {β : Type u_3} [CommRing α] [IsDomain α] [CommRing β] (f : β →+ α) (h : ∀ (x : β), f (x * x) = f x * f x) (h_two : 2 ≠ 0) (h_one : f 1 = 1) : β →+* α

Make a ring homomorphism from an additive group homomorphism from a commutative ring to an integral domain that commutes with self multiplication, assumes that two is nonzero and 1 is sent to 1.

Equations

• f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one = { toFun := (↑f).toFun, map_one' := h_one, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero {α : Type u_2} {β : Type u_3} [CommRing α] [IsDomain α] [CommRing β] (f : β →+ α) (h : ∀ (x : β), f (x * x) = f x * f x) (h_two : 2 ≠ 0) (h_one : f 1 = 1) : ⇑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) = ⇑f

@[simp]

theorem AddMonoidHom.coe_addMonoidHom_mkRingHomOfMulSelfOfTwoNeZero {α : Type u_2} {β : Type u_3} [CommRing α] [IsDomain α] [CommRing β] (f : β →+ α) (h : ∀ (x : β), f (x * x) = f x * f x) (h_two : 2 ≠ 0) (h_one : f 1 = 1) : ↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) = f