Mathlib.Algebra.Ring.Hom.Defs

NonUnitalRingHom structure

(α β : Type*) [NonUnitalNonAssocSemiring α]
  [NonUnitalNonAssocSemiring β] extends α →ₙ* β, α →+ β

Full source

/-- 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`. -/
structure NonUnitalRingHom (α β : Type*) [NonUnitalNonAssocSemiring α]
  [NonUnitalNonAssocSemiring β] extends α →ₙ* β, α →+ β

Non-unital (Semi)Ring Homomorphism

Informal description

The structure representing bundled non-unital semiring homomorphisms, also used for non-unital ring homomorphisms, i.e., a map that preserves both the additive monoid structure and the multiplicative structure (without requiring preservation of multiplicative identity). More precisely, given two non-unital non-associative semirings $\alpha$ and $\beta$, a non-unital ring homomorphism is a function $f: \alpha \to \beta$ that: 1. Preserves addition: $f(x + y) = f(x) + f(y)$ for all $x, y \in \alpha$ 2. Preserves zero: $f(0) = 0$ 3. Preserves multiplication: $f(x * y) = f(x) * f(y)$ for all $x, y \in \alpha$ This structure extends both the multiplicative homomorphism (`α →ₙ* β`) and additive homomorphism (`α →+ β`) structures.

term_→ₙ+*_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `α →ₙ+* β` denotes the type of non-unital ring homomorphisms from `α` to `β`. -/
infixr:25 " →ₙ+* " => NonUnitalRingHom

Non-unital ring homomorphism notation

Informal description

The notation `α →ₙ+* β` denotes the type of non-unital ring homomorphisms from `α$ to $\beta$.

NonUnitalRingHomClass structure

(F : Type*) (α β : outParam Type*) [NonUnitalNonAssocSemiring α]
  [NonUnitalNonAssocSemiring β] [FunLike F α β] : Prop
  extends MulHomClass F α β, AddMonoidHomClass F α β

Full source

/-- `NonUnitalRingHomClass F α β` states that `F` is a type of non-unital (semi)ring
homomorphisms. You should extend this class when you extend `NonUnitalRingHom`. -/
class NonUnitalRingHomClass (F : Type*) (α β : outParam Type*) [NonUnitalNonAssocSemiring α]
  [NonUnitalNonAssocSemiring β] [FunLike F α β] : Prop
  extends MulHomClass F α β, AddMonoidHomClass F α β

Class of Non-unital (Semi)ring Homomorphisms

Informal description

The class `NonUnitalRingHomClass F α β` states that `F` is a type of non-unital (semi)ring homomorphisms between non-unital non-associative semirings `α` and `β`. A term of type `F` is a function that preserves both the additive monoid structure and the multiplicative structure, but does not necessarily preserve a multiplicative identity. This class extends both `MulHomClass` (preserving multiplication) and `AddMonoidHomClass` (preserving addition and zero), indicating that elements of `F` must satisfy both multiplicative and additive homomorphism properties.

NonUnitalRingHomClass.toNonUnitalRingHom definition

(f : F) : α →ₙ+* β

Full source

/-- Turn an element of a type `F` satisfying `NonUnitalRingHomClass F α β` into an actual
`NonUnitalRingHom`. This is declared as the default coercion from `F` to `α →ₙ+* β`. -/
@[coe]
def NonUnitalRingHomClass.toNonUnitalRingHom (f : F) : α →ₙ+* β :=
  { (f : α →ₙ* β), (f : α →+ β) with }

Coercion from non-unital ring homomorphism class to concrete homomorphism

Informal description

Given a type `F` satisfying `NonUnitalRingHomClass F α β` (i.e., elements of `F` are non-unital semiring homomorphisms between non-unital non-associative semirings `α` and `β`), this function converts an element `f : F` into an actual bundled non-unital ring homomorphism `α →ₙ+* β`. The resulting homomorphism preserves both the additive structure (addition and zero) and multiplicative structure (multiplication) between the semirings. This is declared as the default coercion from `F` to `α →ₙ+* β`.

instCoeTCNonUnitalRingHom instance

: CoeTC F (α →ₙ+* β)

Full source

/-- Any type satisfying `NonUnitalRingHomClass` can be cast into `NonUnitalRingHom` via
`NonUnitalRingHomClass.toNonUnitalRingHom`. -/
instance : CoeTC F (α →ₙ+* β) :=
  ⟨NonUnitalRingHomClass.toNonUnitalRingHom⟩

Canonical Coercion from Non-Unital Ring Homomorphism Class to Bundled Homomorphisms

Informal description

For any type `F` that satisfies `NonUnitalRingHomClass F α β` (i.e., elements of `F` are non-unital semiring homomorphisms between non-unital non-associative semirings `α` and `β`), there is a canonical coercion from `F` to the type of bundled non-unital ring homomorphisms `α →ₙ+* β`. This coercion maps each element `f : F` to the corresponding bundled homomorphism preserving both the additive and multiplicative structures.

NonUnitalRingHom.instFunLike instance

: FunLike (α →ₙ+* β) α β

Full source

instance : FunLike (α →ₙ+* β) α β where
  coe f := f.toFun
  coe_injective' f g h := by
    cases f
    cases g
    congr
    apply DFunLike.coe_injective'
    exact h

Function-Like Structure for Non-Unital Ring Homomorphisms

Informal description

For non-unital non-associative semirings $\alpha$ and $\beta$, the type of non-unital ring homomorphisms $\alpha \to_{\text{n}+*} \beta$ is equipped with a function-like structure, meaning each homomorphism can be treated as a function from $\alpha$ to $\beta$.

NonUnitalRingHom.instNonUnitalRingHomClass instance

: NonUnitalRingHomClass (α →ₙ+* β) α β

Full source

instance : NonUnitalRingHomClass (α →ₙ+* β) α β where
  map_add := NonUnitalRingHom.map_add'
  map_zero := NonUnitalRingHom.map_zero'
  map_mul f := f.map_mul'

Non-Unital Ring Homomorphism Class Structure

Informal description

The type of non-unital ring homomorphisms $\alpha \to_{\text{n}+*} \beta$ between non-unital non-associative semirings $\alpha$ and $\beta$ forms a class of non-unital ring homomorphisms, meaning each homomorphism preserves both the additive and multiplicative structures.

NonUnitalRingHom.coe_toMulHom theorem

(f : α →ₙ+* β) : ⇑f.toMulHom = f

Full source

@[simp]
theorem coe_toMulHom (f : α →ₙ+* β) : ⇑f.toMulHom = f :=
  rfl

Underlying multiplicative homomorphism equals the original homomorphism

Informal description

For any non-unital ring homomorphism $f \colon \alpha \to_{\text{n}+*} \beta$ between non-unital non-associative semirings $\alpha$ and $\beta$, the underlying multiplicative homomorphism of $f$ (obtained via `f.toMulHom`) is equal to $f$ when both are viewed as functions from $\alpha$ to $\beta$.

NonUnitalRingHom.coe_mulHom_mk theorem

(f : α → β) (h₁ h₂ h₃) : ((⟨⟨f, h₁⟩, h₂, h₃⟩ : α →ₙ+* β) : α →ₙ* β) = ⟨f, h₁⟩

Full source

@[simp]
theorem coe_mulHom_mk (f : α → β) (h₁ h₂ h₃) :
    ((⟨⟨f, h₁⟩, h₂, h₃⟩ : α →ₙ+* β) : α →ₙ* β) = ⟨f, h₁⟩ :=
  rfl

Underlying multiplicative homomorphism of constructed non-unital ring homomorphism equals the multiplicative homomorphism component

Informal description

Given a function $f \colon \alpha \to \beta$ between non-unital non-associative semirings $\alpha$ and $\beta$, and proofs that $f$ preserves multiplication ($h₁$), addition ($h₂$), and zero ($h₃$), the underlying multiplicative homomorphism of the constructed non-unital ring homomorphism $\langle \langle f, h₁ \rangle, h₂, h₃ \rangle \colon \alpha \to_{\text{n}+*} \beta$ is equal to the multiplicative homomorphism $\langle f, h₁ \rangle \colon \alpha \to_{\text{n}*} \beta$.

NonUnitalRingHom.coe_toAddMonoidHom theorem

(f : α →ₙ+* β) : ⇑f.toAddMonoidHom = f

Full source

theorem coe_toAddMonoidHom (f : α →ₙ+* β) : ⇑f.toAddMonoidHom = f := rfl

Underlying Additive Homomorphism Equals Original Non-Unital Ring Homomorphism

Informal description

For any non-unital ring homomorphism $f \colon \alpha \to_{\text{n}+*} \beta$ between non-unital non-associative semirings $\alpha$ and $\beta$, the underlying additive monoid homomorphism of $f$ (obtained via `f.toAddMonoidHom`) is equal to $f$ when both are viewed as functions from $\alpha$ to $\beta$.

NonUnitalRingHom.coe_addMonoidHom_mk theorem

 (f : α → β) (h₁ h₂ h₃) : ((⟨⟨f, h₁⟩, h₂, h₃⟩ : α →ₙ+* β) : α →+ β) = ⟨⟨f, h₂⟩, h₃⟩

Full source

@[simp]
theorem coe_addMonoidHom_mk (f : α → β) (h₁ h₂ h₃) :
    ((⟨⟨f, h₁⟩, h₂, h₃⟩ : α →ₙ+* β) : α →+ β) = ⟨⟨f, h₂⟩, h₃⟩ :=
  rfl

