# 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.
structure AlgHom (R : Type u) (A : Type v) (B : Type w) [] [] [] [Algebra R A] [Algebra R B] extends :
Type (max v w)

Defining the homomorphism in the category R-Alg.

• toFun : AB
• map_one' : (self.toRingHom).toFun 1 = 1
• map_mul' : ∀ (x y : A), (self.toRingHom).toFun (x * y) = (self.toRingHom).toFun x * (self.toRingHom).toFun y
• map_zero' : (self.toRingHom).toFun 0 = 0
• map_add' : ∀ (x y : A), (self.toRingHom).toFun (x + y) = (self.toRingHom).toFun x + (self.toRingHom).toFun y
• commutes' : ∀ (r : R), (self.toRingHom).toFun (() r) = () r
Instances For
theorem AlgHom.commutes' {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (self : A →ₐ[R] B) (r : R) :
(self.toRingHom).toFun (() r) = () r

Defining the homomorphism in the category R-Alg.

Equations
Instances For

Defining the homomorphism in the category R-Alg.

Equations
• One or more equations did not get rendered due to their size.
Instances For
class AlgHomClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [] [] [] [Algebra R A] [Algebra R B] [FunLike F A B] extends :

AlgHomClass F R A B asserts F is a type of bundled algebra homomorphisms from A to B.

• map_mul : ∀ (f : F) (x y : A), f (x * y) = f x * f y
• map_one : ∀ (f : F), f 1 = 1
• map_add : ∀ (f : F) (x y : A), f (x + y) = f x + f y
• map_zero : ∀ (f : F), f 0 = 0
• commutes : ∀ (f : F) (r : R), f (() r) = () r
Instances
theorem AlgHomClass.commutes {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} [] [] [] [Algebra R A] [Algebra R B] [FunLike F A B] [self : AlgHomClass F R A B] (f : F) (r : R) :
f (() r) = () r
@[instance 100]
instance AlgHomClass.linearMapClass {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [] [] [] [Algebra R A] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] :
Equations
• =
def AlgHomClass.toAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [Algebra R A] [Algebra R B] {F : Type u_5} [FunLike F A B] [AlgHomClass F R A B] (f : F) :

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

