doc-next-gen

Mathlib.Algebra.Algebra.Hom

Module docstring

{"# Homomorphisms of R-algebras

This file defines bundled homomorphisms of R-algebras.

Main definitions

  • AlgHom R A B: the type of R-algebra morphisms from A to B.
  • Algebra.ofId R A : R →ₐ[R] A: the canonical map from R to A, as an AlgHom.

Notations

  • A →ₐ[R] B : R-algebra homomorphism from A to B. "}
AlgHom structure
(R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] extends RingHom A B
Full source 
/-- Defining the homomorphism in the category R-Alg, denoted `A →ₐ[R] B`. -/
structure AlgHom (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Semiring B]
  [Algebra R A] [Algebra R B] extends RingHom A B where
  commutes' : ∀ r : R, toFun (algebraMap R A r) = algebraMap R B r
\( R \)-Algebra Homomorphism
Informal description
The structure representing bundled homomorphisms of \( R \)-algebras, denoted \( A \to_{R} B \), where \( R \) is a commutative semiring and \( A, B \) are semirings equipped with an \( R \)-algebra structure. An \( R \)-algebra homomorphism is a ring homomorphism that additionally preserves the action of \( R \).
term_→ₐ_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc AlgHom]
infixr:25 " →ₐ " => AlgHom _
Notation for R-algebra homomorphisms
Informal description
The notation `A →ₐ[R] B` represents the type of `R`-algebra homomorphisms from `A` to `B`, where `R` is a commutative semiring and `A`, `B` are semirings equipped with an `R`-algebra structure.
term_→ₐ[_]_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc]
notation:25 A " →ₐ[" R "] " B => AlgHom R A B
`R`-algebra homomorphism notation
Informal description
The notation `A →ₐ[R] B` represents the type of `R`-algebra homomorphisms from `A` to `B`, where `R` is a commutative (semi)ring and `A` and `B` are `R`-algebras. An `R`-algebra homomorphism is a map that preserves both the ring structure and the scalar multiplication by elements of `R`.
Algebra.algHom definition
(R A B : Type*) [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : A →ₐ[R] B
Full source 
/-- The algebra morphism underlying `algebraMap` -/
def Algebra.algHom (R A B : Type*)
    [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B]
    [Algebra A B] [IsScalarTower R A B] :
    A →ₐ[R] B where
  toRingHom := algebraMap A B
  commutes' r := by simpa [Algebra.smul_def] using smul_assoc r (1 : A) (1 : B)
Canonical \( R \)-algebra homomorphism from \( A \) to \( B \) under scalar multiplication tower property
Informal description
Given commutative semirings \( R \) and \( A \), and a semiring \( B \), all equipped with \( R \)-algebra structures, and assuming that \( A \) is also an \( R \)-algebra and \( B \) is an \( A \)-algebra with the scalar multiplication tower property (i.e., the scalar multiplication of \( R \) on \( B \) factors through \( A \)), the canonical \( R \)-algebra homomorphism from \( A \) to \( B \) is defined by the algebra map \( A \to B \). This map is a ring homomorphism that commutes with the action of \( R \), satisfying \( \varphi(r \cdot a) = r \cdot \varphi(a) \) for all \( r \in R \) and \( a \in A \).
AlgHomClass structure
(F : Type*) (R A B : outParam Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FunLike F A B] : Prop extends RingHomClass F A B
Full source 
/-- `AlgHomClass F R A B` asserts `F` is a type of bundled algebra homomorphisms
from `A` to `B`. -/
class AlgHomClass (F : Type*) (R A B : outParam Type*)
    [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FunLike F A B] : Prop
    extends RingHomClass F A B where
  commutes : ∀ (f : F) (r : R), f (algebraMap R A r) = algebraMap R B r
Algebra Homomorphism Class
Informal description
The class `AlgHomClass F R A B` asserts that `F` is a type of bundled algebra homomorphisms from `A` to `B`, where `R` is a commutative semiring and `A`, `B` are semirings equipped with an `R`-algebra structure. It extends `RingHomClass F A B`, meaning that elements of `F` are ring homomorphisms that additionally preserve the `R`-algebra structure.
AlgHomClass.linearMapClass instance
[AlgHomClass F R A B] : LinearMapClass F R A B
Full source 
instance (priority := 100) linearMapClass [AlgHomClass F R A B] : LinearMapClass F R A B :=
  { ‹AlgHomClass F R A B› with
    map_smulₛₗ := fun f r x => by
      simp only [Algebra.smul_def, map_mul, commutes, RingHom.id_apply] }
Algebra Homomorphisms are Linear Maps
Informal description
For any commutative semiring $R$ and semirings $A$, $B$ equipped with $R$-algebra structures, every $R$-algebra homomorphism from $A$ to $B$ is also an $R$-linear map.
AlgHomClass.toAlgHom definition
{F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : A →ₐ[R] B
Full source 
/-- Turn an element of a type `F` satisfying `AlgHomClass F α β` into an actual
`AlgHom`. This is declared as the default coercion from `F` to `α →+* β`. -/
@[coe]
def toAlgHom {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : A →ₐ[R] B where
  __ := (f : A →+* B)
  toFun := f
  commutes' := AlgHomClass.commutes f
Conversion from algebra homomorphism class to algebra homomorphism
Informal description
Given a type `F` satisfying `AlgHomClass F R A B`, this function converts an element `f : F` into an actual `R`-algebra homomorphism from `A` to `B`, preserving both the ring structure and the action of `R`. Specifically, it ensures that `f` is a ring homomorphism and that it commutes with the scalar multiplication by elements of `R`.
AlgHomClass.coeTC instance
{F : Type*} [FunLike F A B] [AlgHomClass F R A B] : CoeTC F (A →ₐ[R] B)
Full source 
instance coeTC {F : Type*} [FunLike F A B] [AlgHomClass F R A B] : CoeTC F (A →ₐ[R] B) :=
  ⟨AlgHomClass.toAlgHom⟩
Canonical Coercion from Algebra Homomorphism Class to Algebra Homomorphisms
Informal description
For any commutative semiring $R$, semirings $A$ and $B$ equipped with $R$-algebra structures, and any type $F$ that is a function-like class of $R$-algebra homomorphisms from $A$ to $B$, there is a canonical coercion from $F$ to the type of $R$-algebra homomorphisms $A \to_{R} B$.
AlgHom.funLike instance
: FunLike (A →ₐ[R] B) A B
Full source 
instance funLike : FunLike (A →ₐ[R] B) A B where
  coe f := f.toFun
  coe_injective' f g h := by
    rcases f with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
    rcases g with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
    congr
Function-Like Structure of $R$-Algebra Homomorphisms
Informal description
For any commutative semiring $R$ and semirings $A$, $B$ equipped with $R$-algebra structures, the type of $R$-algebra homomorphisms $A \to_{R} B$ is a function-like class, meaning it can be coerced to a function from $A$ to $B$ in a canonical way.
AlgHom.algHomClass instance
: AlgHomClass (A →ₐ[R] B) R A B
Full source 
instance algHomClass : AlgHomClass (A →ₐ[R] B) R A B where
  map_add f := f.map_add'
  map_zero f := f.map_zero'
  map_mul f := f.map_mul'
  map_one f := f.map_one'
  commutes f := f.commutes'
$R$-Algebra Homomorphism Class Structure
Informal description
The type of $R$-algebra homomorphisms $A \to_{R} B$ forms an `AlgHomClass`, meaning it inherits the properties of a ring homomorphism class while additionally preserving the $R$-algebra structure.
AlgHom.Simps.apply definition
{R : Type u} {α : Type v} {β : Type w} [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α →ₐ[R] β) : α → β
Full source 
/-- See Note [custom simps projection] -/
def Simps.apply {R : Type u} {α : Type v} {β : Type w} [CommSemiring R]
    [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α →ₐ[R] β) : α → β := f
Underlying map of an $R$-algebra homomorphism
Informal description
The function that extracts the underlying map from an $R$-algebra homomorphism $f : \alpha \to_{R} \beta$, where $R$ is a commutative semiring and $\alpha, \beta$ are semirings equipped with $R$-algebra structures. This map sends an element $x \in \alpha$ to its image $f(x) \in \beta$.
AlgHom.coe_coe theorem
{F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : ⇑(f : A →ₐ[R] B) = f
Full source 
@[simp]
protected theorem coe_coe {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) :
    ⇑(f : A →ₐ[R] B) = f :=
  rfl
Coercion Consistency for Algebra Homomorphisms
Informal description
For any type `F` equipped with a function-like structure `FunLike F A B` and an algebra homomorphism class `AlgHomClass F R A B`, the underlying function of the algebra homomorphism `f : A →ₐ[R] B` obtained from `f : F` is equal to `f` itself. In other words, the coercion of `f` to a function coincides with `f` as a function from `A` to `B`.
AlgHom.toFun_eq_coe theorem
(f : A →ₐ[R] B) : f.toFun = f
Full source 
@[simp]
theorem toFun_eq_coe (f : A →ₐ[R] B) : f.toFun = f :=
  rfl
Equality of Underlying Function and Coercion for $R$-Algebra Homomorphisms
Informal description
For any $R$-algebra homomorphism $f \colon A \to_{R} B$, the underlying function $f$ is equal to its coercion to a function from $A$ to $B$.
AlgHom.toMonoidHom' definition
(f : A →ₐ[R] B) : A →* B
Full source 
@[coe]
def toMonoidHom' (f : A →ₐ[R] B) : A →* B := (f : A →+* B)
Underlying monoid homomorphism of an \( R \)-algebra homomorphism
Informal description
Given an \( R \)-algebra homomorphism \( f \colon A \to_{R} B \), this function returns the underlying monoid homomorphism from \( A \) to \( B \), preserving the multiplicative structure and the identity element.
AlgHom.coeOutMonoidHom instance
: CoeOut (A →ₐ[R] B) (A →* B)
Full source 
instance coeOutMonoidHom : CoeOut (A →ₐ[R] B) (A →* B) :=
  ⟨AlgHom.toMonoidHom'⟩
$R$-Algebra Homomorphism as Monoid Homomorphism
Informal description
Every $R$-algebra homomorphism $f \colon A \to_{R} B$ can be viewed as a monoid homomorphism from $A$ to $B$ by forgetting the $R$-algebra structure.
AlgHom.toAddMonoidHom' definition
(f : A →ₐ[R] B) : A →+ B
Full source 
@[coe]
def toAddMonoidHom' (f : A →ₐ[R] B) : A →+ B := (f : A →+* B)
Underlying additive monoid homomorphism of an $R$-algebra homomorphism
Informal description
Given an $R$-algebra homomorphism $f \colon A \to_{R} B$, this function returns the underlying additive monoid homomorphism from $A$ to $B$, which preserves the additive structure (including zero and addition).
AlgHom.coeOutAddMonoidHom instance
: CoeOut (A →ₐ[R] B) (A →+ B)
Full source 
instance coeOutAddMonoidHom : CoeOut (A →ₐ[R] B) (A →+ B) :=
  ⟨AlgHom.toAddMonoidHom'⟩
Additive Monoid Homomorphism Structure on $R$-Algebra Homomorphisms
Informal description
Every $R$-algebra homomorphism $f \colon A \to_{R} B$ can be viewed as an additive monoid homomorphism from $A$ to $B$, preserving the additive structure (including zero and addition).
AlgHom.coe_mk theorem
{f : A →+* B} (h) : ((⟨f, h⟩ : A →ₐ[R] B) : A → B) = f
Full source 
@[simp]
theorem coe_mk {f : A →+* B} (h) : ((⟨f, h⟩ : A →ₐ[R] B) : A → B) = f :=
  rfl
Underlying Function of Bundled $R$-Algebra Homomorphism
Informal description
Given a ring homomorphism $f \colon A \to+* B$ and a proof $h$ that $f$ is an $R$-algebra homomorphism, the underlying function of the bundled $R$-algebra homomorphism $\langle f, h \rangle \colon A \to_{R} B$ is equal to $f$.
AlgHom.coe_mks theorem
{f : A → B} (h₁ h₂ h₃ h₄ h₅) : ⇑(⟨⟨⟨⟨f, h₁⟩, h₂⟩, h₃, h₄⟩, h₅⟩ : A →ₐ[R] B) = f
Full source 
@[norm_cast]
theorem coe_mks {f : A → B} (h₁ h₂ h₃ h₄ h₅) : ⇑(⟨⟨⟨⟨f, h₁⟩, h₂⟩, h₃, h₄⟩, h₅⟩ : A →ₐ[R] B) = f :=
  rfl
Coercion of Constructed $R$-Algebra Homomorphism Equals Original Function
Informal description
Given a function $f: A \to B$ and proofs $h_1, h_2, h_3, h_4, h_5$ that $f$ preserves the $R$-algebra structure, the underlying function of the $R$-algebra homomorphism constructed from $f$ and these proofs is equal to $f$ itself. In other words, the coercion of the bundled homomorphism $\langle \langle \langle \langle f, h_1 \rangle, h_2 \rangle, h_3, h_4 \rangle, h_5 \rangle : A \to_{R} B$ to a function $A \to B$ is exactly $f$.
AlgHom.coe_ringHom_mk theorem
{f : A →+* B} (h) : ((⟨f, h⟩ : A →ₐ[R] B) : A →+* B) = f
Full source 
@[simp, norm_cast]
theorem coe_ringHom_mk {f : A →+* B} (h) : ((⟨f, h⟩ : A →ₐ[R] B) : A →+* B) = f :=
  rfl
Underlying Ring Homomorphism of Bundled $R$-Algebra Homomorphism Equals Original
Informal description
Given a ring homomorphism $f \colon A \to+* B$ and a proof $h$ that $f$ preserves the $R$-algebra structure, the underlying ring homomorphism of the bundled $R$-algebra homomorphism $\langle f, h \rangle \colon A \to_{R} B$ is equal to $f$ itself.
AlgHom.toRingHom_eq_coe theorem
(f : A →ₐ[R] B) : f.toRingHom = f
Full source 
@[simp]
theorem toRingHom_eq_coe (f : A →ₐ[R] B) : f.toRingHom = f :=
  rfl
Equality of Underlying Ring Homomorphism and $R$-Algebra Homomorphism
Informal description
For any $R$-algebra homomorphism $f \colon A \to_{R} B$, the underlying ring homomorphism obtained from $f$ is equal to $f$ itself when viewed as a function.
AlgHom.coe_toRingHom theorem
(f : A →ₐ[R] B) : ⇑(f : A →+* B) = f
Full source 
@[simp, norm_cast]
theorem coe_toRingHom (f : A →ₐ[R] B) : ⇑(f : A →+* B) = f :=
  rfl
Underlying Function of Ring Homomorphism Associated to $R$-Algebra Homomorphism
Informal description
For any $R$-algebra homomorphism $f \colon A \to_{R} B$, the underlying function of the associated ring homomorphism $f \colon A \to+* B$ is equal to $f$ itself.
AlgHom.coe_toMonoidHom theorem
(f : A →ₐ[R] B) : ⇑(f : A →* B) = f
Full source 
@[simp, norm_cast]
theorem coe_toMonoidHom (f : A →ₐ[R] B) : ⇑(f : A →* B) = f :=
  rfl
Underlying Monoid Homomorphism of an $R$-Algebra Homomorphism
Informal description
For any $R$-algebra homomorphism $f \colon A \to_{R} B$, the underlying monoid homomorphism of $f$ is equal to $f$ itself when viewed as a function from $A$ to $B$.
AlgHom.coe_toAddMonoidHom theorem
(f : A →ₐ[R] B) : ⇑(f : A →+ B) = f
Full source 
@[simp, norm_cast]
theorem coe_toAddMonoidHom (f : A →ₐ[R] B) : ⇑(f : A →+ B) = f :=
  rfl
Underlying Additive Monoid Homomorphism of an $R$-Algebra Homomorphism
Informal description
For any $R$-algebra homomorphism $f \colon A \to_{R} B$, the underlying additive monoid homomorphism of $f$ (viewed as a function) is equal to $f$ itself.
AlgHom.toRingHom_toMonoidHom theorem
(f : A →ₐ[R] B) : ((f : A →+* B) : A →* B) = f
Full source 
@[simp]
theorem toRingHom_toMonoidHom (f : A →ₐ[R] B) : ((f : A →+* B) : A →* B) = f :=
  rfl
Coercion Consistency for $R$-Algebra Homomorphisms: Ring to Monoid Homomorphism
Informal description
For any $R$-algebra homomorphism $f \colon A \to_{R} B$, the underlying monoid homomorphism obtained by first coercing $f$ to a ring homomorphism and then to a monoid homomorphism is equal to $f$ itself.
AlgHom.toRingHom_toAddMonoidHom theorem
(f : A →ₐ[R] B) : ((f : A →+* B) : A →+ B) = f
Full source 
@[simp]
theorem toRingHom_toAddMonoidHom (f : A →ₐ[R] B) : ((f : A →+* B) : A →+ B) = f :=
  rfl
Compatibility of $R$-Algebra Homomorphism with Underlying Additive Structure
Informal description
For any $R$-algebra homomorphism $f \colon A \to_{R} B$, the underlying additive monoid homomorphism obtained by first viewing $f$ as a ring homomorphism and then as an additive monoid homomorphism is equal to $f$ itself.
AlgHom.coe_fn_injective theorem
: @Function.Injective (A →ₐ[R] B) (A → B) (↑)
Full source 
theorem coe_fn_injective : @Function.Injective (A →ₐ[R] B) (A → B) (↑) :=
  DFunLike.coe_injective
Injectivity of Coercion for $R$-Algebra Homomorphisms
Informal description
The canonical coercion from $R$-algebra homomorphisms $A \to_{R} B$ to functions $A \to B$ is injective. That is, if two $R$-algebra homomorphisms $f, g \colon A \to_{R} B$ satisfy $f(x) = g(x)$ for all $x \in A$, then $f = g$.
AlgHom.coe_fn_inj theorem
{φ₁ φ₂ : A →ₐ[R] B} : (φ₁ : A → B) = φ₂ ↔ φ₁ = φ₂
Full source 
theorem coe_fn_inj {φ₁ φ₂ : A →ₐ[R] B} : (φ₁ : A → B) = φ₂ ↔ φ₁ = φ₂ :=
  DFunLike.coe_fn_eq
Equality of $R$-Algebra Homomorphisms via Function Equality
Informal description
For any two $R$-algebra homomorphisms $\phi_1, \phi_2: A \to_{R} B$, the underlying functions $\phi_1$ and $\phi_2$ are equal if and only if $\phi_1 = \phi_2$ as $R$-algebra homomorphisms.
AlgHom.coe_ringHom_injective theorem
: Function.Injective ((↑) : (A →ₐ[R] B) → A →+* B)
Full source 
theorem coe_ringHom_injective : Function.Injective ((↑) : (A →ₐ[R] B) → A →+* B) := fun φ₁ φ₂ H =>
  coe_fn_injective <| show ((φ₁ : A →+* B) : A → B) = ((φ₂ : A →+* B) : A → B) from congr_arg _ H
Injectivity of the Ring Homomorphism Coercion from $R$-Algebra Homomorphisms
Informal description
The canonical map from $R$-algebra homomorphisms $A \to_{R} B$ to ring homomorphisms $A \to+* B$ is injective. That is, if two $R$-algebra homomorphisms $\phi_1, \phi_2 \colon A \to_{R} B$ induce the same ring homomorphism when coerced, then $\phi_1 = \phi_2$.
AlgHom.coe_monoidHom_injective theorem
: Function.Injective ((↑) : (A →ₐ[R] B) → A →* B)
Full source 
theorem coe_monoidHom_injective : Function.Injective ((↑) : (A →ₐ[R] B) → A →* B) :=
  RingHom.coe_monoidHom_injective.comp coe_ringHom_injective
Injectivity of the Monoid Homomorphism Coercion from $R$-Algebra Homomorphisms
Informal description
The canonical map from $R$-algebra homomorphisms $A \to_{R} B$ to monoid homomorphisms $A \to* B$ is injective. That is, if two $R$-algebra homomorphisms $\phi_1, \phi_2 \colon A \to_{R} B$ induce the same monoid homomorphism when coerced, then $\phi_1 = \phi_2$.
AlgHom.coe_addMonoidHom_injective theorem
: Function.Injective ((↑) : (A →ₐ[R] B) → A →+ B)
Full source 
theorem coe_addMonoidHom_injective : Function.Injective ((↑) : (A →ₐ[R] B) → A →+ B) :=
  RingHom.coe_addMonoidHom_injective.comp coe_ringHom_injective
Injectivity of the Additive Monoid Homomorphism Coercion from $R$-Algebra Homomorphisms
Informal description
The canonical map from $R$-algebra homomorphisms $A \to_{R} B$ to additive monoid homomorphisms $A \to+ B$ is injective. That is, if two $R$-algebra homomorphisms $\phi_1, \phi_2 \colon A \to_{R} B$ induce the same additive monoid homomorphism when coerced, then $\phi_1 = \phi_2$.
AlgHom.congr_fun theorem
{φ₁ φ₂ : A →ₐ[R] B} (H : φ₁ = φ₂) (x : A) : φ₁ x = φ₂ x
Full source 
protected theorem congr_fun {φ₁ φ₂ : A →ₐ[R] B} (H : φ₁ = φ₂) (x : A) : φ₁ x = φ₂ x :=
  DFunLike.congr_fun H x
Pointwise Equality of $R$-Algebra Homomorphisms
Informal description
For any two $R$-algebra homomorphisms $\phi_1, \phi_2: A \to_{R} B$, if $\phi_1 = \phi_2$, then $\phi_1(x) = \phi_2(x)$ for all $x \in A$.
AlgHom.congr_arg theorem
(φ : A →ₐ[R] B) {x y : A} (h : x = y) : φ x = φ y
Full source 
protected theorem congr_arg (φ : A →ₐ[R] B) {x y : A} (h : x = y) : φ x = φ y :=
  DFunLike.congr_arg φ h
$R$-Algebra Homomorphism Preserves Equality: $\varphi(x) = \varphi(y)$ when $x = y$
Informal description
For any $R$-algebra homomorphism $\varphi : A \to_{R} B$ and elements $x, y \in A$, if $x = y$, then $\varphi(x) = \varphi(y)$.
AlgHom.ext theorem
{φ₁ φ₂ : A →ₐ[R] B} (H : ∀ x, φ₁ x = φ₂ x) : φ₁ = φ₂
Full source 
@[ext]
theorem ext {φ₁ φ₂ : A →ₐ[R] B} (H : ∀ x, φ₁ x = φ₂ x) : φ₁ = φ₂ :=
  DFunLike.ext _ _ H
Extensionality of $R$-algebra homomorphisms
Informal description
For any two $R$-algebra homomorphisms $\phi_1, \phi_2 \colon A \to_{R} B$, if $\phi_1(x) = \phi_2(x)$ for all $x \in A$, then $\phi_1 = \phi_2$.
AlgHom.mk_coe theorem
{f : A →ₐ[R] B} (h₁ h₂ h₃ h₄ h₅) : (⟨⟨⟨⟨f, h₁⟩, h₂⟩, h₃, h₄⟩, h₅⟩ : A →ₐ[R] B) = f
Full source 
@[simp]
theorem mk_coe {f : A →ₐ[R] B} (h₁ h₂ h₃ h₄ h₅) : (⟨⟨⟨⟨f, h₁⟩, h₂⟩, h₃, h₄⟩, h₅⟩ : A →ₐ[R] B) = f :=
  rfl
Constructed $R$-Algebra Homomorphism Equals Original
Informal description
Given an $R$-algebra homomorphism $f \colon A \to_{R} B$ and proofs $h_1, h_2, h_3, h_4, h_5$ of the homomorphism properties, the constructed homomorphism $\langle \langle \langle \langle f, h_1 \rangle, h_2 \rangle, h_3, h_4 \rangle, h_5 \rangle$ is equal to $f$.
AlgHom.commutes theorem
(r : R) : φ (algebraMap R A r) = algebraMap R B r
Full source 
@[simp]
theorem commutes (r : R) : φ (algebraMap R A r) = algebraMap R B r :=
  φ.commutes' r
Commutativity of $R$-algebra homomorphisms with algebra maps
Informal description
For any $R$-algebra homomorphism $\varphi \colon A \to_{R} B$ and any element $r \in R$, the homomorphism $\varphi$ commutes with the algebra maps, i.e., $\varphi(\text{algebraMap}_R^A(r)) = \text{algebraMap}_R^B(r)$.
AlgHom.comp_algebraMap theorem
: (φ : A →+* B).comp (algebraMap R A) = algebraMap R B
Full source 
theorem comp_algebraMap : (φ : A →+* B).comp (algebraMap R A) = algebraMap R B :=
  RingHom.ext <| φ.commutes
Composition of Ring Homomorphism with Algebra Map Preserves Canonical Map
Informal description
For any ring homomorphism $\varphi \colon A \to B$ between $R$-algebras, the composition of $\varphi$ with the canonical algebra map $\text{algebraMap}_R^A \colon R \to A$ equals the canonical algebra map $\text{algebraMap}_R^B \colon R \to B$. That is, $\varphi \circ \text{algebraMap}_R^A = \text{algebraMap}_R^B$.
AlgHom.mk' definition
(f : A →+* B) (h : ∀ (c : R) (x), f (c • x) = c • f x) : A →ₐ[R] B
Full source 
/-- If a `RingHom` is `R`-linear, then it is an `AlgHom`. -/
def mk' (f : A →+* B) (h : ∀ (c : R) (x), f (c • x) = c • f x) : A →ₐ[R] B :=
  { f with
    toFun := f
    commutes' := fun c => by simp only [Algebra.algebraMap_eq_smul_one, h, f.map_one] }
Construction of \( R \)-Algebra Homomorphism from Ring Homomorphism and Linearity Condition
Informal description
Given a ring homomorphism \( f : A \to B \) between \( R \)-algebras \( A \) and \( B \), if \( f \) is \( R \)-linear (i.e., \( f(c \cdot x) = c \cdot f(x) \) for all \( c \in R \) and \( x \in A \)), then \( f \) can be promoted to an \( R \)-algebra homomorphism \( A \to_{R} B \).
AlgHom.coe_mk' theorem
(f : A →+* B) (h : ∀ (c : R) (x), f (c • x) = c • f x) : ⇑(mk' f h) = f
Full source 
@[simp]
theorem coe_mk' (f : A →+* B) (h : ∀ (c : R) (x), f (c • x) = c • f x) : ⇑(mk' f h) = f :=
  rfl
Equality of Underlying Function in $R$-Algebra Homomorphism Construction
Informal description
Let $R$ be a commutative semiring and $A$, $B$ be semirings equipped with $R$-algebra structures. Given a ring homomorphism $f: A \to B$ that satisfies the $R$-linearity condition $f(c \cdot x) = c \cdot f(x)$ for all $c \in R$ and $x \in A$, the underlying function of the $R$-algebra homomorphism constructed from $f$ via `mk'` is equal to $f$ itself.
AlgHom.id definition
: A →ₐ[R] A
Full source 
/-- Identity map as an `AlgHom`. -/
protected def id : A →ₐ[R] A :=
  { RingHom.id A with commutes' := fun _ => rfl }
Identity \( R \)-algebra homomorphism
Informal description
The identity \( R \)-algebra homomorphism from \( A \) to itself, which maps each element \( x \in A \) to itself. This homomorphism preserves both the ring structure and the \( R \)-algebra structure, satisfying: - \( f(x + y) = f(x) + f(y) \) - \( f(x \cdot y) = f(x) \cdot f(y) \) - \( f(0) = 0 \) - \( f(1) = 1 \) - \( f(r \cdot x) = r \cdot f(x) \) for all \( r \in R \) and \( x \in A \)
AlgHom.coe_id theorem
: ⇑(AlgHom.id R A) = id
Full source 
@[simp, norm_cast]
theorem coe_id : ⇑(AlgHom.id R A) = id :=
  rfl
Identity $R$-Algebra Homomorphism is the Identity Function
Informal description
The underlying function of the identity $R$-algebra homomorphism from $A$ to itself is equal to the identity function on $A$, i.e., for all $x \in A$, we have $(\mathrm{id}_A)(x) = x$.
AlgHom.id_toRingHom theorem
: (AlgHom.id R A : A →+* A) = RingHom.id _
Full source 
@[simp]
theorem id_toRingHom : (AlgHom.id R A : A →+* A) = RingHom.id _ :=
  rfl
Identity $R$-Algebra Homomorphism as Identity Ring Homomorphism
Informal description
The underlying ring homomorphism of the identity $R$-algebra homomorphism from $A$ to itself is equal to the identity ring homomorphism on $A$.
AlgHom.id_apply theorem
(p : A) : AlgHom.id R A p = p
Full source 
theorem id_apply (p : A) : AlgHom.id R A p = p :=
  rfl
Identity $R$-Algebra Homomorphism Acts as Identity Function
Informal description
For any element $p$ in an $R$-algebra $A$, the identity $R$-algebra homomorphism $\mathrm{id} \colon A \to_{R} A$ maps $p$ to itself, i.e., $\mathrm{id}(p) = p$.
AlgHom.comp definition
(φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) : A →ₐ[R] C
Full source 
/-- If `φ₁` and `φ₂` are `R`-algebra homomorphisms with the
domain of `φ₁` equal to the codomain of `φ₂`, then
`φ₁.comp φ₂` is the algebra homomorphism `x ↦ φ₁ (φ₂ x)`.
-/
def comp (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) : A →ₐ[R] C :=
  { φ₁.toRingHom.comp ↑φ₂ with
    commutes' := fun r : R => by rw [← φ₁.commutes, ← φ₂.commutes]; rfl }
Composition of \( R \)-algebra homomorphisms
Informal description
Given \( R \)-algebra homomorphisms \( \phi_1 \colon B \to C \) and \( \phi_2 \colon A \to B \), their composition \( \phi_1 \circ \phi_2 \colon A \to C \) is defined as the \( R \)-algebra homomorphism that maps each element \( x \in A \) to \( \phi_1(\phi_2(x)) \). This composition preserves both the ring structure and the action of \( R \).
AlgHom.coe_comp theorem
(φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) : ⇑(φ₁.comp φ₂) = φ₁ ∘ φ₂
Full source 
@[simp]
theorem coe_comp (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) : ⇑(φ₁.comp φ₂) = φ₁ ∘ φ₂ :=
  rfl
Composition of $R$-algebra homomorphisms preserves underlying functions
Informal description
For any $R$-algebra homomorphisms $\phi_1 \colon B \to C$ and $\phi_2 \colon A \to B$, the underlying function of their composition $\phi_1 \circ \phi_2 \colon A \to C$ is equal to the composition of the underlying functions $\phi_1 \circ \phi_2$.
AlgHom.comp_apply theorem
(φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) (p : A) : φ₁.comp φ₂ p = φ₁ (φ₂ p)
Full source 
theorem comp_apply (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) (p : A) : φ₁.comp φ₂ p = φ₁ (φ₂ p) :=
  rfl
Composition of $R$-algebra homomorphisms preserves evaluation
Informal description
For any $R$-algebra homomorphisms $\phi_1 \colon B \to C$ and $\phi_2 \colon A \to B$, and for any element $p \in A$, the composition $\phi_1 \circ \phi_2$ evaluated at $p$ equals $\phi_1$ applied to $\phi_2(p)$, i.e., $(\phi_1 \circ \phi_2)(p) = \phi_1(\phi_2(p))$.
AlgHom.comp_toRingHom theorem
(φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) : (φ₁.comp φ₂ : A →+* C) = (φ₁ : B →+* C).comp ↑φ₂
Full source 
theorem comp_toRingHom (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :
    (φ₁.comp φ₂ : A →+* C) = (φ₁ : B →+* C).comp ↑φ₂ :=
  rfl
Composition of $R$-Algebra Homomorphisms Preserves Underlying Ring Homomorphism
Informal description
For any $R$-algebra homomorphisms $\phi_1 \colon B \to C$ and $\phi_2 \colon A \to B$, the underlying ring homomorphism of their composition $\phi_1 \circ \phi_2 \colon A \to C$ is equal to the composition of the underlying ring homomorphisms $\phi_1 \circ \phi_2$.
AlgHom.comp_id theorem
: φ.comp (AlgHom.id R A) = φ
Full source 
@[simp]
theorem comp_id : φ.comp (AlgHom.id R A) = φ :=
  rfl
Composition with Identity Preserves $R$-Algebra Homomorphism
Informal description
For any $R$-algebra homomorphism $\phi \colon A \to B$, the composition of $\phi$ with the identity $R$-algebra homomorphism on $A$ equals $\phi$, i.e., $\phi \circ \text{id}_A = \phi$.
AlgHom.id_comp theorem
: (AlgHom.id R B).comp φ = φ
Full source 
@[simp]
theorem id_comp : (AlgHom.id R B).comp φ = φ :=
  rfl
Identity Composition Preserves $R$-Algebra Homomorphism
Informal description
For any $R$-algebra homomorphism $\varphi \colon A \to B$, the composition of the identity $R$-algebra homomorphism on $B$ with $\varphi$ equals $\varphi$, i.e., $\text{id}_B \circ \varphi = \varphi$.
AlgHom.comp_assoc theorem
(φ₁ : C →ₐ[R] D) (φ₂ : B →ₐ[R] C) (φ₃ : A →ₐ[R] B) : (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)
Full source 
theorem comp_assoc (φ₁ : C →ₐ[R] D) (φ₂ : B →ₐ[R] C) (φ₃ : A →ₐ[R] B) :
    (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃) :=
  rfl
Associativity of Composition of $R$-Algebra Homomorphisms
Informal description
For any $R$-algebra homomorphisms $\phi_1 \colon C \to D$, $\phi_2 \colon B \to C$, and $\phi_3 \colon A \to B$, the composition of $R$-algebra homomorphisms is associative, i.e., $(\phi_1 \circ \phi_2) \circ \phi_3 = \phi_1 \circ (\phi_2 \circ \phi_3)$.
AlgHom.toLinearMap definition
: A →ₗ[R] B
Full source 
/-- R-Alg ⥤ R-Mod -/
def toLinearMap : A →ₗ[R] B where
  toFun := φ
  map_add' := map_add _
  map_smul' := map_smul _
Linear map associated to an \( R \)-algebra homomorphism
Informal description
The linear map associated to an \( R \)-algebra homomorphism \( \varphi \colon A \to B \), where \( A \) and \( B \) are \( R \)-algebras. This map preserves addition and scalar multiplication by elements of \( R \), satisfying: - \( \varphi(x + y) = \varphi(x) + \varphi(y) \) for all \( x, y \in A \) - \( \varphi(r \cdot x) = r \cdot \varphi(x) \) for all \( r \in R \) and \( x \in A \)
AlgHom.toLinearMap_apply theorem
(p : A) : φ.toLinearMap p = φ p
Full source 
@[simp]
theorem toLinearMap_apply (p : A) : φ.toLinearMap p = φ p :=
  rfl
Equality of Linear Map and Algebra Homomorphism Evaluations
Informal description
For any $R$-algebra homomorphism $\varphi \colon A \to B$ and any element $p \in A$, the linear map associated to $\varphi$ evaluated at $p$ is equal to $\varphi(p)$, i.e., $\varphi_{\text{lin}}(p) = \varphi(p)$.
AlgHom.toLinearMap_injective theorem
: Function.Injective (toLinearMap : _ → A →ₗ[R] B)
Full source 
theorem toLinearMap_injective :
    Function.Injective (toLinearMap : _ → A →ₗ[R] B) := fun _φ₁ _φ₂ h =>
  ext <| LinearMap.congr_fun h
Injectivity of the Linear Map Associated to an $R$-Algebra Homomorphism
Informal description
The map that associates to each $R$-algebra homomorphism $\varphi \colon A \to_{R} B$ its underlying $R$-linear map is injective. In other words, if two $R$-algebra homomorphisms $\varphi_1, \varphi_2 \colon A \to_{R} B$ induce the same linear map, then $\varphi_1 = \varphi_2$.
AlgHom.comp_toLinearMap theorem
(f : A →ₐ[R] B) (g : B →ₐ[R] C) : (g.comp f).toLinearMap = g.toLinearMap.comp f.toLinearMap
Full source 
@[simp]
theorem comp_toLinearMap (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
    (g.comp f).toLinearMap = g.toLinearMap.comp f.toLinearMap :=
  rfl
Composition of Algebra Homomorphisms Preserves Linear Map Composition
Informal description
Let $R$ be a commutative semiring, and let $A$, $B$, and $C$ be $R$-algebras. For any $R$-algebra homomorphisms $f \colon A \to B$ and $g \colon B \to C$, the linear map associated to the composition $g \circ f$ is equal to the composition of the linear maps associated to $g$ and $f$, i.e., $(g \circ f)_{\text{lin}} = g_{\text{lin}} \circ f_{\text{lin}}$.
AlgHom.toLinearMap_id theorem
: toLinearMap (AlgHom.id R A) = LinearMap.id
Full source 
@[simp]
theorem toLinearMap_id : toLinearMap (AlgHom.id R A) = LinearMap.id :=
  rfl
Identity Algebra Homomorphism Yields Identity Linear Map
Informal description
For any commutative semiring $R$ and $R$-algebra $A$, the linear map associated to the identity $R$-algebra homomorphism $\text{id} \colon A \to A$ is equal to the identity linear map on $A$.
AlgHom.ofLinearMap definition
(f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ x y, f (x * y) = f x * f y) : A →ₐ[R] B
Full source 
/-- Promote a `LinearMap` to an `AlgHom` by supplying proofs about the behavior on `1` and `*`. -/
@[simps]
def ofLinearMap (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ x y, f (x * y) = f x * f y) :
    A →ₐ[R] B :=
  { f.toAddMonoidHom with
    toFun := f
    map_one' := map_one
    map_mul' := map_mul
    commutes' := fun c => by simp only [Algebra.algebraMap_eq_smul_one, f.map_smul, map_one] }
Promotion of linear map to algebra homomorphism
Informal description
Given a linear map \( f \colon A \to B \) between \( R \)-algebras \( A \) and \( B \), if \( f \) satisfies: 1. \( f(1) = 1 \) (preservation of multiplicative identity) 2. \( f(x \cdot y) = f(x) \cdot f(y) \) for all \( x, y \in A \) (preservation of multiplication) then \( f \) can be promoted to an \( R \)-algebra homomorphism \( A \to_{R} B \). This homomorphism also preserves the action of \( R \) on \( A \) and \( B \).
AlgHom.ofLinearMap_toLinearMap theorem
(map_one) (map_mul) : ofLinearMap φ.toLinearMap map_one map_mul = φ
Full source 
@[simp]
theorem ofLinearMap_toLinearMap (map_one) (map_mul) :
    ofLinearMap φ.toLinearMap map_one map_mul = φ :=
  rfl
Recovery of Algebra Homomorphism from its Linear Map
Informal description
Let $R$ be a commutative semiring, and let $A$ and $B$ be semirings equipped with $R$-algebra structures. Given an $R$-algebra homomorphism $\varphi \colon A \to B$ and proofs that: 1. $\varphi(1) = 1$ (preservation of multiplicative identity) 2. $\varphi(x \cdot y) = \varphi(x) \cdot \varphi(y)$ for all $x, y \in A$ (preservation of multiplication) then the construction of an $R$-algebra homomorphism from the associated linear map $\varphi$ recovers $\varphi$ itself, i.e., $\text{ofLinearMap}(\varphi.\text{toLinearMap}, \text{map\_one}, \text{map\_mul}) = \varphi$.
AlgHom.toLinearMap_ofLinearMap theorem
(f : A →ₗ[R] B) (map_one) (map_mul) : toLinearMap (ofLinearMap f map_one map_mul) = f
Full source 
@[simp]
theorem toLinearMap_ofLinearMap (f : A →ₗ[R] B) (map_one) (map_mul) :
    toLinearMap (ofLinearMap f map_one map_mul) = f :=
  rfl
Linear Map Identity under Algebra Homomorphism Construction
Informal description
For any linear map $f \colon A \to B$ between $R$-algebras $A$ and $B$ that satisfies: 1. $f(1) = 1$ (preservation of multiplicative identity) 2. $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in A$ (preservation of multiplication), the linear map associated to the $R$-algebra homomorphism constructed from $f$ via `ofLinearMap` is equal to $f$ itself. In other words, the operation of converting a linear map to an algebra homomorphism and back to a linear map is the identity operation when the linear map satisfies the algebra homomorphism conditions.
AlgHom.ofLinearMap_id theorem
(map_one) (map_mul) : ofLinearMap LinearMap.id map_one map_mul = AlgHom.id R A
Full source 
@[simp]
theorem ofLinearMap_id (map_one) (map_mul) :
    ofLinearMap LinearMap.id map_one map_mul = AlgHom.id R A :=
  rfl
Promotion of Identity Linear Map to Identity Algebra Homomorphism
Informal description
Let $A$ be an $R$-algebra and let $\text{LinearMap.id} \colon A \to A$ be the identity linear map. If $\text{LinearMap.id}$ satisfies: 1. $\text{LinearMap.id}(1) = 1$ (preservation of multiplicative identity) 2. $\text{LinearMap.id}(x \cdot y) = \text{LinearMap.id}(x) \cdot \text{LinearMap.id}(y)$ for all $x, y \in A$ (preservation of multiplication) then the $R$-algebra homomorphism obtained by promoting $\text{LinearMap.id}$ via $\text{ofLinearMap}$ is equal to the identity $R$-algebra homomorphism $\text{AlgHom.id} \colon A \to_{R} A$.
AlgHom.map_smul_of_tower theorem
{R'} [SMul R' A] [SMul R' B] [LinearMap.CompatibleSMul A B R' R] (r : R') (x : A) : φ (r • x) = r • φ x
Full source 
theorem map_smul_of_tower {R'} [SMul R' A] [SMul R' B] [LinearMap.CompatibleSMul A B R' R] (r : R')
    (x : A) : φ (r • x) = r • φ x :=
  φ.toLinearMap.map_smul_of_tower r x
Scalar multiplication preservation under $R$-algebra homomorphisms with compatible actions
Informal description
Let $R'$ be a type equipped with scalar multiplication operations on $A$ and $B$, and suppose these operations are compatible with the $R$-algebra structures on $A$ and $B$ through the linear map $\varphi$. Then for any scalar $r \in R'$ and any element $x \in A$, the $R$-algebra homomorphism $\varphi$ satisfies $\varphi(r \cdot x) = r \cdot \varphi(x)$.
AlgHom.End instance
: Monoid (A →ₐ[R] A)
Full source 
@[simps -isSimp toSemigroup_toMul_mul toOne_one]
instance End : Monoid (A →ₐ[R] A) where
  mul := comp
  mul_assoc _ _ _ := rfl
  one := AlgHom.id R A
  one_mul _ := rfl
  mul_one _ := rfl
Monoid Structure on $R$-Algebra Endomorphisms
Informal description
The set of $R$-algebra endomorphisms $A \to_{R} A$ forms a monoid under composition, where the identity element is the identity homomorphism and the multiplication operation is given by composition of homomorphisms.
AlgHom.one_apply theorem
(x : A) : (1 : A →ₐ[R] A) x = x
Full source 
@[simp]
theorem one_apply (x : A) : (1 : A →ₐ[R] A) x = x :=
  rfl
Identity $R$-Algebra Homomorphism Acts as Identity on Elements
Informal description
For any element $x$ in an $R$-algebra $A$, the identity $R$-algebra homomorphism $1 \colon A \to_{R} A$ satisfies $1(x) = x$.
AlgHom.mul_apply theorem
(φ ψ : A →ₐ[R] A) (x : A) : (φ * ψ) x = φ (ψ x)
Full source 
@[simp]
theorem mul_apply (φ ψ : A →ₐ[R] A) (x : A) : (φ * ψ) x = φ (ψ x) :=
  rfl
Composition of $R$-Algebra Endomorphisms
Informal description
For any $R$-algebra endomorphisms $\phi, \psi \colon A \to_{R} A$ and any element $x \in A$, the composition $(\phi \circ \psi)(x)$ equals $\phi(\psi(x))$.
AlgHom.coe_pow theorem
(φ : A →ₐ[R] A) (n : ℕ) : ⇑(φ ^ n) = φ^[n]
Full source 
@[simp] theorem coe_pow (φ : A →ₐ[R] A) (n : ℕ) : ⇑(φ ^ n) = φ^[n] :=
   n.rec (by ext; simp) fun _ ih ↦ by ext; simp [pow_succ, ih]
Iteration of $R$-algebra endomorphisms: $\varphi^n = \varphi^[n]$
Informal description
For any $R$-algebra endomorphism $\varphi \colon A \to_{R} A$ and any natural number $n$, the underlying function of the $n$-th power of $\varphi$ is equal to the $n$-th iterate of $\varphi$, i.e., $(\varphi^n)(x) = \varphi^[n](x)$ for all $x \in A$.
AlgHom.algebraMap_eq_apply theorem
(f : A →ₐ[R] B) {y : R} {x : A} (h : algebraMap R A y = x) : algebraMap R B y = f x
Full source 
theorem algebraMap_eq_apply (f : A →ₐ[R] B) {y : R} {x : A} (h : algebraMap R A y = x) :
    algebraMap R B y = f x :=
  h ▸ (f.commutes _).symm
Compatibility of Algebra Homomorphisms with Algebra Maps
Informal description
Let $R$ be a commutative semiring and $A$, $B$ be semirings equipped with $R$-algebra structures. For any $R$-algebra homomorphism $f \colon A \to_{R} B$, if $x \in A$ is the image of $y \in R$ under the algebra map $\text{algebraMap}_R^A$, then the image of $y$ under $\text{algebraMap}_R^B$ equals $f(x)$. In other words, if $\text{algebraMap}_R^A(y) = x$, then $\text{algebraMap}_R^B(y) = f(x)$.
RingHom.toNatAlgHom definition
[Semiring R] [Semiring S] (f : R →+* S) : R →ₐ[ℕ] S
Full source 
/-- Reinterpret a `RingHom` as an `ℕ`-algebra homomorphism. -/
def toNatAlgHom [Semiring R] [Semiring S] (f : R →+* S) : R →ₐ[ℕ] S :=
  { f with
    toFun := f
    commutes' := fun n => by simp }
Reinterpretation of a Ring Homomorphism as an \( \mathbb{N} \)-Algebra Homomorphism
Informal description
Given a semiring homomorphism \( f \colon R \to S \) between semirings \( R \) and \( S \), the function `RingHom.toNatAlgHom` reinterprets \( f \) as an \( \mathbb{N} \)-algebra homomorphism \( R \to_{\mathbb{N}} S \). This reinterpretation preserves the underlying function \( f \) and satisfies the additional property that it commutes with the natural number scalar multiplication, i.e., for any natural number \( n \), the action of \( n \) on \( R \) is preserved under \( f \).
RingHom.toNatAlgHom_coe theorem
[Semiring R] [Semiring S] (f : R →+* S) : ⇑f.toNatAlgHom = ⇑f
Full source 
@[simp]
lemma toNatAlgHom_coe [Semiring R] [Semiring S] (f : R →+* S) :
    ⇑f.toNatAlgHom = ⇑f := rfl
Equality of Underlying Functions in Natural Number Algebra Homomorphism Construction
Informal description
For any semirings $R$ and $S$, and any ring homomorphism $f \colon R \to S$, the underlying function of the $\mathbb{N}$-algebra homomorphism obtained from $f$ via `RingHom.toNatAlgHom` is equal to $f$ itself. In other words, $f.toNatAlgHom(x) = f(x)$ for all $x \in R$.
RingHom.toNatAlgHom_apply theorem
[Semiring R] [Semiring S] (f : R →+* S) (x : R) : f.toNatAlgHom x = f x
Full source 
lemma toNatAlgHom_apply [Semiring R] [Semiring S] (f : R →+* S) (x : R) :
    f.toNatAlgHom x = f x := rfl
Evaluation of $\mathbb{N}$-Algebra Homomorphism from Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings, and let $f: R \to S$ be a ring homomorphism. Then for any element $x \in R$, the evaluation of the $\mathbb{N}$-algebra homomorphism obtained from $f$ at $x$ equals $f(x)$, i.e., $f.toNatAlgHom(x) = f(x)$.
RingHom.toIntAlgHom definition
[Ring R] [Ring S] (f : R →+* S) : R →ₐ[ℤ] S
Full source 
/-- Reinterpret a `RingHom` as a `ℤ`-algebra homomorphism. -/
def toIntAlgHom [Ring R] [Ring S] (f : R →+* S) : R →ₐ[ℤ] S :=
  { f with commutes' := fun n => by simp }
Reinterpretation of a ring homomorphism as a $\mathbb{Z}$-algebra homomorphism
Informal description
Given a ring homomorphism $f \colon R \to S$ between rings $R$ and $S$, the function `RingHom.toIntAlgHom` reinterprets $f$ as a $\mathbb{Z}$-algebra homomorphism $R \to_{\mathbb{Z}} S$. This reinterpretation preserves the action of $\mathbb{Z}$ by construction, i.e., for any integer $n$, the map satisfies $f(n \cdot r) = n \cdot f(r)$ for all $r \in R$.
RingHom.toIntAlgHom_coe theorem
[Ring R] [Ring S] (f : R →+* S) : ⇑f.toIntAlgHom = ⇑f
Full source 
@[simp]
lemma toIntAlgHom_coe [Ring R] [Ring S] (f : R →+* S) :
    ⇑f.toIntAlgHom = ⇑f := rfl
Underlying Function of $\mathbb{Z}$-Algebra Homomorphism from Ring Homomorphism
Informal description
For any ring homomorphism $f \colon R \to S$ between rings $R$ and $S$, the underlying function of the $\mathbb{Z}$-algebra homomorphism obtained from $f$ via `RingHom.toIntAlgHom` is equal to $f$ itself. In other words, the coercion of $f.toIntAlgHom$ to a function coincides with $f$.
RingHom.toIntAlgHom_apply theorem
[Ring R] [Ring S] (f : R →+* S) (x : R) : f.toIntAlgHom x = f x
Full source 
lemma toIntAlgHom_apply [Ring R] [Ring S] (f : R →+* S) (x : R) :
    f.toIntAlgHom x = f x := rfl
Equality of Ring Homomorphism and its $\mathbb{Z}$-Algebra Homomorphism Interpretation
Informal description
Let $R$ and $S$ be rings, and let $f \colon R \to S$ be a ring homomorphism. Then for any element $x \in R$, the $\mathbb{Z}$-algebra homomorphism obtained from $f$ via `RingHom.toIntAlgHom` satisfies $(f.toIntAlgHom)(x) = f(x)$.
RingHom.toIntAlgHom_injective theorem
[Ring R] [Ring S] : Function.Injective (RingHom.toIntAlgHom : (R →+* S) → _)
Full source 
lemma toIntAlgHom_injective [Ring R] [Ring S] :
    Function.Injective (RingHom.toIntAlgHom : (R →+* S) → _) :=
  fun _ _ e ↦ DFunLike.ext _ _ (fun x ↦ DFunLike.congr_fun e x)
Injectivity of the $\mathbb{Z}$-Algebra Homomorphism Interpretation of Ring Homomorphisms
Informal description
For any rings $R$ and $S$, the map that reinterprets a ring homomorphism $f \colon R \to S$ as a $\mathbb{Z}$-algebra homomorphism is injective. That is, if two ring homomorphisms $f, g \colon R \to S$ satisfy $f(n \cdot r) = g(n \cdot r)$ for all $n \in \mathbb{Z}$ and $r \in R$, then $f = g$.
Algebra.ofId definition
: R →ₐ[R] A
Full source 
/-- `AlgebraMap` as an `AlgHom`. -/
def ofId : R →ₐ[R] A :=
  { algebraMap R A with commutes' := fun _ => rfl }
Canonical \( R \)-algebra homomorphism from \( R \) to \( A \)
Informal description
The canonical \( R \)-algebra homomorphism from \( R \) to \( A \), which is the algebra map \( R \to A \) equipped with the additional property that it commutes with the action of \( R \).
Algebra.ofId_apply theorem
(r) : ofId R A r = algebraMap R A r
Full source 
theorem ofId_apply (r) : ofId R A r = algebraMap R A r :=
  rfl
Canonical $R$-algebra homomorphism agrees with algebra map: $\text{ofId}_R A (r) = \text{algebraMap}_R A (r)$
Informal description
For any element $r$ in a commutative semiring $R$, the canonical $R$-algebra homomorphism $\text{ofId}_R A$ evaluated at $r$ is equal to the algebra map $\text{algebraMap}_R A$ evaluated at $r$, i.e., $\text{ofId}_R A (r) = \text{algebraMap}_R A (r)$.
Algebra.subsingleton_id instance
: Subsingleton (R →ₐ[R] A)
Full source 
/-- This is a special case of a more general instance that we define in a later file. -/
instance subsingleton_id : Subsingleton (R →ₐ[R] A) :=
  ⟨fun f g => AlgHom.ext fun _ => (f.commutes _).trans (g.commutes _).symm⟩
Uniqueness of the Canonical $R$-Algebra Homomorphism from $R$ to $A$
Informal description
For any commutative semiring $R$ and $R$-algebra $A$, the type of $R$-algebra homomorphisms from $R$ to $A$ is a subsingleton (i.e., has at most one element up to equality).
Algebra.ext_id theorem
(f g : R →ₐ[R] A) : f = g
Full source 
/-- This ext lemma closes trivial subgoals create when chaining heterobasic ext lemmas. -/
@[ext high]
theorem ext_id (f g : R →ₐ[R] A) : f = g := Subsingleton.elim _ _
Uniqueness of $R$-algebra homomorphisms from $R$ to $A$
Informal description
For any two $R$-algebra homomorphisms $f, g: R \to_{R} A$, we have $f = g$.
Algebra.comp_ofId theorem
(φ : A →ₐ[R] B) : φ.comp (Algebra.ofId R A) = Algebra.ofId R B
Full source 
@[simp]
theorem comp_ofId (φ : A →ₐ[R] B) : φ.comp (Algebra.ofId R A) = Algebra.ofId R B := by ext
Compatibility of $R$-algebra homomorphisms with canonical maps
Informal description
For any $R$-algebra homomorphism $\phi \colon A \to_{R} B$, the composition of $\phi$ with the canonical $R$-algebra homomorphism $\text{ofId}_R \colon R \to_{R} A$ equals the canonical $R$-algebra homomorphism $\text{ofId}_R \colon R \to_{R} B$. In other words, $\phi \circ \text{ofId}_R = \text{ofId}_R$.
Algebra.instMulDistribMulActionAlgHomUnits instance
: MulDistribMulAction (A →ₐ[R] A) Aˣ
Full source 
instance : MulDistribMulAction (A →ₐ[R] A) Aˣ where
  smul f := Units.map f
  one_smul _ := by ext; rfl
  mul_smul _ _ _ := by ext; rfl
  smul_mul _ _ _ := by ext; exact map_mul _ _ _
  smul_one _ := by ext; exact map_one _
Multiplicative Distributive Action of Algebra Endomorphisms on Units
Informal description
The group of units $A^\times$ of an $R$-algebra $A$ carries a multiplicative distributive action by the monoid of $R$-algebra endomorphisms $A \to_{R} A$. This means that for any $R$-algebra endomorphism $f$ and any units $x, y \in A^\times$, the action satisfies $f \cdot (x * y) = (f \cdot x) * (f \cdot y)$.
Algebra.smul_units_def theorem
(f : A →ₐ[R] A) (x : Aˣ) : f • x = Units.map (f : A →* A) x
Full source 
@[simp]
theorem smul_units_def (f : A →ₐ[R] A) (x : Aˣ) :
    f • x = Units.map (f : A →* A) x := rfl
Action of Algebra Endomorphism on Units via Induced Monoid Homomorphism
Informal description
For any $R$-algebra endomorphism $f \colon A \to_{R} A$ and any unit $x \in A^\times$, the action of $f$ on $x$ is given by the image of $x$ under the induced monoid homomorphism $f \colon A \to^* A$ applied to the units, i.e., $f \cdot x = \text{Units.map}(f)(x)$.
Algebra.algebraMapSubmonoid_map_eq theorem
(f : A →ₐ[R] B) : (algebraMapSubmonoid A M).map f = algebraMapSubmonoid B M
Full source 
lemma algebraMapSubmonoid_map_eq (f : A →ₐ[R] B) :
    (algebraMapSubmonoid A M).map f = algebraMapSubmonoid B M := by
  ext x
  constructor
  · rintro ⟨a, ⟨r, hr, rfl⟩, rfl⟩
    simp only [AlgHom.commutes]
    use r
  · rintro ⟨r, hr, rfl⟩
    simp only [Submonoid.mem_map]
    use (algebraMap R A r)
    simp only [AlgHom.commutes, and_true]
    use r
Equality of Submonoid Images under Algebra Homomorphism
Informal description
Let $R$ be a commutative semiring, and let $A$ and $B$ be semirings equipped with $R$-algebra structures. Given an $R$-algebra homomorphism $f \colon A \to_{R} B$ and a submonoid $M$ of $R$, the image of the submonoid $\text{algebraMapSubmonoid}_A(M)$ under $f$ is equal to $\text{algebraMapSubmonoid}_B(M)$. In other words, the following equality holds for the submonoids of $B$: $$ f(\text{algebraMapSubmonoid}_A(M)) = \text{algebraMapSubmonoid}_B(M). $$
Algebra.algebraMapSubmonoid_le_comap theorem
(f : A →ₐ[R] B) : algebraMapSubmonoid A M ≤ (algebraMapSubmonoid B M).comap f.toRingHom
Full source 
lemma algebraMapSubmonoid_le_comap (f : A →ₐ[R] B) :
    algebraMapSubmonoid A M ≤ (algebraMapSubmonoid B M).comap f.toRingHom := by
  rw [← algebraMapSubmonoid_map_eq M f]
  exact Submonoid.le_comap_map (Algebra.algebraMapSubmonoid A M)
Inclusion of Algebra Map Submonoid in Preimage under $R$-Algebra Homomorphism
Informal description
Let $R$ be a commutative semiring, and let $A$ and $B$ be semirings equipped with $R$-algebra structures. Given an $R$-algebra homomorphism $f \colon A \to_{R} B$ and a submonoid $M$ of $R$, the submonoid $\text{algebraMapSubmonoid}_A(M)$ is contained in the preimage of $\text{algebraMapSubmonoid}_B(M)$ under the ring homomorphism $f$. In other words, the following inclusion holds for the submonoids of $A$: $$ \text{algebraMapSubmonoid}_A(M) \subseteq f^{-1}(\text{algebraMapSubmonoid}_B(M)). $$
MulSemiringAction.toAlgHom definition
(m : M) : A →ₐ[R] A
Full source 
/-- Each element of the monoid defines an algebra homomorphism.

This is a stronger version of `MulSemiringAction.toRingHom` and
`DistribMulAction.toLinearMap`. -/
@[simps]
def toAlgHom (m : M) : A →ₐ[R] A :=
  { MulSemiringAction.toRingHom _ _ m with
    toFun := fun a => m • a
    commutes' := smul_algebraMap _ }
$R$-algebra homomorphism induced by monoid action element
Informal description
For each element $m$ of the monoid $M$ acting multiplicatively on the $R$-algebra $A$, the map sending $a \mapsto m \cdot a$ is an $R$-algebra homomorphism from $A$ to itself. This homomorphism preserves both the ring structure and the $R$-algebra structure, meaning it satisfies: 1. $m \cdot (a + b) = m \cdot a + m \cdot b$ (additive preservation) 2. $m \cdot (a * b) = (m \cdot a) * (m \cdot b)$ (multiplicative preservation) 3. $m \cdot (r \cdot a) = r \cdot (m \cdot a)$ for $r \in R$ ($R$-linearity) 4. $m \cdot 1 = 1$ (preservation of multiplicative identity) where $\cdot$ denotes both the monoid action and the algebra scalar multiplication.
MulSemiringAction.toAlgHom_injective theorem
[FaithfulSMul M A] : Function.Injective (MulSemiringAction.toAlgHom R A : M → A →ₐ[R] A)
Full source 
theorem toAlgHom_injective [FaithfulSMul M A] :
    Function.Injective (MulSemiringAction.toAlgHom R A : M → A →ₐ[R] A) := fun _m₁ _m₂ h =>
  eq_of_smul_eq_smul fun r => AlgHom.ext_iff.1 h r
Injectivity of Monoid Action to Algebra Homomorphism Map under Faithful Action
Informal description
Let $M$ be a monoid acting multiplicatively on an $R$-algebra $A$, where the scalar multiplication action is faithful (i.e., distinct elements of $M$ act differently on $A$). Then the map sending each $m \in M$ to the corresponding $R$-algebra homomorphism $a \mapsto m \cdot a$ is injective.