Underlying Additive Homomorphism of Constructed Non-Unital Ring Homomorphism Equals Additive Component

Informal description

Given a function $f \colon \alpha \to \beta$ between non-unital non-associative semirings $\alpha$ and $\beta$, and proofs that $f$ preserves multiplication ($h₁$), addition ($h₂$), and zero ($h₃$), the underlying additive monoid homomorphism of the constructed non-unital ring homomorphism $\langle \langle f, h₁ \rangle, h₂, h₃ \rangle \colon \alpha \to_{\text{n}+*} \beta$ is equal to the additive monoid homomorphism $\langle \langle f, h₂ \rangle, h₃ \rangle \colon \alpha \to_{+} \beta$.

NonUnitalRingHom.copy definition

(f : α →ₙ+* β) (f' : α → β) (h : f' = f) : α →ₙ+* β

Full source

/-- Copy of a `RingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : α →ₙ+* β) (f' : α → β) (h : f' = f) : α →ₙ+* β :=
  { f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }

Copy of a non-unital ring homomorphism with a new function

Informal description

Given a non-unital ring homomorphism $f : \alpha \to_{\text{n}+*} \beta$ between non-unital non-associative semirings $\alpha$ and $\beta$, and a function $f' : \alpha \to \beta$ that is definitionally equal to $f$, the function `NonUnitalRingHom.copy` constructs a new non-unital ring homomorphism from $f'$ that behaves identically to $f$ with respect to both addition and multiplication. This is useful for fixing definitional equalities when working with non-unital ring homomorphisms.

NonUnitalRingHom.coe_copy theorem

(f : α →ₙ+* β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f'

Full source

@[simp]
theorem coe_copy (f : α →ₙ+* β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl

Underlying Function of Copied Non-Unital Ring Homomorphism Equals Given Function

Informal description

For any non-unital ring homomorphism $f \colon \alpha \to_{\text{n}+*} \beta$ between non-unital non-associative semirings $\alpha$ and $\beta$, and any function $f' \colon \alpha \to \beta$ such that $f' = f$, the underlying function of the copied homomorphism $f.copy\ f'\ h$ is equal to $f'$.

NonUnitalRingHom.copy_eq theorem

(f : α →ₙ+* β) (f' : α → β) (h : f' = f) : f.copy f' h = f

Full source

theorem copy_eq (f : α →ₙ+* β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

Copy of Non-Unital Ring Homomorphism Equals Original

Informal description

Let $\alpha$ and $\beta$ be non-unital non-associative semirings. For any non-unital ring homomorphism $f: \alpha \to_{\text{n}+*} \beta$ and any function $f': \alpha \to \beta$ such that $f' = f$, the copy of $f$ constructed with $f'$ is equal to $f$ itself.

NonUnitalRingHom.ext theorem

⦃f g : α →ₙ+* β⦄ : (∀ x, f x = g x) → f = g

Full source

@[ext]
theorem ext ⦃f g : α →ₙ+* β⦄ : (∀ x, f x = g x) → f = g :=
  DFunLike.ext _ _

Extensionality of Non-Unital Ring Homomorphisms

Informal description

For any two non-unital ring homomorphisms $f, g: \alpha \to_{\text{n}+*} \beta$ between non-unital non-associative semirings $\alpha$ and $\beta$, if $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.

NonUnitalRingHom.mk_coe theorem

(f : α →ₙ+* β) (h₁ h₂ h₃) : NonUnitalRingHom.mk (MulHom.mk f h₁) h₂ h₃ = f

Full source

@[simp]
theorem mk_coe (f : α →ₙ+* β) (h₁ h₂ h₃) : NonUnitalRingHom.mk (MulHom.mk f h₁) h₂ h₃ = f :=
  ext fun _ => rfl

Construction of Non-Unital Ring Homomorphism via Multiplicative Homomorphism Preserves Original Map

Informal description

Let $\alpha$ and $\beta$ be non-unital non-associative semirings. For any non-unital ring homomorphism $f: \alpha \to_{\text{n}+*} \beta$ and any proofs $h_1$ of multiplicative preservation, $h_2$ of additive preservation, and $h_3$ of zero preservation, the construction of $f$ via `NonUnitalRingHom.mk` from the multiplicative homomorphism `MulHom.mk f h₁` and proofs $h_2$, $h_3$ equals $f$ itself.

NonUnitalRingHom.coe_addMonoidHom_injective theorem

: Injective fun f : α →ₙ+* β => (f : α →+ β)

Full source

theorem coe_addMonoidHom_injective : Injective fun f : α →ₙ+* β => (f : α →+ β) :=
  Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Injectivity of the Additive Homomorphism Component of Non-Unital Ring Homomorphisms

Informal description

The canonical map from the type of non-unital ring homomorphisms $\alpha \to_{\text{n}+*} \beta$ to the type of additive monoid homomorphisms $\alpha \to_{+} \beta$ is injective. That is, if two non-unital ring homomorphisms $f, g: \alpha \to_{\text{n}+*} \beta$ induce the same additive monoid homomorphism, then $f = g$.

NonUnitalRingHom.coe_mulHom_injective theorem

: Injective fun f : α →ₙ+* β => (f : α →ₙ* β)

Full source

theorem coe_mulHom_injective : Injective fun f : α →ₙ+* β => (f : α →ₙ* β) :=
  Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Injectivity of the Multiplicative Homomorphism Component of Non-Unital Ring Homomorphisms

Informal description

For non-unital non-associative semirings $\alpha$ and $\beta$, the canonical map from the type of non-unital ring homomorphisms $\alpha \to_{\text{n}+*} \beta$ to the type of multiplicative homomorphisms $\alpha \to_{\text{n}*} \beta$ is injective. That is, if two non-unital ring homomorphisms $f, g : \alpha \to_{\text{n}+*} \beta$ satisfy $(f : \alpha \to_{\text{n}*} \beta) = (g : \alpha \to_{\text{n}*} \beta)$, then $f = g$.

NonUnitalRingHom.id definition

(α : Type*) [NonUnitalNonAssocSemiring α] : α →ₙ+* α

Full source

/-- The identity non-unital ring homomorphism from a non-unital semiring to itself. -/
protected def id (α : Type*) [NonUnitalNonAssocSemiring α] : α →ₙ+* α where
  toFun := id
  map_mul' _ _ := rfl
  map_zero' := rfl
  map_add' _ _ := rfl

Identity Non-unital Ring Homomorphism

Informal description

The identity non-unital ring homomorphism from a non-unital semiring $\alpha$ to itself, which maps every element to itself and preserves both the additive and multiplicative structures. Specifically: - For all $x \in \alpha$, $f(x) = x$ - $f(x * y) = f(x) * f(y)$ for all $x, y \in \alpha$ - $f(0) = 0$ - $f(x + y) = f(x) + f(y)$ for all $x, y \in \alpha$

NonUnitalRingHom.instZero instance

: Zero (α →ₙ+* β)

Full source

instance : Zero (α →ₙ+* β) :=
  ⟨{ toFun := 0, map_mul' := fun _ _ => (mul_zero (0 : β)).symm, map_zero' := rfl,
      map_add' := fun _ _ => (add_zero (0 : β)).symm }⟩

Zero Non-unital Ring Homomorphism

Informal description

For any two non-unital non-associative semirings $\alpha$ and $\beta$, the type of non-unital ring homomorphisms $\alpha \to_{\text{n}+*} \beta$ has a zero element, which is the constant zero function.

NonUnitalRingHom.instInhabited instance

: Inhabited (α →ₙ+* β)

Full source

instance : Inhabited (α →ₙ+* β) :=
  ⟨0⟩

Non-unital Ring Homomorphisms are Inhabited

Informal description

For any two non-unital non-associative semirings $\alpha$ and $\beta$, the type of non-unital ring homomorphisms $\alpha \to_{\text{n}+*} \beta$ is inhabited (i.e., contains at least one element).

NonUnitalRingHom.coe_zero theorem

: ⇑(0 : α →ₙ+* β) = 0

Full source

@[simp]
theorem coe_zero : ⇑(0 : α →ₙ+* β) = 0 :=
  rfl

Zero Non-unital Ring Homomorphism is the Zero Function

Informal description

The zero non-unital ring homomorphism $0 : \alpha \to_{\text{n}+*} \beta$ between two non-unital non-associative semirings $\alpha$ and $\beta$ is equal to the zero function, i.e., $0(x) = 0$ for all $x \in \alpha$.

NonUnitalRingHom.zero_apply theorem

(x : α) : (0 : α →ₙ+* β) x = 0

Full source

@[simp]
theorem zero_apply (x : α) : (0 : α →ₙ+* β) x = 0 :=
  rfl

Evaluation of Zero Non-unital Ring Homomorphism

Informal description

For any element $x$ in a non-unital non-associative semiring $\alpha$, the zero non-unital ring homomorphism $0 : \alpha \to_{\text{n}+*} \beta$ evaluates to the zero element of $\beta$, i.e., $0(x) = 0$.

NonUnitalRingHom.id_apply theorem

(x : α) : NonUnitalRingHom.id α x = x

Full source

@[simp]
theorem id_apply (x : α) : NonUnitalRingHom.id α x = x :=
  rfl

Identity Non-unital Ring Homomorphism Evaluation: $\text{id}(x) = x$

Informal description

For any element $x$ in a non-unital non-associative semiring $\alpha$, the identity non-unital ring homomorphism evaluated at $x$ equals $x$, i.e., $\text{id}(x) = x$.

NonUnitalRingHom.coe_addMonoidHom_id theorem

: (NonUnitalRingHom.id α : α →+ α) = AddMonoidHom.id α

Full source

@[simp]
theorem coe_addMonoidHom_id : (NonUnitalRingHom.id α : α →+ α) = AddMonoidHom.id α :=
  rfl

Identity Non-unital Ring Homomorphism as Identity Additive Monoid Homomorphism

Informal description

The additive monoid homomorphism underlying the identity non-unital ring homomorphism from a non-unital semiring $\alpha$ to itself is equal to the identity additive monoid homomorphism on $\alpha$.

NonUnitalRingHom.coe_mulHom_id theorem

: (NonUnitalRingHom.id α : α →ₙ* α) = MulHom.id α

Full source

@[simp]
theorem coe_mulHom_id : (NonUnitalRingHom.id α : α →ₙ* α) = MulHom.id α :=
  rfl

Identity Non-Unital Ring Homomorphism as Identity Multiplicative Homomorphism

Informal description

The underlying multiplicative homomorphism of the identity non-unital ring homomorphism on a non-unital non-associative semiring $\alpha$ is equal to the identity multiplicative homomorphism on $\alpha$.

NonUnitalRingHom.comp definition

(g : β →ₙ+* γ) (f : α →ₙ+* β) : α →ₙ+* γ

Full source

/-- Composition of non-unital ring homomorphisms is a non-unital ring homomorphism. -/
def comp (g : β →ₙ+* γ) (f : α →ₙ+* β) : α →ₙ+* γ :=
  { g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }

Composition of Non-unital Ring Homomorphisms

Informal description

Given non-unital non-associative semirings $\alpha$, $\beta$, and $\gamma$, the composition of two non-unital ring homomorphisms $g : \beta \to \gamma$ and $f : \alpha \to \beta$ is a non-unital ring homomorphism $\alpha \to \gamma$ defined by $(g \circ f)(x) = g(f(x))$ for all $x \in \alpha$. This composition preserves both the additive and multiplicative structures: 1. Additive structure: $(g \circ f)(x + y) = g(f(x) + f(y)) = g(f(x)) + g(f(y)) = (g \circ f)(x) + (g \circ f)(y)$ 2. Multiplicative structure: $(g \circ f)(x * y) = g(f(x * y)) = g(f(x) * f(y)) = g(f(x)) * g(f(y)) = (g \circ f)(x) * (g \circ f)(y)$

NonUnitalRingHom.comp_assoc theorem

 {δ} {_ : NonUnitalNonAssocSemiring δ} (f : α →ₙ+* β) (g : β →ₙ+* γ) (h : γ →ₙ+* δ) :
  (h.comp g).comp f = h.comp (g.comp f)

Full source

/-- Composition of non-unital ring homomorphisms is associative. -/
theorem comp_assoc {δ} {_ : NonUnitalNonAssocSemiring δ} (f : α →ₙ+* β) (g : β →ₙ+* γ)
    (h : γ →ₙ+* δ) : (h.comp g).comp f = h.comp (g.comp f) :=
  rfl

Associativity of Composition of Non-unital Ring Homomorphisms

Informal description

For non-unital non-associative semirings $\alpha$, $\beta$, $\gamma$, and $\delta$, and non-unital ring homomorphisms $f: \alpha \to \beta$, $g: \beta \to \gamma$, and $h: \gamma \to \delta$, the composition of homomorphisms is associative, i.e., $(h \circ g) \circ f = h \circ (g \circ f)$.

NonUnitalRingHom.coe_comp theorem

(g : β →ₙ+* γ) (f : α →ₙ+* β) : ⇑(g.comp f) = g ∘ f

Full source

@[simp]
theorem coe_comp (g : β →ₙ+* γ) (f : α →ₙ+* β) : ⇑(g.comp f) = g ∘ f :=
  rfl

Composition of Non-unital Ring Homomorphisms Preserves Underlying Functions

Informal description

For non-unital non-associative semirings $\alpha$, $\beta$, and $\gamma$, and given non-unital ring homomorphisms $g : \beta \to \gamma$ and $f : \alpha \to \beta$, the underlying function of the composition $g \circ f$ is equal to the composition of the underlying functions of $g$ and $f$, i.e., $(g \circ f)(x) = g(f(x))$ for all $x \in \alpha$.

NonUnitalRingHom.comp_apply theorem

(g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α) : g.comp f x = g (f x)

Full source

@[simp]
theorem comp_apply (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α) : g.comp f x = g (f x) :=
  rfl

Composition of Non-unital Ring Homomorphisms Preserves Evaluation

Informal description

For non-unital non-associative semirings $\alpha$, $\beta$, and $\gamma$, given non-unital ring homomorphisms $g : \beta \to \gamma$ and $f : \alpha \to \beta$, the composition $g \circ f$ evaluated at any element $x \in \alpha$ equals $g$ applied to $f(x)$, i.e., $(g \circ f)(x) = g(f(x))$.

NonUnitalRingHom.coe_comp_addMonoidHom theorem

 (g : β →ₙ+* γ) (f : α →ₙ+* β) : AddMonoidHom.mk ⟨g ∘ f, (g.comp f).map_zero'⟩ (g.comp f).map_add' = (g : β →+ γ).comp f

Full source

@[simp]
theorem coe_comp_addMonoidHom (g : β →ₙ+* γ) (f : α →ₙ+* β) :
    AddMonoidHom.mk ⟨g ∘ f, (g.comp f).map_zero'⟩ (g.comp f).map_add' = (g : β →+ γ).comp f :=
  rfl

Compatibility of Composition with Additive Structure in Non-unital Ring Homomorphisms

Informal description

For non-unital non-associative semirings $\alpha$, $\beta$, and $\gamma$, and given non-unital ring homomorphisms $g : \beta \to \gamma$ and $f : \alpha \to \beta$, the underlying additive monoid homomorphism of the composition $g \circ f$ is equal to the composition of the underlying additive monoid homomorphisms of $g$ and $f$. More precisely, if we view $g$ and $f$ as additive monoid homomorphisms (forgetting their multiplicative structure), then the additive monoid homomorphism structure on $g \circ f$ coincides with the composition of $g$ and $f$ as additive monoid homomorphisms.

NonUnitalRingHom.coe_comp_mulHom theorem

(g : β →ₙ+* γ) (f : α →ₙ+* β) : MulHom.mk (g ∘ f) (g.comp f).map_mul' = (g : β →ₙ* γ).comp f

Full source

@[simp]
theorem coe_comp_mulHom (g : β →ₙ+* γ) (f : α →ₙ+* β) :
    MulHom.mk (g ∘ f) (g.comp f).map_mul' = (g : β →ₙ* γ).comp f :=
  rfl

Compatibility of Composition with Multiplicative Homomorphism Structure

Informal description

For non-unital non-associative semirings $\alpha$, $\beta$, and $\gamma$, given non-unital ring homomorphisms $g : \beta \to \gamma$ and $f : \alpha \to \beta$, the multiplicative homomorphism structure of their composition $g \circ f$ is equal to the composition of their multiplicative homomorphism structures. That is, $\text{MulHom.mk}(g \circ f, (g \circ f).\text{map\_mul}) = (g : \beta \to_{\text{n}*} \gamma) \circ f$.

NonUnitalRingHom.comp_zero theorem

(g : β →ₙ+* γ) : g.comp (0 : α →ₙ+* β) = 0

Full source

@[simp]
theorem comp_zero (g : β →ₙ+* γ) : g.comp (0 : α →ₙ+* β) = 0 := by
  ext
  simp

Composition with Zero Homomorphism Yields Zero Homomorphism

Informal description

For any non-unital ring homomorphism $g : \beta \to_{\text{n}+*} \gamma$ between non-unital non-associative semirings, the composition of $g$ with the zero homomorphism $0 : \alpha \to_{\text{n}+*} \beta$ is equal to the zero homomorphism $0 : \alpha \to_{\text{n}+*} \gamma$. In other words, $g \circ 0 = 0$.

NonUnitalRingHom.zero_comp theorem

(f : α →ₙ+* β) : (0 : β →ₙ+* γ).comp f = 0

Full source

@[simp]
theorem zero_comp (f : α →ₙ+* β) : (0 : β →ₙ+* γ).comp f = 0 := by
  ext
  rfl

Composition with Zero Homomorphism Yields Zero Homomorphism

Informal description

For any non-unital ring homomorphism $f \colon \alpha \to_{\text{n}+*} \beta$ between non-unital non-associative semirings $\alpha$ and $\beta$, the composition of the zero homomorphism $0 \colon \beta \to_{\text{n}+*} \gamma$ with $f$ equals the zero homomorphism $\alpha \to_{\text{n}+*} \gamma$. That is, $0 \circ f = 0$.

NonUnitalRingHom.comp_id theorem

(f : α →ₙ+* β) : f.comp (NonUnitalRingHom.id α) = f

Full source

@[simp]
theorem comp_id (f : α →ₙ+* β) : f.comp (NonUnitalRingHom.id α) = f :=
  ext fun _ => rfl

Right Identity Property of Non-unital Ring Homomorphism Composition

Informal description

For any non-unital ring homomorphism $f \colon \alpha \to_{\text{n}+*} \beta$ between non-unital non-associative semirings $\alpha$ and $\beta$, the composition of $f$ with the identity homomorphism on $\alpha$ equals $f$ itself, i.e., $f \circ \text{id}_\alpha = f$.

NonUnitalRingHom.id_comp theorem

(f : α →ₙ+* β) : (NonUnitalRingHom.id β).comp f = f

Full source

@[simp]
theorem id_comp (f : α →ₙ+* β) : (NonUnitalRingHom.id β).comp f = f :=
  ext fun _ => rfl

Identity Homomorphism Acts as Left Identity Under Composition

Informal description

For any non-unital ring homomorphism $f \colon \alpha \to_{\text{n}+*} \beta$ between non-unital non-associative semirings $\alpha$ and $\beta$, the composition of the identity homomorphism on $\beta$ with $f$ equals $f$ itself. That is, $\text{id}_\beta \circ f = f$.

NonUnitalRingHom.instMonoidWithZero instance

: MonoidWithZero (α →ₙ+* α)

Full source

instance : MonoidWithZero (α →ₙ+* α) where
  one := NonUnitalRingHom.id α
  mul := comp
  mul_one := comp_id
  one_mul := id_comp
  mul_assoc _ _ _ := comp_assoc _ _ _
  zero := 0
  mul_zero := comp_zero
  zero_mul := zero_comp

Monoid with Zero Structure on Non-unital Ring Endomorphisms

Informal description

For any non-unital non-associative semiring $\alpha$, the set of non-unital ring endomorphisms $\alpha \to_{\text{n}+*} \alpha$ forms a monoid with zero under composition, where the zero element is the constant zero function and the identity element is the identity homomorphism.

NonUnitalRingHom.one_def theorem

: (1 : α →ₙ+* α) = NonUnitalRingHom.id α

Full source

theorem one_def : (1 : α →ₙ+* α) = NonUnitalRingHom.id α :=
  rfl

Identity Homomorphism as Multiplicative Identity in Non-unital Ring Endomorphisms

Informal description

In the monoid of non-unital ring endomorphisms on a non-unital non-associative semiring $\alpha$, the multiplicative identity element $1$ is equal to the identity homomorphism $\text{id}_\alpha$.

NonUnitalRingHom.coe_one theorem

: ⇑(1 : α →ₙ+* α) = id

Full source

@[simp]
theorem coe_one : ⇑(1 : α →ₙ+* α) = id :=
  rfl

Identity Non-unital Ring Endomorphism Acts as Identity Function

Informal description

For any non-unital non-associative semiring $\alpha$, the underlying function of the multiplicative identity element in the monoid of non-unital ring endomorphisms $\alpha \to_{\text{n}+*} \alpha$ is equal to the identity function on $\alpha$.

NonUnitalRingHom.mul_def theorem

(f g : α →ₙ+* α) : f * g = f.comp g

Full source

theorem mul_def (f g : α →ₙ+* α) : f * g = f.comp g :=
  rfl

Product of Non-unital Ring Endomorphisms Equals Composition

Informal description

For any two non-unital ring endomorphisms $f, g$ on a non-unital non-associative semiring $\alpha$, the product $f * g$ is equal to the composition $f \circ g$ of the two homomorphisms.

NonUnitalRingHom.coe_mul theorem

(f g : α →ₙ+* α) : ⇑(f * g) = f ∘ g

Full source

@[simp]
theorem coe_mul (f g : α →ₙ+* α) : ⇑(f * g) = f ∘ g :=
  rfl

Composition of Non-Unital Ring Endomorphisms as Product

Informal description

For any two non-unital ring endomorphisms $f, g$ on a non-unital non-associative semiring $\alpha$, the underlying function of their product $f * g$ is equal to the composition $f \circ g$ of their underlying functions.

NonUnitalRingHom.cancel_right theorem

{g₁ g₂ : β →ₙ+* γ} {f : α →ₙ+* β} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

Full source

@[simp]
theorem cancel_right {g₁ g₂ : β →ₙ+* γ} {f : α →ₙ+* β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => ext <| hf.forall.2 (NonUnitalRingHom.ext_iff.1 h), fun h => h ▸ rfl⟩

Right Cancellation Property for Non-Unital Ring Homomorphisms under Surjective Composition

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be non-unital non-associative semirings. Given two non-unital ring homomorphisms $g_1, g_2 : \beta \to \gamma$ and a surjective non-unital ring homomorphism $f : \alpha \to \beta$, the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.

NonUnitalRingHom.cancel_left theorem

{g : β →ₙ+* γ} {f₁ f₂ : α →ₙ+* β} (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

Full source

@[simp]
theorem cancel_left {g : β →ₙ+* γ} {f₁ f₂ : α →ₙ+* β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun x => hg <| by rw [← comp_apply, h, comp_apply], fun h => h ▸ rfl⟩

Left Cancellation Property for Non-Unital Ring Homomorphisms under Injective Composition

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be non-unital non-associative semirings. Given a non-unital ring homomorphism $g : \beta \to \gamma$ that is injective, and two non-unital ring homomorphisms $f_1, f_2 : \alpha \to \beta$, the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.

RingHom structure

(α : Type*) (β : Type*) [NonAssocSemiring α] [NonAssocSemiring β] extends
  α →* β, α →+ β, α →ₙ+* β, α →*₀ β

Full source

/-- 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`. -/
structure RingHom (α : Type*) (β : Type*) [NonAssocSemiring α] [NonAssocSemiring β] extends
  α →* β, α →+ β, α →ₙ+* β, α →*₀ β

