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

ink

structure NonUnitalRingHom (α : Type u_1) (β : Type u_2) [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] extends MulHom : Type (maxu_1u_2)

• The proposition that the function preserves 0

  map_zero' : MulHom.toFun toMulHom 0 = 0

• The proposition that the function preserves addition

  map_add' : ∀ (x y : α), MulHom.toFun toMulHom (x + y) = MulHom.toFun toMulHom x + MulHom.toFun toMulHom y

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.

ink

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))

ink

abbrev NonUnitalRingHom.toAddMonoidHom {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] (self : α →ₙ+* β) : α →+ β

Reinterpret a non-unital ring homomorphism f : α →ₙ+* β→ₙ+* β as an additive monoid homomorphism α →+ β→+ β. The simp-normal form is (f : α →+ β)→+ β).

Equations

• One or more equations did not get rendered due to their size.

ink

class NonUnitalRingHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] extends MulHomClass : Type (max(maxu_1u_2)u_3)

• The proposition that the function preserves addition

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

• The proposition that the function preserves 0

  map_zero : ∀ (f : F), ↑f 0 = 0

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

ink

def NonUnitalRingHomClass.toNonUnitalRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] [inst : 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

• One or more equations did not get rendered due to their size.

ink

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

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

Equations

• instCoeTCNonUnitalRingHom = { coe := NonUnitalRingHomClass.toNonUnitalRingHom }

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

ink

instance NonUnitalRingHom.instNonUnitalRingHomClassNonUnitalRingHom {α : Type u_1} {β : Type u_2} : {x : NonUnitalNonAssocSemiring α} → {x_1 : NonUnitalNonAssocSemiring β} → NonUnitalRingHomClass (α →ₙ+* β) α β

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem NonUnitalRingHom.coe_toMulHom {α : Type u_1} {β : Type u_2} : ∀ {x : NonUnitalNonAssocSemiring α} {x_1 : NonUnitalNonAssocSemiring β} (f : α →ₙ+* β), ↑f.toMulHom = ↑f

ink

@[simp]

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

ink

theorem NonUnitalRingHom.coe_toAddMonoidHom {α : Type u_1} {β : Type u_2} : ∀ {x : NonUnitalNonAssocSemiring α} {x_1 : NonUnitalNonAssocSemiring β} (f : α →ₙ+* β), ↑(NonUnitalRingHom.toAddMonoidHom f) = ↑f

ink

@[simp]

theorem NonUnitalRingHom.coe_addMonoidHom_mk {α : Type u_2} {β : Type u_1} : ∀ {x : NonUnitalNonAssocSemiring α} {x_1 : NonUnitalNonAssocSemiring β} (f : α → β) (h₁ : ∀ (x_2 y : α), f (x_2 * y) = f x_2 * f y) (h₂ : MulHom.toFun { toFun := f, map_mul' := h₁ } 0 = 0) (h₃ : ∀ (x_2 y : α), MulHom.toFun { toFun := f, map_mul' := h₁ } (x_2 + y) = MulHom.toFun { toFun := f, map_mul' := h₁ } x_2 + MulHom.toFun { toFun := f, map_mul' := h₁ } y), ↑{ toMulHom := { toFun := f, map_mul' := h₁ }, map_zero' := h₂, map_add' := h₃ } = { toZeroHom := { toFun := f, map_zero' := h₂ }, map_add' := h₃ }

ink

def NonUnitalRingHom.copy {α : Type u_1} {β : Type u_2} : {x : NonUnitalNonAssocSemiring α} → {x_1 : NonUnitalNonAssocSemiring β} → (f : α →ₙ+* β) → (f' : α → β) → f' = ↑f → α →ₙ+* β

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem NonUnitalRingHom.coe_copy {α : Type u_1} {β : Type u_2} : ∀ {x : NonUnitalNonAssocSemiring α} {x_1 : NonUnitalNonAssocSemiring β} (f : α →ₙ+* β) (f' : α → β) (h : f' = ↑f), ↑(NonUnitalRingHom.copy f f' h) = f'

ink

theorem NonUnitalRingHom.copy_eq {α : Type u_1} {β : Type u_2} : ∀ {x : NonUnitalNonAssocSemiring α} {x_1 : NonUnitalNonAssocSemiring β} (f : α →ₙ+* β) (f' : α → β) (h : f' = ↑f), NonUnitalRingHom.copy f f' h = f

ink

theorem NonUnitalRingHom.ext {α : Type u_1} {β : Type u_2} : ∀ {x : NonUnitalNonAssocSemiring α} {x_1 : NonUnitalNonAssocSemiring β} ⦃f g : α →ₙ+* β⦄, (∀ (x_2 : α), ↑f x_2 = ↑g x_2) → f = g

ink

theorem NonUnitalRingHom.ext_iff {α : Type u_1} {β : Type u_2} : ∀ {x : NonUnitalNonAssocSemiring α} {x_1 : NonUnitalNonAssocSemiring β} {f g : α →ₙ+* β}, f = g ↔ ∀ (x_2 : α), ↑f x_2 = ↑g x_2

ink

@[simp]

theorem NonUnitalRingHom.mk_coe {α : Type u_1} {β : Type u_2} : ∀ {x : NonUnitalNonAssocSemiring α} {x_1 : NonUnitalNonAssocSemiring β} (f : α →ₙ+* β) (h₁ : ∀ (x_2 y : α), ↑f (x_2 * y) = ↑f x_2 * ↑f y) (h₂ : MulHom.toFun { toFun := ↑f, map_mul' := h₁ } 0 = 0) (h₃ : ∀ (x_2 y : α), MulHom.toFun { toFun := ↑f, map_mul' := h₁ } (x_2 + y) = MulHom.toFun { toFun := ↑f, map_mul' := h₁ } x_2 + MulHom.toFun { toFun := ↑f, map_mul' := h₁ } y), { toMulHom := { toFun := ↑f, map_mul' := h₁ }, map_zero' := h₂, map_add' := h₃ } = f

ink

theorem NonUnitalRingHom.coe_addMonoidHom_injective {α : Type u_1} {β : Type u_2} : ∀ {x : NonUnitalNonAssocSemiring α} {x_1 : NonUnitalNonAssocSemiring β}, Function.Injective fun f => ↑f

ink

theorem NonUnitalRingHom.coe_mulHom_injective {α : Type u_1} {β : Type u_2} : ∀ {x : NonUnitalNonAssocSemiring α} {x_1 : NonUnitalNonAssocSemiring β}, Function.Injective fun f => ↑f

ink

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

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• NonUnitalRingHom.instInhabitedNonUnitalRingHom = { default := 0 }

ink

@[simp]

theorem NonUnitalRingHom.coe_zero {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] : ↑0 = 0

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

def NonUnitalRingHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] : {x : NonUnitalNonAssocSemiring γ} → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γ

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Composition of non-unital ring homomorphisms is associative.

ink

@[simp]

theorem NonUnitalRingHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] : ∀ {x : NonUnitalNonAssocSemiring γ} (g : β →ₙ+* γ) (f : α →ₙ+* β), ↑(NonUnitalRingHom.comp g f) = ↑g ∘ ↑f

ink

@[simp]

theorem NonUnitalRingHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] : ∀ {x : NonUnitalNonAssocSemiring γ} (g : β →ₙ+* γ) (f : α →ₙ+* β) (x_1 : α), ↑(NonUnitalRingHom.comp g f) x_1 = ↑g (↑f x_1)

ink

@[simp]

theorem NonUnitalRingHom.coe_comp_addMonoidHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] : ∀ {x : NonUnitalNonAssocSemiring γ} (g : β →ₙ+* γ) (f : α →ₙ+* β), { toZeroHom := { toFun := ↑g ∘ ↑f, map_zero' := (_ : MulHom.toFun (NonUnitalRingHom.comp g f).toMulHom 0 = 0) }, map_add' := (_ : ∀ (x_1 y : α), MulHom.toFun (NonUnitalRingHom.comp g f).toMulHom (x_1 + y) = MulHom.toFun (NonUnitalRingHom.comp g f).toMulHom x_1 + MulHom.toFun (NonUnitalRingHom.comp g f).toMulHom y) } = AddMonoidHom.comp ↑g ↑f

ink

@[simp]

theorem NonUnitalRingHom.coe_comp_mulHom {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] : ∀ {x : NonUnitalNonAssocSemiring γ} (g : β →ₙ+* γ) (f : α →ₙ+* β), { toFun := ↑g ∘ ↑f, map_mul' := (_ : ∀ (x_1 y : α), MulHom.toFun (NonUnitalRingHom.comp g f).toMulHom (x_1 * y) = MulHom.toFun (NonUnitalRingHom.comp g f).toMulHom x_1 * MulHom.toFun (NonUnitalRingHom.comp g f).toMulHom y) } = MulHom.comp ↑g ↑f

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

instance NonUnitalRingHom.instMonoidWithZeroNonUnitalRingHom {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : MonoidWithZero (α →ₙ+* α)

Equations

• NonUnitalRingHom.instMonoidWithZeroNonUnitalRingHom = MonoidWithZero.mk (_ : ∀ (f : α →ₙ+* α), NonUnitalRingHom.comp 0 f = 0) (_ : ∀ (g : α →ₙ+* α), NonUnitalRingHom.comp g 0 = 0)

ink

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

ink

@[simp]

theorem NonUnitalRingHom.coe_one {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : ↑1 = id

ink

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

ink

@[simp]

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

ink

theorem NonUnitalRingHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] : ∀ {x : NonUnitalNonAssocSemiring γ} {g₁ g₂ : β →ₙ+* γ} {f : α →ₙ+* β}, Function.Surjective ↑f → (NonUnitalRingHom.comp g₁ f = NonUnitalRingHom.comp g₂ f ↔ g₁ = g₂)

ink

theorem NonUnitalRingHom.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst : NonUnitalNonAssocSemiring β] : ∀ {x : NonUnitalNonAssocSemiring γ} {g : β →ₙ+* γ} {f₁ f₂ : α →ₙ+* β}, Function.Injective ↑g → (NonUnitalRingHom.comp g f₁ = NonUnitalRingHom.comp g f₂ ↔ f₁ = f₂)

ink

structure RingHom (α : Type u_1) (β : Type u_2) [inst : NonAssocSemiring α] [inst : NonAssocSemiring β] extends MonoidHom : Type (maxu_1u_2)

• The proposition that the function preserves 0

  map_zero' : OneHom.toFun (↑toMonoidHom) 0 = 0

• The proposition that the function preserves addition

  map_add' : ∀ (x y : α), OneHom.toFun (↑toMonoidHom) (x + y) = OneHom.toFun (↑toMonoidHom) x + OneHom.toFun (↑toMonoidHom) y

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.

ink

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))

ink

abbrev RingHom.toMonoidWithZeroHom {α : Type u_1} {β : Type u_2} [inst : NonAssocSemiring α] [inst : NonAssocSemiring β] (self : α →+* β) : α →*₀ β

Reinterpret a ring homomorphism f : α →+* β→+* β as a monoid with zero homomorphism α →*₀ β→*₀ β. The simp-normal form is (f : α →*₀ β)→*₀ β).

Equations

• One or more equations did not get rendered due to their size.

ink

abbrev RingHom.toAddMonoidHom {α : Type u_1} {β : Type u_2} [inst : NonAssocSemiring α] [inst : NonAssocSemiring β] (self : α →+* β) : α →+ β

Reinterpret a ring homomorphism f : α →+* β→+* β as an additive monoid homomorphism α →+ β→+ β. The simp-normal form is (f : α →+ β)→+ β).