Equations
• f = let __spread.0 := f; { toFun := f, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
instance AlgHomClass.coeTC {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [Algebra R A] [Algebra R B] {F : Type u_5} [FunLike F A B] [AlgHomClass F R A B] :
CoeTC F (A →ₐ[R] B)
Equations
• AlgHomClass.coeTC = { coe := AlgHomClass.toAlgHom }
instance AlgHom.funLike {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] :
FunLike (A →ₐ[R] B) A B
Equations
• AlgHom.funLike = { coe := fun (f : A →ₐ[R] B) => (f.toRingHom).toFun, coe_injective' := }
instance AlgHom.algHomClass {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] :
AlgHomClass (A →ₐ[R] B) R A B
Equations
• =
def AlgHom.Simps.apply {R : Type u} {α : Type v} {β : Type w} [] [] [] [Algebra R α] [Algebra R β] (f : α →ₐ[R] β) :
αβ

See Note [custom simps projection]

Equations
Instances For
@[simp]
theorem AlgHom.coe_coe {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] {F : Type u_1} [FunLike F A B] [AlgHomClass F R A B] (f : F) :
f = f
@[simp]
theorem AlgHom.toFun_eq_coe {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
(f.toRingHom).toFun = f
def AlgHom.toMonoidHom' {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
A →* B
Equations
• f = f
Instances For
instance AlgHom.coeOutMonoidHom {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] :
CoeOut (A →ₐ[R] B) (A →* B)
Equations
• AlgHom.coeOutMonoidHom = { coe := AlgHom.toMonoidHom' }
def AlgHom.toAddMonoidHom' {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
A →+ B
Equations
• f = f
Instances For
instance AlgHom.coeOutAddMonoidHom {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] :
CoeOut (A →ₐ[R] B) (A →+ B)
Equations
@[simp]
theorem AlgHom.coe_mk {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] {f : A →+* B} (h : ∀ (r : R), (f).toFun (() r) = () r) :
{ toRingHom := f, commutes' := h } = f
theorem AlgHom.coe_mks {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] {f : AB} (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), { toFun := f, map_one' := h₁ }.toFun (x * y) = { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y) (h₃ : ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x y : A), ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x + ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y) (h₅ : ∀ (r : R), ({ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun (() r) = () r) :
{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ } = f
@[simp]
theorem AlgHom.coe_ringHom_mk {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] {f : A →+* B} (h : ∀ (r : R), (f).toFun (() r) = () r) :
{ toRingHom := f, commutes' := h } = f
@[simp]
theorem AlgHom.toRingHom_eq_coe {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
f.toRingHom = f
@[simp]
theorem AlgHom.coe_toRingHom {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
f = f
@[simp]
theorem AlgHom.coe_toMonoidHom {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
f = f
@[simp]
theorem AlgHom.coe_toAddMonoidHom {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
f = f
theorem AlgHom.coe_fn_injective {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] :
Function.Injective DFunLike.coe
theorem AlgHom.coe_fn_inj {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] {φ₁ : A →ₐ[R] B} {φ₂ : A →ₐ[R] B} :
φ₁ = φ₂ φ₁ = φ₂
theorem AlgHom.coe_ringHom_injective {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] :
Function.Injective RingHomClass.toRingHom
theorem AlgHom.coe_monoidHom_injective {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] :
Function.Injective MonoidHomClass.toMonoidHom
theorem AlgHom.coe_addMonoidHom_injective {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] :
theorem AlgHom.congr_fun {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] {φ₁ : A →ₐ[R] B} {φ₂ : A →ₐ[R] B} (H : φ₁ = φ₂) (x : A) :
φ₁ x = φ₂ x
theorem AlgHom.congr_arg {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {x : A} {y : A} (h : x = y) :
φ x = φ y
theorem AlgHom.ext {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] {φ₁ : A →ₐ[R] B} {φ₂ : A →ₐ[R] B} (H : ∀ (x : A), φ₁ x = φ₂ x) :
φ₁ = φ₂
theorem AlgHom.ext_iff {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] {φ₁ : A →ₐ[R] B} {φ₂ : A →ₐ[R] B} :
φ₁ = φ₂ ∀ (x : A), φ₁ x = φ₂ x
@[simp]
theorem AlgHom.mk_coe {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] {f : A →ₐ[R] B} (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), { toFun := f, map_one' := h₁ }.toFun (x * y) = { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y) (h₃ : ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x y : A), ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x + ({ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y) (h₅ : ∀ (r : R), ({ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun (() r) = () r) :
{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ } = f
@[simp]
theorem AlgHom.commutes {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (r : R) :
φ (() r) = () r
theorem AlgHom.comp_algebraMap {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :
(φ).comp () =
theorem AlgHom.map_add {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (r : A) (s : A) :
φ (r + s) = φ r + φ s
@[deprecated map_zero]
theorem AlgHom.map_zero {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :
φ 0 = 0
@[deprecated map_mul]
theorem AlgHom.map_mul {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (x : A) (y : A) :
φ (x * y) = φ x * φ y
@[deprecated map_one]
theorem AlgHom.map_one {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :
φ 1 = 1
@[deprecated map_pow]
theorem AlgHom.map_pow {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (x : A) (n : ) :
φ (x ^ n) = φ x ^ n
@[deprecated map_smul]
theorem AlgHom.map_smul {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (r : R) (x : A) :
φ (r x) = r φ x
@[deprecated map_sum]
theorem AlgHom.map_sum {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {ι : Type u_1} (f : ιA) (s : ) :
φ (xs, f x) = xs, φ (f x)
@[deprecated map_finsupp_sum]
theorem AlgHom.map_finsupp_sum {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {α : Type u_1} [Zero α] {ι : Type u_2} (f : ι →₀ α) (g : ιαA) :
φ (f.sum g) = f.sum fun (i : ι) (a : α) => φ (g i a)
def AlgHom.mk' {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →+* B) (h : ∀ (c : R) (x : A), f (c x) = c f x) :

If a RingHom is R-linear, then it is an AlgHom.

Equations
• = { toFun := f, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem AlgHom.coe_mk' {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →+* B) (h : ∀ (c : R) (x : A), f (c x) = c f x) :
() = f
def AlgHom.id (R : Type u) (A : Type v) [] [] [Algebra R A] :

Identity map as an AlgHom.

Equations
• = let __src := ; { toRingHom := __src, commutes' := }
Instances For
@[simp]
theorem AlgHom.coe_id (R : Type u) (A : Type v) [] [] [Algebra R A] :
() = id
@[simp]
theorem AlgHom.id_toRingHom (R : Type u) (A : Type v) [] [] [Algebra R A] :
() =
theorem AlgHom.id_apply {R : Type u} {A : Type v} [] [] [Algebra R A] (p : A) :
() p = p
def AlgHom.comp {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :

Composition of algebra homeomorphisms.

Equations
• φ₁.comp φ₂ = let __src := φ₁.comp φ₂; { toRingHom := __src, commutes' := }
Instances For
@[simp]
theorem AlgHom.coe_comp {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :
(φ₁.comp φ₂) = φ₁ φ₂
theorem AlgHom.comp_apply {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) (p : A) :
(φ₁.comp φ₂) p = φ₁ (φ₂ p)
theorem AlgHom.comp_toRingHom {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :
(φ₁.comp φ₂) = (φ₁).comp φ₂
@[simp]
theorem AlgHom.comp_id {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :
φ.comp () = φ
@[simp]
theorem AlgHom.id_comp {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :
().comp φ = φ
theorem AlgHom.comp_assoc {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} {D : Type v₁} [] [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] (φ₁ : C →ₐ[R] D) (φ₂ : B →ₐ[R] C) (φ₃ : A →ₐ[R] B) :
(φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)
def AlgHom.toLinearMap {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :

R-Alg ⥤ R-Mod

Equations
• φ.toLinearMap = { toFun := φ, map_add' := , map_smul' := }
Instances For
@[simp]
theorem AlgHom.toLinearMap_apply {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (p : A) :
φ.toLinearMap p = φ p
theorem AlgHom.toLinearMap_injective {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] :
Function.Injective AlgHom.toLinearMap
@[simp]
theorem AlgHom.comp_toLinearMap {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [] [] [] [] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
(g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
@[simp]
theorem AlgHom.toLinearMap_id {R : Type u} {A : Type v} [] [] [Algebra R A] :
().toLinearMap = LinearMap.id
@[simp]
theorem AlgHom.ofLinearMap_apply {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ (x y : A), f (x * y) = f x * f y) (a : A) :
(AlgHom.ofLinearMap f map_one map_mul) a = f a
def AlgHom.ofLinearMap {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ (x y : A), f (x * y) = f x * f y) :

Promote a LinearMap to an AlgHom by supplying proofs about the behavior on 1 and *.

Equations
• AlgHom.ofLinearMap f map_one map_mul = let __src := f.toAddMonoidHom; { toFun := f, map_one' := map_one, map_mul' := map_mul, map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem AlgHom.ofLinearMap_toLinearMap {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (map_one : φ.toLinearMap 1 = 1) (map_mul : ∀ (x y : A), φ.toLinearMap (x * y) = φ.toLinearMap x * φ.toLinearMap y) :
AlgHom.ofLinearMap φ.toLinearMap map_one map_mul = φ
@[simp]
theorem AlgHom.toLinearMap_ofLinearMap {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ (x y : A), f (x * y) = f x * f y) :
(AlgHom.ofLinearMap f map_one map_mul).toLinearMap = f
@[simp]
theorem AlgHom.ofLinearMap_id {R : Type u} {A : Type v} [] [] [Algebra R A] (map_one : LinearMap.id 1 = 1) (map_mul : ∀ (x y : A), LinearMap.id (x * y) = LinearMap.id x * LinearMap.id y) :
AlgHom.ofLinearMap LinearMap.id map_one map_mul =
theorem AlgHom.map_smul_of_tower {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {R' : Type u_1} [SMul R' A] [SMul R' B] [] (r : R') (x : A) :
φ (r x) = r φ x
@[deprecated map_list_prod]
theorem AlgHom.map_list_prod {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (s : List A) :
φ s.prod = (List.map (φ) s).prod
theorem AlgHom.End_toSemigroup_toMul_mul {R : Type u} {A : Type v} [] [] [Algebra R A] (φ₁ : A →ₐ[R] A) (φ₂ : A →ₐ[R] A) :
φ₁ * φ₂ = φ₁.comp φ₂
theorem AlgHom.End_toOne_one {R : Type u} {A : Type v} [] [] [Algebra R A] :
1 =
instance AlgHom.End {R : Type u} {A : Type v} [] [] [Algebra R A] :
Equations
@[simp]
theorem AlgHom.one_apply {R : Type u} {A : Type v} [] [] [Algebra R A] (x : A) :
1 x = x
@[simp]
theorem AlgHom.mul_apply {R : Type u} {A : Type v} [] [] [Algebra R A] (φ : A →ₐ[R] A) (ψ : A →ₐ[R] A) (x : A) :
(φ * ψ) x = φ (ψ x)
theorem AlgHom.algebraMap_eq_apply {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) {y : R} {x : A} (h : () y = x) :
() y = f x
@[deprecated map_multiset_prod]
theorem AlgHom.map_multiset_prod {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (s : ) :
φ s.prod = (Multiset.map (φ) s).prod
@[deprecated map_prod]
theorem AlgHom.map_prod {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {ι : Type u_1} (f : ιA) (s : ) :
φ (xs, f x) = xs, φ (f x)
@[deprecated map_finsupp_prod]
theorem AlgHom.map_finsupp_prod {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {α : Type u_1} [Zero α] {ι : Type u_2} (f : ι →₀ α) (g : ιαA) :
φ (f.prod g) = f.prod fun (i : ι) (a : α) => φ (g i a)
@[deprecated map_neg]
theorem AlgHom.map_neg {R : Type u} {A : Type v} {B : Type w} [] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (x : A) :
φ (-x) = -φ x
@[deprecated map_sub]
theorem AlgHom.map_sub {R : Type u} {A : Type v} {B : Type w} [] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (x : A) (y : A) :
φ (x - y) = φ x - φ y
def RingHom.toNatAlgHom {R : Type u_1} {S : Type u_2} [] [] (f : R →+* S) :

Reinterpret a RingHom as an ℕ-algebra homomorphism.

Equations
• f.toNatAlgHom = { toFun := f, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
def RingHom.toIntAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [] [] (f : R →+* S) :

Reinterpret a RingHom as a ℤ-algebra homomorphism.

Equations
• f.toIntAlgHom = { toRingHom := f, commutes' := }
Instances For
theorem RingHom.toIntAlgHom_injective {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [] [] :
Function.Injective RingHom.toIntAlgHom
def RingHom.toRatAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [] [] (f : R →+* S) :

Reinterpret a RingHom as a ℚ-algebra homomorphism. This actually yields an equivalence, see RingHom.equivRatAlgHom.

Equations
• f.toRatAlgHom = { toRingHom := f, commutes' := }
Instances For
@[simp]
theorem RingHom.toRatAlgHom_toRingHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [] [] (f : R →+* S) :
f.toRatAlgHom = f
@[simp]
theorem AlgHom.toRingHom_toRatAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [] [] (f : R →ₐ[] S) :
(f).toRatAlgHom = f
@[simp]
theorem RingHom.equivRatAlgHom_symm_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [] [] (self : R →ₐ[] S) :
RingHom.equivRatAlgHom.symm self = self.toRingHom
@[simp]
theorem RingHom.equivRatAlgHom_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [] [] (f : R →+* S) :
RingHom.equivRatAlgHom f = f.toRatAlgHom
def RingHom.equivRatAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [] [] :
(R →+* S) (R →ₐ[] S)

The equivalence between RingHom and ℚ-algebra homomorphisms.

Equations
• RingHom.equivRatAlgHom = { toFun := RingHom.toRatAlgHom, invFun := AlgHom.toRingHom, left_inv := , right_inv := }
Instances For
def Algebra.ofId (R : Type u) (A : Type v) [] [] [Algebra R A] :

AlgebraMap as an AlgHom.

Equations
• = let __src := ; { toRingHom := __src, commutes' := }
Instances For
theorem Algebra.ofId_apply {R : Type u} (A : Type v) [] [] [Algebra R A] (r : R) :
() r = () r
instance Algebra.subsingleton_id {R : Type u} (A : Type v) [] [] [Algebra R A] :

This is a special case of a more general instance that we define in a later file.

Equations
• =
theorem Algebra.ext_id {R : Type u} (A : Type v) [] [] [Algebra R A] (f : R →ₐ[R] A) (g : R →ₐ[R] A) :
f = g

This ext lemma closes trivial subgoals create when chaining heterobasic ext lemmas.

@[simp]
theorem Algebra.smul_units_def {R : Type u} (A : Type v) [] [] [Algebra R A] (f : A →ₐ[R] A) (x : Aˣ) :
f x = () x
theorem Algebra.algebraMapSubmonoid_map_eq {R : Type u} {A : Type v} [] [] [Algebra R A] (M : ) {B : Type w} [] [Algebra R B] (f : A →ₐ[R] B) :
theorem Algebra.algebraMapSubmonoid_le_comap {R : Type u} {A : Type v} [] [] [Algebra R A] (M : ) {B : Type w} [] [Algebra R B] (f : A →ₐ[R] B) :
Submonoid.comap f.toRingHom
@[simp]
theorem MulSemiringAction.toAlgHom_apply {M : Type u_1} (R : Type u_3) (A : Type u_4) [] [] [Algebra R A] [] [] [] (m : M) (a : A) :
() a = m a
def MulSemiringAction.toAlgHom {M : Type u_1} (R : Type u_3) (A : Type u_4) [] [] [Algebra R A] [] [] [] (m : M) :

Each element of the monoid defines an algebra homomorphism.

This is a stronger version of MulSemiringAction.toRingHom and DistribMulAction.toLinearMap.

Equations
• = let __src := ; { toFun := fun (a : A) => m a, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
theorem MulSemiringAction.toAlgHom_injective {M : Type u_1} (R : Type u_3) (A : Type u_4) [] [] [Algebra R A] [] [] [] [] :