(Semi-)Ring Homomorphism

Informal description

The structure representing bundled semiring homomorphisms (also used for ring homomorphisms), which are maps between semirings (or rings) that preserve both the additive and multiplicative structures. Specifically, a ring homomorphism $f : \alpha \to \beta$ between non-associative semirings satisfies: - $f(x + y) = f(x) + f(y)$ (additive preservation) - $f(x * y) = f(x) * f(y)$ (multiplicative preservation) - $f(0) = 0$ (preservation of zero) - $f(1) = 1$ (preservation of multiplicative identity) This structure extends both monoid homomorphisms and additive monoid homomorphisms to maintain a coherent field ordering.

term_→+*_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `α →+* β` denotes the type of ring homomorphisms from `α` to `β`. -/
infixr:25 " →+* " => RingHom

Ring homomorphism notation

Informal description

The notation `α →+* β` denotes the type of ring homomorphisms from a (semi)ring `α` to a (semi)ring `β`.

RingHomClass structure

(F : Type*) (α β : outParam Type*)
    [NonAssocSemiring α] [NonAssocSemiring β] [FunLike F α β] : Prop
  extends MonoidHomClass F α β, AddMonoidHomClass F α β, MonoidWithZeroHomClass F α β

Full source

/-- `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`. -/
class RingHomClass (F : Type*) (α β : outParam Type*)
    [NonAssocSemiring α] [NonAssocSemiring β] [FunLike F α β] : Prop
  extends MonoidHomClass F α β, AddMonoidHomClass F α β, MonoidWithZeroHomClass F α β