Equations

• One or more equations did not get rendered due to their size.

ink

abbrev RingHom.toNonUnitalRingHom {α : Type u_1} {β : Type u_2} [inst : NonAssocSemiring α] [inst : NonAssocSemiring β] (self : α →+* β) : α →ₙ+* β

Reinterpret a ring homomorphism f : α →+* β→+* β as a non-unital ring homomorphism α →ₙ+* β→ₙ+* β. The simp-normal form is (f : α →ₙ+* β)→ₙ+* β).

Equations

• One or more equations did not get rendered due to their size.

ink

class RingHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : NonAssocSemiring α] [inst : NonAssocSemiring β] extends MonoidHomClass : Type (max(maxu_1u_2)u_3)

• The proposition that the function preserves addition

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

• The proposition that the function preserves 0

  map_zero : ∀ (f : F), ↑f 0 = 0

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.

ink

@[simp]

theorem map_bit1 {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : NonAssocSemiring α] [inst : NonAssocSemiring β] [inst : RingHomClass F α β] (f : F) (a : α) : ↑f (bit1 a) = bit1 (↑f a)

Ring homomorphisms preserve bit1.

ink

def RingHomClass.toRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → [inst : RingHomClass 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

• One or more equations did not get rendered due to their size.

ink

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

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

Equations

• instCoeTCRingHom = { coe := RingHomClass.toRingHom }

ink

instance RingHomClass.toNonUnitalRingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} : {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → [inst : RingHomClass F α β] → NonUnitalRingHomClass F α β

Equations

• RingHomClass.toNonUnitalRingHomClass = let src := inst; NonUnitalRingHomClass.mk (_ : ∀ (f : F) (x y : α), ↑f (x + y) = ↑f x + ↑f y) (_ : ∀ (f : F), ↑f 0 = 0)

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

ink

instance RingHom.instRingHomClassRingHom {α : Type u_1} {β : Type u_2} : {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → RingHomClass (α →+* β) α β

Equations

• One or more equations did not get rendered due to their size.

ink

theorem RingHom.toFun_eq_coe {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), (↑↑f).toFun = ↑f

ink

@[simp]

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

ink

@[simp]

theorem RingHom.coe_coe {α : Type u_2} {β : Type u_3} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_1} [inst : RingHomClass F α β] (f : F), ↑↑f = ↑f

ink

instance RingHom.coeToMonoidHom {α : Type u_1} {β : Type u_2} : {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → Coe (α →+* β) (α →* β)

Equations

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

ink

@[simp]

theorem RingHom.toMonoidHom_eq_coe {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), ↑f = ↑f

ink

theorem RingHom.toMonoidWithZeroHom_eq_coe {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), ↑(RingHom.toMonoidWithZeroHom f) = ↑f

ink

@[simp]

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

ink

@[simp]

theorem RingHom.toAddMonoidHom_eq_coe {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), RingHom.toAddMonoidHom f = ↑f

ink

@[simp]

theorem RingHom.coe_addMonoidHom_mk {α : Type u_2} {β : Type u_1} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α → β) (h₁ : f 1 = 1) (h₂ : ∀ (x_2 y : α), OneHom.toFun { toFun := f, map_one' := h₁ } (x_2 * y) = OneHom.toFun { toFun := f, map_one' := h₁ } x_2 * OneHom.toFun { toFun := f, map_one' := h₁ } y) (h₃ : OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0) (h₄ : ∀ (x_2 y : α), OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) (x_2 + y) = OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) x_2 + OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) y), ↑{ toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ } = { toZeroHom := { toFun := f, map_zero' := h₃ }, map_add' := h₄ }

ink

def RingHom.copy {α : Type u_1} {β : Type u_2} : {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → (f : α →+* β) → (f' : α → β) → f' = ↑f → α →+* β

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem RingHom.coe_copy {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (f' : α → β) (h : f' = ↑f), ↑(RingHom.copy f f' h) = f'

ink

theorem RingHom.copy_eq {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (f' : α → β) (h : f' = ↑f), RingHom.copy f f' h = f

ink

theorem RingHom.congr_fun {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {f g : α →+* β}, f = g → ∀ (x_2 : α), ↑f x_2 = ↑g x_2

ink

theorem RingHom.congr_arg {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) {x_2 y : α}, x_2 = y → ↑f x_2 = ↑f y

ink

theorem RingHom.coe_inj {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄, ↑f = ↑g → f = g

ink

theorem RingHom.ext {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄, (∀ (x_2 : α), ↑f x_2 = ↑g x_2) → f = g

ink

theorem RingHom.ext_iff {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {f g : α →+* β}, f = g ↔ ∀ (x_2 : α), ↑f x_2 = ↑g x_2

ink

@[simp]

theorem RingHom.mk_coe {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (h₁ : ↑f 1 = 1) (h₂ : ∀ (x_2 y : α), OneHom.toFun { toFun := ↑f, map_one' := h₁ } (x_2 * y) = OneHom.toFun { toFun := ↑f, map_one' := h₁ } x_2 * OneHom.toFun { toFun := ↑f, map_one' := h₁ } y) (h₃ : OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0) (h₄ : ∀ (x_2 y : α), OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) (x_2 + y) = OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) x_2 + OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) y), { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ } = f

ink

theorem RingHom.coe_addMonoidHom_injective {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, Function.Injective fun f => ↑f

ink

theorem RingHom.coe_monoidHom_injective {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, Function.Injective fun f => ↑f

ink

theorem RingHom.map_zero {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), ↑f 0 = 0

Ring homomorphisms map zero to zero.

ink

theorem RingHom.map_one {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), ↑f 1 = 1

Ring homomorphisms map one to one.

ink

theorem RingHom.map_add {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (a b : α), ↑f (a + b) = ↑f a + ↑f b

Ring homomorphisms preserve addition.

ink

theorem RingHom.map_mul {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (a b : α), ↑f (a * b) = ↑f a * ↑f b

Ring homomorphisms preserve multiplication.

ink

@[simp]

theorem RingHom.map_ite_zero_one {α : Type u_2} {β : Type u_3} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_1} [inst : RingHomClass F α β] (f : F) (p : Prop) [inst_1 : Decidable p], ↑f (if p then 0 else 1) = if p then 0 else 1

ink

@[simp]

theorem RingHom.map_ite_one_zero {α : Type u_2} {β : Type u_3} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_1} [inst : RingHomClass F α β] (f : F) (p : Prop) [inst_1 : Decidable p], ↑f (if p then 1 else 0) = if p then 1 else 0

ink

theorem RingHom.codomain_trivial_iff_map_one_eq_zero {α : Type u_2} {β : Type u_1} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), 0 = 1 ↔ ↑f 1 = 0

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

ink

theorem RingHom.codomain_trivial_iff_range_trivial {α : Type u_2} {β : Type u_1} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), 0 = 1 ↔ ∀ (x_2 : α), ↑f x_2 = 0

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

ink

theorem RingHom.codomain_trivial_iff_range_eq_singleton_zero {α : Type u_2} {β : Type u_1} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), 0 = 1 ↔ Set.range ↑f = {0}

f : α →+* β→+* β has a trivial codomain iff its range is {0}.

ink

theorem RingHom.map_one_ne_zero {α : Type u_2} {β : Type u_1} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) [inst : Nontrivial β], ↑f 1 ≠ 0

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

ink

theorem RingHom.domain_nontrivial {α : Type u_2} {β : Type u_1} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, (α →+* β) → ∀ [inst : Nontrivial β], Nontrivial α

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

ink

theorem RingHom.codomain_trivial {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, (α →+* β) → ∀ [h : Subsingleton α], Subsingleton β

ink

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

Ring homomorphisms preserve additive inverse.

ink

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

Ring homomorphisms preserve subtraction.

ink

def RingHom.mk' {α : Type u_1} {β : Type u_2} [inst : NonAssocSemiring α] [inst : 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

• One or more equations did not get rendered due to their size.

ink

theorem RingHom.isUnit_map {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst : Semiring β] (f : α →+* β) {a : α} : IsUnit a → IsUnit (↑f a)

ink

theorem RingHom.map_dvd {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst : Semiring β] (f : α →+* β) {a : α} {b : α} : a ∣ b → ↑f a ∣ ↑f b

ink

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

The identity ring homomorphism from a semiring to itself.

Equations

• One or more equations did not get rendered due to their size.

ink

instance RingHom.instInhabitedRingHom {α : Type u_1} : {x : NonAssocSemiring α} → Inhabited (α →+* α)

Equations

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

ink

@[simp]

theorem RingHom.id_apply {α : Type u_1} : ∀ {x : NonAssocSemiring α} (x_1 : α), ↑(RingHom.id α) x_1 = x_1

ink

@[simp]

theorem RingHom.coe_addMonoidHom_id {α : Type u_1} : ∀ {x : NonAssocSemiring α}, ↑(RingHom.id α) = AddMonoidHom.id α

ink

@[simp]

theorem RingHom.coe_monoidHom_id {α : Type u_1} : ∀ {x : NonAssocSemiring α}, ↑(RingHom.id α) = MonoidHom.id α

ink

def RingHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} : {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → {x_2 : NonAssocSemiring γ} → (β →+* γ) → (α →+* β) → α →+* γ

Composition of ring homomorphisms is a ring homomorphism.

Equations

• One or more equations did not get rendered due to their size.

ink

theorem RingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} {δ : Type u_1} {x_3 : NonAssocSemiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ), RingHom.comp (RingHom.comp h g) f = RingHom.comp h (RingHom.comp g f)

Composition of semiring homomorphisms is associative.

ink

@[simp]

theorem RingHom.coe_comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} (hnp : β →+* γ) (hmn : α →+* β), ↑(RingHom.comp hnp hmn) = ↑hnp ∘ ↑hmn

ink

theorem RingHom.comp_apply {α : Type u_3} {β : Type u_1} {γ : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} (hnp : β →+* γ) (hmn : α →+* β) (x_3 : α), ↑(RingHom.comp hnp hmn) x_3 = ↑hnp (↑hmn x_3)

ink

@[simp]

theorem RingHom.comp_id {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), RingHom.comp f (RingHom.id α) = f

ink

@[simp]

theorem RingHom.id_comp {α : Type u_1} {β : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), RingHom.comp (RingHom.id β) f = f

ink

instance RingHom.instMonoidRingHom {α : Type u_1} : {x : NonAssocSemiring α} → Monoid (α →+* α)

Equations

• RingHom.instMonoidRingHom = Monoid.mk (_ : ∀ (f : α →+* α), RingHom.comp (RingHom.id α) f = f) (_ : ∀ (f : α →+* α), RingHom.comp f (RingHom.id α) = f) npowRec

ink

theorem RingHom.one_def {α : Type u_1} : ∀ {x : NonAssocSemiring α}, 1 = RingHom.id α

ink

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

ink

@[simp]

theorem RingHom.coe_one {α : Type u_1} : ∀ {x : NonAssocSemiring α}, ↑1 = id

ink

@[simp]

theorem RingHom.coe_mul {α : Type u_1} : ∀ {x : NonAssocSemiring α} (f g : α →+* α), ↑(f * g) = ↑f ∘ ↑g

ink

theorem RingHom.cancel_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} {g₁ g₂ : β →+* γ} {f : α →+* β}, Function.Surjective ↑f → (RingHom.comp g₁ f = RingHom.comp g₂ f ↔ g₁ = g₂)

ink

theorem RingHom.cancel_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} {g : β →+* γ} {f₁ f₂ : α →+* β}, Function.Injective ↑g → (RingHom.comp g f₁ = RingHom.comp g f₂ ↔ f₁ = f₂)

ink

theorem Function.Injective.isDomain {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst : IsDomain α] [inst : Ring β] (f : β →+* α) (hf : Function.Injective ↑f) : IsDomain β

Pullback IsDomain instance along an injective function.

ink

def AddMonoidHom.mkRingHomOfMulSelfOfTwoNeZero {α : Type u_1} {β : Type u_2} [inst : CommRing α] [inst : IsDomain α] [inst : 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

• One or more equations did not get rendered due to their size.

ink

@[simp]

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

ink

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