(Semi-)Ring Homomorphism Class

Informal description

The class `RingHomClass F α β` asserts that `F` is a type of (semi)ring homomorphisms between non-associative semirings `α` and `β`. It extends `MonoidHomClass`, `AddMonoidHomClass`, and `MonoidWithZeroHomClass`, ensuring that elements of `F` preserve both the multiplicative and additive structures, including the multiplicative identity and zero elements.

RingHomClass.toRingHom definition

(f : F) : α →+* β

Full source

/-- Turn an element of a type `F` satisfying `RingHomClass F α β` into an actual
`RingHom`. This is declared as the default coercion from `F` to `α →+* β`. -/
@[coe]
def RingHomClass.toRingHom (f : F) : α →+* β :=
  { (f : α →* β), (f : α →+ β) with }

Conversion from Ring Homomorphism Class to Ring Homomorphism

Informal description

Given a type `F` satisfying `RingHomClass F α β`, this function converts an element `f : F` into an actual ring homomorphism from `α` to `β`, preserving both the additive and multiplicative structures, including the zero and multiplicative identity elements.

instCoeTCRingHom instance

: CoeTC F (α →+* β)

Full source

/-- Any type satisfying `RingHomClass` can be cast into `RingHom` via `RingHomClass.toRingHom`. -/
instance : CoeTC F (α →+* β) :=
  ⟨RingHomClass.toRingHom⟩

Canonical Coercion from Ring Homomorphism Class to Ring Homomorphisms

Informal description

For any type $F$ satisfying `RingHomClass F α β`, there is a canonical coercion from $F$ to the type of ring homomorphisms $\alpha \to+* \beta$. This means any element of $F$ can be automatically treated as a ring homomorphism preserving both the additive and multiplicative structures between non-associative semirings $\alpha$ and $\beta$.

RingHomClass.toNonUnitalRingHomClass instance

: NonUnitalRingHomClass F α β

Full source

instance (priority := 100) RingHomClass.toNonUnitalRingHomClass : NonUnitalRingHomClass F α β :=
  { ‹RingHomClass F α β› with }

(Semi-)Ring Homomorphisms as Non-Unital (Semi-)Ring Homomorphisms

Informal description

For any type $F$ representing (semi)ring homomorphisms between non-associative semirings $\alpha$ and $\beta$, the structure $F$ also satisfies the properties of non-unital (semi)ring homomorphisms. This means that every (semi)ring homomorphism preserves both the additive and multiplicative structures, including the zero element and addition, but not necessarily the multiplicative identity.

RingHom.instFunLike instance

: FunLike (α →+* β) α β

Full source

instance instFunLike : FunLike (α →+* β) α β where
  coe f := f.toFun
  coe_injective' f g h := by
    cases f
    cases g
    congr
    apply DFunLike.coe_injective'
    exact h

Function-Like Structure on Ring Homomorphisms

Informal description

For any two non-associative semirings $\alpha$ and $\beta$, the type of ring homomorphisms $\alpha \to+* \beta$ has a function-like structure, meaning each ring homomorphism can be treated as a function from $\alpha$ to $\beta$.

RingHom.instRingHomClass instance

: RingHomClass (α →+* β) α β

Full source

instance instRingHomClass : RingHomClass (α →+* β) α β where
  map_add := RingHom.map_add'
  map_zero := RingHom.map_zero'
  map_mul f := f.map_mul'
  map_one f := f.map_one'

Ring Homomorphism Class Structure

Informal description

The type of ring homomorphisms $\alpha \to+* \beta$ between non-associative semirings $\alpha$ and $\beta$ forms a class of ring homomorphisms, meaning each element preserves both the additive and multiplicative structures, including the zero and multiplicative identity elements.

RingHom.toFun_eq_coe theorem

(f : α →+* β) : f.toFun = f

Full source

theorem toFun_eq_coe (f : α →+* β) : f.toFun = f :=
  rfl

Ring homomorphism's underlying function equals its coercion

Informal description

For any ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings, the underlying function $f$ is equal to its coercion to a function.

RingHom.coe_mk theorem

(f : α →* β) (h₁ h₂) : ((⟨f, h₁, h₂⟩ : α →+* β) : α → β) = f

Full source

@[simp]
theorem coe_mk (f : α →* β) (h₁ h₂) : ((⟨f, h₁, h₂⟩ : α →+* β) : α → β) = f :=
  rfl

Ring Homomorphism Construction Preserves Underlying Function

Informal description

Given a monoid homomorphism $f \colon \alpha \to \beta$ between non-associative semirings, and proofs $h_1$ that $f$ preserves addition and $h_2$ that $f$ preserves zero, the underlying function of the constructed ring homomorphism $\langle f, h_1, h_2 \rangle \colon \alpha \to+* \beta$ is equal to $f$.

RingHom.coe_coe theorem

{F : Type*} [FunLike F α β] [RingHomClass F α β] (f : F) : ((f : α →+* β) : α → β) = f

Full source

@[simp]
theorem coe_coe {F : Type*} [FunLike F α β] [RingHomClass F α β] (f : F) :
    ((f : α →+* β) : α → β) = f :=
  rfl

Double Coercion of Ring Homomorphism Class to Function

Informal description

For any type `F` with a `FunLike` instance and a `RingHomClass` instance for non-associative semirings `α` and `β`, and for any `f : F`, the function obtained by first coercing `f` to a ring homomorphism and then to a function is equal to `f` itself as a function from `α` to `β`.

RingHom.coeToMonoidHom instance

: Coe (α →+* β) (α →* β)

Full source

instance coeToMonoidHom : Coe (α →+* β) (α →* β) :=
  ⟨RingHom.toMonoidHom⟩

Ring Homomorphism as Monoid Homomorphism

Informal description

Every ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings can be viewed as a monoid homomorphism between the multiplicative monoids of $\alpha$ and $\beta$.

RingHom.toMonoidHom_eq_coe theorem

(f : α →+* β) : f.toMonoidHom = f

Full source

@[simp]
theorem toMonoidHom_eq_coe (f : α →+* β) : f.toMonoidHom = f :=
  rfl

Ring Homomorphism as Monoid Homomorphism Equality

Informal description

For any ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings, the underlying monoid homomorphism obtained from $f$ is equal to $f$ itself when viewed as a monoid homomorphism.

RingHom.toMonoidWithZeroHom_eq_coe theorem

(f : α →+* β) : (f.toMonoidWithZeroHom : α → β) = f

Full source

theorem toMonoidWithZeroHom_eq_coe (f : α →+* β) : (f.toMonoidWithZeroHom : α → β) = f := by
  rfl

Equality of Ring Homomorphism and its Monoid-with-Zero Homomorphism Underlying Function

Informal description

For any ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings, the underlying function of the monoid-with-zero homomorphism associated to $f$ is equal to $f$ itself.

RingHom.coe_monoidHom_mk theorem

(f : α →* β) (h₁ h₂) : ((⟨f, h₁, h₂⟩ : α →+* β) : α →* β) = f

Full source

@[simp]
theorem coe_monoidHom_mk (f : α →* β) (h₁ h₂) : ((⟨f, h₁, h₂⟩ : α →+* β) : α →* β) = f :=
  rfl

Coercion of Constructed Ring Homomorphism to Monoid Homomorphism Recovers Original Map

Informal description

Let $\alpha$ and $\beta$ be non-associative semirings. Given a monoid homomorphism $f \colon \alpha \to \beta$ and proofs $h_1$, $h_2$ that $f$ preserves addition and zero, the underlying monoid homomorphism of the ring homomorphism constructed from $f$, $h_1$, and $h_2$ is equal to $f$ itself. In other words, the coercion of the constructed ring homomorphism back to a monoid homomorphism recovers the original $f$.

RingHom.toAddMonoidHom_eq_coe theorem

(f : α →+* β) : f.toAddMonoidHom = f

Full source

@[simp]
theorem toAddMonoidHom_eq_coe (f : α →+* β) : f.toAddMonoidHom = f :=
  rfl

Ring Homomorphism as Additive Monoid Homomorphism

Informal description

For any ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings, the underlying additive monoid homomorphism of $f$ is equal to $f$ itself when viewed as a function.

RingHom.coe_addMonoidHom_mk theorem

 (f : α → β) (h₁ h₂ h₃ h₄) : ((⟨⟨⟨f, h₁⟩, h₂⟩, h₃, h₄⟩ : α →+* β) : α →+ β) = ⟨⟨f, h₃⟩, h₄⟩

Full source

@[simp]
theorem coe_addMonoidHom_mk (f : α → β) (h₁ h₂ h₃ h₄) :
    ((⟨⟨⟨f, h₁⟩, h₂⟩, h₃, h₄⟩ : α →+* β) : α →+ β) = ⟨⟨f, h₃⟩, h₄⟩ :=
  rfl

Underlying Additive Homomorphism of a Ring Homomorphism Construction

Informal description

For any function $f : \alpha \to \beta$ between non-associative semirings $\alpha$ and $\beta$, and for any proofs $h_1, h_2, h_3, h_4$ of the homomorphism properties, the additive monoid homomorphism underlying the ring homomorphism $\langle \langle \langle f, h_1 \rangle, h_2 \rangle, h_3, h_4 \rangle : \alpha \to+* \beta$ is equal to the additive monoid homomorphism $\langle \langle f, h_3 \rangle, h_4 \rangle$.

RingHom.copy definition

(f : α →+* β) (f' : α → β) (h : f' = f) : α →+* β

Full source

/-- Copy of a `RingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
def copy (f : α →+* β) (f' : α → β) (h : f' = f) : α →+* β :=
  { f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }

Copy of a ring homomorphism with a new function

Informal description

Given a ring homomorphism $f \colon \alpha \to+* \beta$ and a function $f' \colon \alpha \to \beta$ that is definitionally equal to $f$, the function `RingHom.copy` constructs a new ring homomorphism with the underlying function $f'$ that preserves both the additive and multiplicative structures. This is useful for fixing definitional equalities while maintaining the homomorphism structure.

RingHom.coe_copy theorem

(f : α →+* β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f'

Full source

@[simp]
theorem coe_copy (f : α →+* β) (f' : α → β) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl

Underlying Function of Copied Ring Homomorphism Equals Input Function

Informal description

Given a ring homomorphism $f \colon \alpha \to+* \beta$ and a function $f' \colon \alpha \to \beta$ such that $f' = f$, the underlying function of the copied ring homomorphism $f.copy\ f'\ h$ is equal to $f'$.

RingHom.copy_eq theorem

(f : α →+* β) (f' : α → β) (h : f' = f) : f.copy f' h = f

Full source

theorem copy_eq (f : α →+* β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

Copy of Ring Homomorphism with Equal Function is Original

Informal description

Let $\alpha$ and $\beta$ be non-associative semirings, and let $f \colon \alpha \to+* \beta$ be a ring homomorphism. For any function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ with underlying function $f'$ is equal to $f$ itself.

RingHom.congr_fun theorem

{f g : α →+* β} (h : f = g) (x : α) : f x = g x

Full source

protected theorem congr_fun {f g : α →+* β} (h : f = g) (x : α) : f x = g x :=
  DFunLike.congr_fun h x

Pointwise Equality of Equal Ring Homomorphisms

Informal description

For any two ring homomorphisms $f, g : \alpha \to+* \beta$ between non-associative semirings, if $f = g$, then for all $x \in \alpha$, we have $f(x) = g(x)$.

RingHom.congr_arg theorem

(f : α →+* β) {x y : α} (h : x = y) : f x = f y

Full source

protected theorem congr_arg (f : α →+* β) {x y : α} (h : x = y) : f x = f y :=
  DFunLike.congr_arg f h

Ring Homomorphism Preserves Equality: $x = y \implies f(x) = f(y)$

Informal description

For any ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings $\alpha$ and $\beta$, and for any elements $x, y \in \alpha$ such that $x = y$, we have $f(x) = f(y)$.

RingHom.coe_inj theorem

⦃f g : α →+* β⦄ (h : (f : α → β) = g) : f = g

Full source

theorem coe_inj ⦃f g : α →+* β⦄ (h : (f : α → β) = g) : f = g :=
  DFunLike.coe_injective h

Injectivity of Ring Homomorphism Coercion to Functions

Informal description

For any two ring homomorphisms $f, g : \alpha \to+* \beta$ between non-associative semirings, if the underlying functions are equal (i.e., $f(x) = g(x)$ for all $x \in \alpha$), then $f = g$ as ring homomorphisms.

RingHom.ext theorem

⦃f g : α →+* β⦄ : (∀ x, f x = g x) → f = g

Full source

@[ext]
theorem ext ⦃f g : α →+* β⦄ : (∀ x, f x = g x) → f = g :=
  DFunLike.ext _ _

Extensionality of Ring Homomorphisms

Informal description

For any two ring homomorphisms $f, g : \alpha \to+* \beta$ between non-associative semirings, if $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.

RingHom.mk_coe theorem

(f : α →+* β) (h₁ h₂ h₃ h₄) : RingHom.mk ⟨⟨f, h₁⟩, h₂⟩ h₃ h₄ = f

Full source

@[simp]
theorem mk_coe (f : α →+* β) (h₁ h₂ h₃ h₄) : RingHom.mk ⟨⟨f, h₁⟩, h₂⟩ h₃ h₄ = f :=
  ext fun _ => rfl

Ring Homomorphism Construction Equals Original

Informal description

For any ring homomorphism $f : \alpha \to+* \beta$ between non-associative semirings, and for any proofs $h_1, h_2, h_3, h_4$ of the homomorphism properties, the constructed ring homomorphism `RingHom.mk ⟨⟨f, h₁⟩, h₂⟩ h₃ h₄` is equal to $f$.

RingHom.coe_addMonoidHom_injective theorem

: Injective (fun f : α →+* β => (f : α →+ β))

Full source

theorem coe_addMonoidHom_injective : Injective (fun f : α →+* β => (f : α →+ β)) := fun _ _ h =>
  ext <| DFunLike.congr_fun (F := α →+ β) h

Injectivity of Ring Homomorphism to Additive Monoid Homomorphism Map

Informal description

The canonical map from the type of ring homomorphisms $\alpha \to+* \beta$ to the type of additive monoid homomorphisms $\alpha \to+ \beta$ is injective. In other words, if two ring homomorphisms $f, g : \alpha \to+* \beta$ induce the same additive monoid homomorphism when viewed as functions, then $f = g$.

RingHom.coe_monoidHom_injective theorem

: Injective (fun f : α →+* β => (f : α →* β))

Full source

theorem coe_monoidHom_injective : Injective (fun f : α →+* β => (f : α →* β)) :=
  Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Injectivity of Ring Homomorphism to Monoid Homomorphism Coercion

Informal description

The canonical map from the type of ring homomorphisms $\alpha \to+* \beta$ to the type of monoid homomorphisms $\alpha \to* \beta$ is injective. That is, if two ring homomorphisms $f, g \colon \alpha \to+* \beta$ induce the same monoid homomorphism when viewed as multiplicative maps, then $f = g$.

RingHom.map_zero theorem

(f : α →+* β) : f 0 = 0

Full source

/-- Ring homomorphisms map zero to zero. -/
protected theorem map_zero (f : α →+* β) : f 0 = 0 :=
  map_zero f

Ring homomorphisms preserve zero

Informal description

For any ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings $\alpha$ and $\beta$, the image of the zero element is preserved, i.e., $f(0) = 0$.

RingHom.map_one theorem

(f : α →+* β) : f 1 = 1

Full source

/-- Ring homomorphisms map one to one. -/
protected theorem map_one (f : α →+* β) : f 1 = 1 :=
  map_one f

Ring homomorphisms preserve the multiplicative identity

Informal description

For any ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings $\alpha$ and $\beta$, the image of the multiplicative identity element $1$ under $f$ is again $1$, i.e., $f(1) = 1$.

RingHom.map_add theorem

(f : α →+* β) : ∀ a b, f (a + b) = f a + f b

Full source

/-- Ring homomorphisms preserve addition. -/
protected theorem map_add (f : α →+* β) : ∀ a b, f (a + b) = f a + f b :=
  map_add f

Ring Homomorphism Preserves Addition: $f(a + b) = f(a) + f(b)$

Informal description

For any ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings $\alpha$ and $\beta$, and for any elements $a, b \in \alpha$, the homomorphism preserves addition, i.e., $f(a + b) = f(a) + f(b)$.

RingHom.map_mul theorem

(f : α →+* β) : ∀ a b, f (a * b) = f a * f b

Full source

/-- Ring homomorphisms preserve multiplication. -/
protected theorem map_mul (f : α →+* β) : ∀ a b, f (a * b) = f a * f b :=
  map_mul f

Ring Homomorphism Preserves Multiplication: $f(a * b) = f(a) * f(b)$

Informal description

For any ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings $\alpha$ and $\beta$, and for any elements $a, b \in \alpha$, the homomorphism preserves multiplication, i.e., $f(a * b) = f(a) * f(b)$.

RingHom.codomain_trivial_iff_map_one_eq_zero theorem

: (0 : β) = 1 ↔ f 1 = 0

Full source

/-- `f : α →+* β` has a trivial codomain iff `f 1 = 0`. -/
theorem codomain_trivial_iff_map_one_eq_zero : (0 : β) = 1 ↔ f 1 = 0 := by rw [map_one, eq_comm]

Trivial Codomain Criterion for Ring Homomorphisms: $0 = 1 \leftrightarrow f(1) = 0$

Informal description

For a ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings, the codomain $\beta$ is trivial (i.e., $0 = 1$ in $\beta$) if and only if $f(1) = 0$.

RingHom.codomain_trivial_iff_range_trivial theorem

: (0 : β) = 1 ↔ ∀ x, f x = 0

Full source

/-- `f : α →+* β` has a trivial codomain iff it has a trivial range. -/
theorem codomain_trivial_iff_range_trivial : (0 : β) = 1 ↔ ∀ x, f x = 0 :=
  f.codomain_trivial_iff_map_one_eq_zero.trans
    ⟨fun h x => by rw [← mul_one x, map_mul, h, mul_zero], fun h => h 1⟩

Trivial Codomain Criterion for Ring Homomorphisms: $0 = 1 \leftrightarrow \text{range}(f) = \{0\}$

Informal description

For a ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings, the codomain $\beta$ is trivial (i.e., $0 = 1$ in $\beta$) if and only if the range of $f$ is trivial (i.e., $f(x) = 0$ for all $x \in \alpha$).

RingHom.map_one_ne_zero theorem

[Nontrivial β] : f 1 ≠ 0

Full source

/-- `f : α →+* β` doesn't map `1` to `0` if `β` is nontrivial -/
theorem map_one_ne_zero [Nontrivial β] : f 1 ≠ 0 :=
  mt f.codomain_trivial_iff_map_one_eq_zero.mpr zero_ne_one

Nonzero Image of Identity under Ring Homomorphisms with Nontrivial Codomain

Informal description

For any ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings, if the codomain $\beta$ is nontrivial (i.e., $0 \neq 1$ in $\beta$), then $f(1) \neq 0$.

RingHom.domain_nontrivial theorem

[Nontrivial β] : Nontrivial α

Full source

/-- If there is a homomorphism `f : α →+* β` and `β` is nontrivial, then `α` is nontrivial. -/
theorem domain_nontrivial [Nontrivial β] : Nontrivial α :=
  ⟨⟨1, 0, mt (fun h => show f 1 = 0 by rw [h, map_zero]) f.map_one_ne_zero⟩⟩

Nontriviality of Domain via Ring Homomorphism with Nontrivial Codomain

Informal description

If there exists a ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings and $\beta$ is nontrivial (i.e., $0 \neq 1$ in $\beta$), then $\alpha$ is also nontrivial.

RingHom.codomain_trivial theorem

(f : α →+* β) [h : Subsingleton α] : Subsingleton β

Full source

theorem codomain_trivial (f : α →+* β) [h : Subsingleton α] : Subsingleton β :=
  (subsingleton_or_nontrivial β).resolve_right fun _ =>
    not_nontrivial_iff_subsingleton.mpr h f.domain_nontrivial

Subsingleton Codomain via Ring Homomorphism with Subsingleton Domain

Informal description

Let $f \colon \alpha \to \beta$ be a ring homomorphism between non-associative semirings. If the domain $\alpha$ is a subsingleton (i.e., all elements of $\alpha$ are equal), then the codomain $\beta$ is also a subsingleton.

RingHom.map_neg theorem

[NonAssocRing α] [NonAssocRing β] (f : α →+* β) (x : α) : f (-x) = -f x

Full source

/-- Ring homomorphisms preserve additive inverse. -/
protected theorem map_neg [NonAssocRing α] [NonAssocRing β] (f : α →+* β) (x : α) : f (-x) = -f x :=
  map_neg f x

Ring homomorphisms preserve negation

Informal description

Let $\alpha$ and $\beta$ be non-associative rings, and let $f \colon \alpha \to \beta$ be a ring homomorphism. Then for any $x \in \alpha$, we have $f(-x) = -f(x)$.

RingHom.map_sub theorem

[NonAssocRing α] [NonAssocRing β] (f : α →+* β) (x y : α) : f (x - y) = f x - f y

Full source

/-- Ring homomorphisms preserve subtraction. -/
protected theorem map_sub [NonAssocRing α] [NonAssocRing β] (f : α →+* β) (x y : α) :
    f (x - y) = f x - f y :=
  map_sub f x y

Ring Homomorphism Preserves Subtraction

Informal description

Let $\alpha$ and $\beta$ be non-associative rings, and let $f \colon \alpha \to \beta$ be a ring homomorphism. Then for any $x, y \in \alpha$, we have $f(x - y) = f(x) - f(y)$.

RingHom.mk' definition

[NonAssocSemiring α] [NonAssocRing β] (f : α →* β) (map_add : ∀ a b, f (a + b) = f a + f b) : α →+* β

Full source

/-- Makes a ring homomorphism from a monoid homomorphism of rings which preserves addition. -/
def mk' [NonAssocSemiring α] [NonAssocRing β] (f : α →* β)
    (map_add : ∀ a b, f (a + b) = f a + f b) : α →+* β :=
  { AddMonoidHom.mk' f map_add, f with }

Ring homomorphism from monoid homomorphism preserving addition

Informal description

Given a monoid homomorphism $ f \colon \alpha \to \beta $ between non-associative semirings $\alpha$ and $\beta$ (where $\beta$ is a non-associative ring), and a proof that $ f $ preserves addition (i.e., $ f(a + b) = f(a) + f(b) $ for all $ a, b \in \alpha $), this constructs a ring homomorphism from $\alpha$ to $\beta$. The resulting ring homomorphism preserves both the multiplicative and additive structures, including the multiplicative identity and zero.

RingHom.id definition

(α : Type*) [NonAssocSemiring α] : α →+* α

Full source

/-- The identity ring homomorphism from a semiring to itself. -/
def id (α : Type*) [NonAssocSemiring α] : α →+* α where
  toFun := _root_.id
  map_zero' := rfl
  map_one' := rfl
  map_add' _ _ := rfl
  map_mul' _ _ := rfl

Identity ring homomorphism

Informal description

The identity ring homomorphism from a semiring $\alpha$ to itself, which maps each element $x \in \alpha$ to itself. This homomorphism preserves both the additive and multiplicative structures, satisfying: - $f(x + y) = f(x) + f(y)$ - $f(x \cdot y) = f(x) \cdot f(y)$ - $f(0) = 0$ - $f(1) = 1$

RingHom.instInhabited instance

: Inhabited (α →+* α)

Full source

instance : Inhabited (α →+* α) :=
  ⟨id α⟩

Inhabited Type of Ring Endomorphisms on a Non-Associative Semiring

Informal description

For any non-associative semiring $\alpha$, the type of ring homomorphisms from $\alpha$ to itself is inhabited, with the identity homomorphism as a canonical element.

RingHom.coe_id theorem

: ⇑(RingHom.id α) = _root_.id

Full source

@[simp, norm_cast]
theorem coe_id : ⇑(RingHom.id α) = _root_.id := rfl

Identity Ring Homomorphism as Identity Function

Informal description

The underlying function of the identity ring homomorphism on a non-associative semiring $\alpha$ is equal to the identity function on $\alpha$.

RingHom.id_apply theorem

(x : α) : RingHom.id α x = x

Full source

@[simp]
theorem id_apply (x : α) : RingHom.id α x = x :=
  rfl

Identity Ring Homomorphism Evaluation: $\text{id}_\alpha(x) = x$

Informal description

For any element $x$ in a non-associative semiring $\alpha$, the identity ring homomorphism $\text{id}_\alpha$ satisfies $\text{id}_\alpha(x) = x$.

RingHom.coe_addMonoidHom_id theorem

: (id α : α →+ α) = AddMonoidHom.id α

Full source

@[simp]
theorem coe_addMonoidHom_id : (id α : α →+ α) = AddMonoidHom.id α :=
  rfl

Identity Ring Homomorphism as Identity Additive Monoid Homomorphism

Informal description

The additive monoid homomorphism underlying the identity ring homomorphism on a non-associative semiring $\alpha$ is equal to the identity additive monoid homomorphism on $\alpha$.

RingHom.coe_monoidHom_id theorem

: (id α : α →* α) = MonoidHom.id α

Full source

@[simp]
theorem coe_monoidHom_id : (id α : α →* α) = MonoidHom.id α :=
  rfl

Identity Ring Homomorphism as Monoid Homomorphism: $\text{id}_\alpha = \text{MonoidHom.id}_\alpha$

Informal description

The underlying monoid homomorphism of the identity ring homomorphism on a non-associative semiring $\alpha$ is equal to the identity monoid homomorphism on $\alpha$. In other words, when viewing the identity ring homomorphism $\text{id}_\alpha$ as a monoid homomorphism, it coincides with $\text{MonoidHom.id}_\alpha$.

RingHom.comp definition

(g : β →+* γ) (f : α →+* β) : α →+* γ

Full source

/-- Composition of ring homomorphisms is a ring homomorphism. -/
def comp (g : β →+* γ) (f : α →+* β) : α →+* γ :=
  { g.toNonUnitalRingHom.comp f.toNonUnitalRingHom with toFun := g ∘ f, map_one' := by simp }

Composition of ring homomorphisms

Informal description

Given ring homomorphisms $g \colon \beta \to \gamma$ and $f \colon \alpha \to \beta$ between non-associative semirings, their composition $g \circ f \colon \alpha \to \gamma$ is again a ring homomorphism. This composition preserves both the additive and multiplicative structures, as well as the multiplicative identity (i.e., $(g \circ f)(1) = 1$).

RingHom.comp_assoc theorem

 {δ} {_ : NonAssocSemiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ) : (h.comp g).comp f = h.comp (g.comp f)

Full source

/-- Composition of semiring homomorphisms is associative. -/
theorem comp_assoc {δ} {_ : NonAssocSemiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ) :
    (h.comp g).comp f = h.comp (g.comp f) :=
  rfl

Associativity of Ring Homomorphism Composition

Informal description

For non-associative semirings $\alpha$, $\beta$, $\gamma$, and $\delta$, and ring homomorphisms $f \colon \alpha \to \beta$, $g \colon \beta \to \gamma$, and $h \colon \gamma \to \delta$, the composition of ring homomorphisms is associative, i.e., $(h \circ g) \circ f = h \circ (g \circ f)$.

RingHom.coe_comp theorem

(hnp : β →+* γ) (hmn : α →+* β) : (hnp.comp hmn : α → γ) = hnp ∘ hmn

Full source

@[simp]
theorem coe_comp (hnp : β →+* γ) (hmn : α →+* β) : (hnp.comp hmn : α → γ) = hnp ∘ hmn :=
  rfl

Composition of Ring Homomorphisms as Function Composition

Informal description

For any ring homomorphisms $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ between non-associative semirings, the underlying function of the composition $g \circ f$ is equal to the composition of the underlying functions of $g$ and $f$, i.e., $(g \circ f)(x) = g(f(x))$ for all $x \in \alpha$.

RingHom.comp_apply theorem

(hnp : β →+* γ) (hmn : α →+* β) (x : α) : (hnp.comp hmn : α → γ) x = hnp (hmn x)

Full source

theorem comp_apply (hnp : β →+* γ) (hmn : α →+* β) (x : α) :
    (hnp.comp hmn : α → γ) x = hnp (hmn x) :=
  rfl

Evaluation of Composition of Ring Homomorphisms

Informal description

For ring homomorphisms $g \colon \beta \to \gamma$ and $f \colon \alpha \to \beta$ between non-associative semirings, and for any element $x \in \alpha$, the composition $(g \circ f)(x)$ equals $g(f(x))$.

RingHom.comp_id theorem

(f : α →+* β) : f.comp (id α) = f

Full source

@[simp]
theorem comp_id (f : α →+* β) : f.comp (id α) = f :=
  ext fun _ => rfl

Right Identity Property of Ring Homomorphism Composition

Informal description

For any ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings, the composition of $f$ with the identity ring homomorphism on $\alpha$ equals $f$ itself, i.e., $f \circ \text{id}_\alpha = f$.

RingHom.id_comp theorem

(f : α →+* β) : (id β).comp f = f

Full source

@[simp]
theorem id_comp (f : α →+* β) : (id β).comp f = f :=
  ext fun _ => rfl

Identity Ring Homomorphism Acts as Left Identity for Composition

Informal description

For any ring homomorphism $f \colon \alpha \to \beta$ between non-associative semirings, the composition of the identity homomorphism on $\beta$ with $f$ equals $f$ itself, i.e., $\text{id}_\beta \circ f = f$.

RingHom.instOne instance

: One (α →+* α)

Full source

instance instOne : One (α →+* α) where one := id _

Identity Ring Homomorphism as Multiplicative Identity

Informal description

For any non-associative semiring $\alpha$, the set of ring homomorphisms from $\alpha$ to itself has a multiplicative identity given by the identity ring homomorphism.

RingHom.instMul instance

: Mul (α →+* α)

Full source

instance instMul : Mul (α →+* α) where mul := comp

Multiplication Structure on Ring Endomorphisms via Composition

Informal description

For any non-associative semiring $\alpha$, the set of ring homomorphisms from $\alpha$ to itself forms a multiplicative structure where multiplication is given by composition of homomorphisms.

RingHom.one_def theorem

: (1 : α →+* α) = id α

Full source

lemma one_def : (1 : α →+* α) = id α := rfl

Identity Ring Homomorphism as One

Informal description

The multiplicative identity element in the semiring of ring endomorphisms on a non-associative semiring $\alpha$ is equal to the identity ring homomorphism, i.e., $1 = \text{id}_\alpha$.

RingHom.mul_def theorem

(f g : α →+* α) : f * g = f.comp g

Full source

lemma mul_def (f g : α →+* α) : f * g = f.comp g := rfl

Product of Ring Endomorphisms is Composition

Informal description

For any ring homomorphisms $f, g \colon \alpha \to \alpha$ (where $\alpha$ is a non-associative semiring), the product $f * g$ is equal to the composition $f \circ g$ of the homomorphisms.

RingHom.coe_one theorem

: ⇑(1 : α →+* α) = _root_.id

Full source

@[simp, norm_cast] lemma coe_one : ⇑(1 : α →+* α) = _root_.id := rfl

Identity Ring Homomorphism as Identity Function

Informal description

For any non-associative semiring $\alpha$, the underlying function of the identity ring homomorphism $1 : \alpha \to+* \alpha$ is equal to the identity function $\mathrm{id} : \alpha \to \alpha$.

RingHom.coe_mul theorem

(f g : α →+* α) : ⇑(f * g) = f ∘ g

Full source

@[simp, norm_cast] lemma coe_mul (f g : α →+* α) : ⇑(f * g) = f ∘ g := rfl

Composition of Ring Endomorphisms as Multiplication

Informal description

For any ring homomorphisms $f, g : \alpha \to+* \alpha$ between non-associative semirings, the underlying function of their product $f * g$ is equal to the composition $f \circ g$ of the underlying functions.

RingHom.instMonoid instance

: Monoid (α →+* α)

Full source

instance instMonoid : Monoid (α →+* α) where
  mul_one := comp_id
  one_mul := id_comp
  mul_assoc _ _ _ := comp_assoc _ _ _
  npow n f := (npowRec n f).copy f^[n] <| by induction n <;> simp [npowRec, *]
  npow_succ _ _ := DFunLike.coe_injective <| Function.iterate_succ _ _

Monoid Structure on Ring Endomorphisms via Composition

Informal description

For any non-associative semiring $\alpha$, the set of ring endomorphisms $\alpha \to+* \alpha$ forms a monoid under composition, where the identity element is the identity ring homomorphism and multiplication is given by composition of homomorphisms.

RingHom.coe_pow theorem

(f : α →+* α) (n : ℕ) : ⇑(f ^ n) = f^[n]

Full source

@[simp, norm_cast] lemma coe_pow (f : α →+* α) (n : ℕ) : ⇑(f ^ n) = f^[n] := rfl

Iteration of Ring Endomorphism via Composition Power: $f^n = f^{\circ n}$

Informal description

For any ring endomorphism $f \colon \alpha \to \alpha$ and any natural number $n$, the underlying function of the $n$-th power of $f$ (under composition) is equal to the $n$-th iterate of $f$, i.e., $(f^n)(x) = f^[n](x) = f(f(\cdots f(x)\cdots))$ (composed $n$ times).

RingHom.cancel_right theorem

{g₁ g₂ : β →+* γ} {f : α →+* β} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

Full source

@[simp]
theorem cancel_right {g₁ g₂ : β →+* γ} {f : α →+* β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => RingHom.ext <| hf.forall.2 (RingHom.ext_iff.1 h), fun h => h ▸ rfl⟩

Right Cancellation Property for Composition of Ring Homomorphisms with Surjective Map

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be non-associative semirings. Given ring homomorphisms $g_1, g_2 \colon \beta \to \gamma$ and a surjective ring homomorphism $f \colon \alpha \to \beta$, the compositions $g_1 \circ f$ and $g_2 \circ f$ are equal if and only if $g_1 = g_2$.

RingHom.cancel_left theorem

{g : β →+* γ} {f₁ f₂ : α →+* β} (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

Full source

@[simp]
theorem cancel_left {g : β →+* γ} {f₁ f₂ : α →+* β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => RingHom.ext fun x => hg <| by rw [← comp_apply, h, comp_apply], fun h => h ▸ rfl⟩

Left Cancellation Property for Composition of Ring Homomorphisms with Injective Map

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be non-associative semirings. Given ring homomorphisms $f_1, f_2 \colon \alpha \to \beta$ and an injective ring homomorphism $g \colon \beta \to \gamma$, the compositions $g \circ f_1$ and $g \circ f_2$ are equal if and only if $f_1 = f_2$.

RingHom.map_pow theorem

(f : α →+* β) (a) : ∀ n : ℕ, f (a ^ n) = f a ^ n

Full source

protected lemma RingHom.map_pow (f : α →+* β) (a) : ∀ n : ℕ, f (a ^ n) = f a ^ n := map_pow f a

Power Preservation under Ring Homomorphisms: $f(a^n) = f(a)^n$

Informal description

Let $\alpha$ and $\beta$ be semirings and let $f : \alpha \to \beta$ be a ring homomorphism. For any element $a \in \alpha$ and any natural number $n$, we have $f(a^n) = (f(a))^n$.

AddMonoidHom.mkRingHomOfMulSelfOfTwoNeZero definition

(h : ∀ x, f (x * x) = f x * f x) (h_two : (2 : α) ≠ 0) (h_one : f 1 = 1) : β →+* α

Full source

/-- 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`. -/
def mkRingHomOfMulSelfOfTwoNeZero (h : ∀ x, f (x * x) = f x * f x) (h_two : (2 : α) ≠ 0)
    (h_one : f 1 = 1) : β →+* α :=
  { f with
    map_one' := h_one,
    map_mul' := fun x y => by
      have hxy := h (x + y)
      rw [mul_add, add_mul, add_mul, f.map_add, f.map_add, f.map_add, f.map_add, h x, h y, add_mul,
        mul_add, mul_add, ← sub_eq_zero, add_comm (f x * f x + f (y * x)), ← sub_sub, ← sub_sub,
        ← sub_sub, mul_comm y x, mul_comm (f y) (f x)] at hxy
      simp only [add_assoc, add_sub_assoc, add_sub_cancel] at hxy
      rw [sub_sub, ← two_mul, ← add_sub_assoc, ← two_mul, ← mul_sub, mul_eq_zero (M₀ := α),
        sub_eq_zero, or_iff_not_imp_left] at hxy
      exact hxy h_two }

Ring homomorphism from self-multiplicative additive homomorphism with $2 \neq 0$ condition

Informal description

Given an additive group homomorphism $f$ from a commutative ring $\alpha$ to an integral domain $\beta$ that commutes with self-multiplication (i.e., $f(x^2) = f(x)^2$ for all $x \in \alpha$), and assuming that $2 \neq 0$ in $\alpha$ and $f(1) = 1$, then $f$ can be extended to a ring homomorphism from $\alpha$ to $\beta$.

AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero theorem

(h h_two h_one) : (f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one : β → α) = f

Full source

@[simp]
theorem coe_fn_mkRingHomOfMulSelfOfTwoNeZero (h h_two h_one) :
    (f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one : β → α) = f :=
  rfl

Coincidence of Underlying Function in Ring Homomorphism Construction from Self-Multiplicative Additive Homomorphism

Informal description

Let $f : \alpha \to \beta$ be an additive group homomorphism from a commutative ring $\alpha$ to an integral domain $\beta$ satisfying $f(x^2) = f(x)^2$ for all $x \in \alpha$. If $2 \neq 0$ in $\alpha$ and $f(1) = 1$, then the underlying function of the ring homomorphism constructed from $f$ via `mkRingHomOfMulSelfOfTwoNeZero` coincides with $f$ itself. That is, for all $x \in \alpha$, we have $f(x) = f.mkRingHomOfMulSelfOfTwoNeZero(h, h_{two}, h_{one})(x)$.

AddMonoidHom.coe_addMonoidHom_mkRingHomOfMulSelfOfTwoNeZero theorem

(h h_two h_one) : (f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one : β →+ α) = f

Full source

@[simp]
theorem coe_addMonoidHom_mkRingHomOfMulSelfOfTwoNeZero (h h_two h_one) :
    (f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one : β →+ α) = f := by
  ext
  rfl

Additive Structure Preservation in Ring Homomorphism Construction from Self-Multiplicative Homomorphism

Informal description

Let $f : \alpha \to \beta$ be an additive group homomorphism from a commutative ring $\alpha$ to an integral domain $\beta$ satisfying $f(x^2) = f(x)^2$ for all $x \in \alpha$. If $2 \neq 0$ in $\alpha$ and $f(1) = 1$, then the underlying additive group homomorphism of the ring homomorphism constructed from $f$ via `mkRingHomOfMulSelfOfTwoNeZero` coincides with $f$ itself. That is, the additive structure of the constructed ring homomorphism is identical to $f$.

Mathlib.Algebra.Ring.Hom.Defs

Main definitions

Notations

Implementation notes

Tags