mathlib3 documentation

algebra.algebra.hom

Homomorphisms of R-algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines bundled homomorphisms of R-algebras.

Main definitions #

Notations #

source
def alg_hom.to_ring_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (self : A →ₐ[R] B) :
A →+* B

Reinterpret an alg_hom as a ring_hom

source
@[nolint]
structure alg_hom (R : Type u) (A : Type v) (B : Type w) [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
Type (max v w)

Defining the homomorphism in the category R-Alg.

Instances for alg_hom
source
@[nolint, instance]
def alg_hom_class.to_ring_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [self : alg_hom_class F R A B] :
ring_hom_class F A B
source
@[class]
structure alg_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
Type (max u_1 u_3 u_4)

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

Instances of this typeclass
Instances of other typeclasses for alg_hom_class
  • alg_hom_class.has_sizeof_inst
source
@[protected, instance]
def alg_hom_class.linear_map_class {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {F : Type u_4} [alg_hom_class F R A B] :
linear_map_class F R A B
Equations
source
@[protected, instance]
def alg_hom_class.alg_hom.has_coe_t {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {F : Type u_4} [alg_hom_class F R A B] :
has_coe_t F (A →ₐ[R] B)
Equations
source
@[protected, instance]
def alg_hom.has_coe_to_fun {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
has_coe_to_fun (A →ₐ[R] B) (λ (_x : A →ₐ[R] B), A → B)
Equations
source
@[protected, simp]
theorem alg_hom.coe_coe {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {F : Type u_1} [alg_hom_class F R A B] (f : F) :
⇑↑f = ⇑f
source
@[simp]
theorem alg_hom.to_fun_eq_coe {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
f.to_fun = ⇑f
source
@[protected, instance]
def alg_hom.alg_hom_class {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
alg_hom_class (A →ₐ[R] B) R A B
Equations
source
@[protected, instance]
def alg_hom.coe_ring_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
has_coe (A →ₐ[R] B) (A →+* B)
Equations
source
@[protected, instance]
def alg_hom.coe_monoid_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
has_coe (A →ₐ[R] B) (A →* B)
Equations
source
@[protected, instance]
def alg_hom.coe_add_monoid_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
has_coe (A →ₐ[R] B) (A →+ B)
Equations
source
@[simp, norm_cast]
theorem alg_hom.coe_mk {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {f : A → B} (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), f (x * y) = f x * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : A), f (x + y) = f x + f y) (h₅ : ∀ (r : R), f (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r) :
⇑{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅} = f
source
@[simp]
theorem alg_hom.to_ring_hom_eq_coe {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
f.to_ring_hom = ↑f
source
@[simp, norm_cast]
theorem alg_hom.coe_to_ring_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
⇑↑f = ⇑f
source
@[simp, norm_cast]
theorem alg_hom.coe_to_monoid_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
⇑↑f = ⇑f
source
@[simp, norm_cast]
theorem alg_hom.coe_to_add_monoid_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
⇑↑f = ⇑f
source
theorem alg_hom.coe_fn_injective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
function.injective coe_fn
source
theorem alg_hom.coe_fn_inj {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {φ₁ φ₂ : A →ₐ[R] B} :
⇑φ₁ = ⇑φ₂ ↔ φ₁ = φ₂
source
theorem alg_hom.coe_ring_hom_injective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
function.injective coe
source
theorem alg_hom.coe_monoid_hom_injective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
function.injective coe
source
theorem alg_hom.coe_add_monoid_hom_injective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
function.injective coe
source
@[protected]
theorem alg_hom.congr_fun {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {φ₁ φ₂ : A →ₐ[R] B} (H : φ₁ = φ₂) (x : A) :
⇑φ₁ x = ⇑φ₂ x
source
@[protected]
theorem alg_hom.congr_arg {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {x y : A} (h : x = y) :
⇑φ x = ⇑φ y
source
@[ext]
theorem alg_hom.ext {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {φ₁ φ₂ : A →ₐ[R] B} (H : ∀ (x : A), ⇑φ₁ x = ⇑φ₂ x) :
φ₁ = φ₂
source
theorem alg_hom.ext_iff {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {φ₁ φ₂ : A →ₐ[R] B} :
φ₁ = φ₂ ↔ ∀ (x : A), ⇑φ₁ x = ⇑φ₂ x
source
@[simp]
theorem alg_hom.mk_coe {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {f : A →ₐ[R] B} (h₁ : ⇑f 1 = 1) (h₂ : ∀ (x y : A), ⇑f (x * y) = ⇑f x * ⇑f y) (h₃ : ⇑f 0 = 0) (h₄ : ∀ (x y : A), ⇑f (x + y) = ⇑f x + ⇑f y) (h₅ : ∀ (r : R), ⇑f (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r) :
{to_fun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅} = f
source
@[simp]
theorem alg_hom.commutes {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (r : R) :
⇑φ (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r
source
theorem alg_hom.comp_algebra_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
↑φ.comp (algebra_map R A) = algebra_map R B
source
@[protected]
theorem alg_hom.map_add {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (r s : A) :
⇑φ (r + s) = ⇑φ r + ⇑φ s
source
@[protected]
theorem alg_hom.map_zero {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
⇑φ 0 = 0
source
@[protected]
theorem alg_hom.map_mul {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x y : A) :
⇑φ (x * y) = ⇑φ x * ⇑φ y
source
@[protected]
theorem alg_hom.map_one {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
⇑φ 1 = 1
source
@[protected]
theorem alg_hom.map_pow {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x : A) (n : ℕ) :
⇑φ (x ^ n) = ⇑φ x ^ n
source
@[protected, simp]
theorem alg_hom.map_smul {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (r : R) (x : A) :
⇑φ (r • x) = r • ⇑φ x
source
@[protected]
theorem alg_hom.map_sum {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {ι : Type u_1} (f : ι → A) (s : finset ι) :
⇑φ (s.sum (λ (x : ι), f x)) = s.sum (λ (x : ι), ⇑φ (f x))
source
@[protected]
theorem alg_hom.map_finsupp_sum {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {α : Type u_1} [has_zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A) :
⇑φ (f.sum g) = f.sum (λ (i : ι) (a : α), ⇑φ (g i a))
source
@[protected]
theorem alg_hom.map_bit0 {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x : A) :
⇑φ (bit0 x) = bit0 (⇑φ x)
source
@[protected]
theorem alg_hom.map_bit1 {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x : A) :
⇑φ (bit1 x) = bit1 (⇑φ x)
source
def alg_hom.mk' {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →+* B) (h : ∀ (c : R) (x : A), ⇑f (c • x) = c • ⇑f x) :
A →ₐ[R] B

If a ring_hom is R-linear, then it is an alg_hom.

Equations
source
@[simp]
theorem alg_hom.coe_mk' {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →+* B) (h : ∀ (c : R) (x : A), ⇑f (c • x) = c • ⇑f x) :
⇑(alg_hom.mk' f h) = ⇑f
source
@[protected]
def alg_hom.id (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
A →ₐ[R] A

Identity map as an alg_hom.

Equations
source
@[simp]
theorem alg_hom.coe_id (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
⇑(alg_hom.id R A) = id
source
@[simp]
theorem alg_hom.id_to_ring_hom (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
↑(alg_hom.id R A) = ring_hom.id A
source
theorem alg_hom.id_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (p : A) :
⇑(alg_hom.id R A) p = p
source
def alg_hom.comp {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :
A →ₐ[R] C

Composition of algebra homeomorphisms.

Equations
source
@[simp]
theorem alg_hom.coe_comp {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :
⇑(φ₁.comp φ₂) = ⇑φ₁ ∘ ⇑φ₂
source
theorem alg_hom.comp_apply {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) (p : A) :
⇑(φ₁.comp φ₂) p = ⇑φ₁ (⇑φ₂ p)
source
theorem alg_hom.comp_to_ring_hom {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :
↑(φ₁.comp φ₂) = ↑φ₁.comp ↑φ₂
source
@[simp]
theorem alg_hom.comp_id {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
φ.comp (alg_hom.id R A) = φ
source
@[simp]
theorem alg_hom.id_comp {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
(alg_hom.id R B).comp φ = φ
source
theorem alg_hom.comp_assoc {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} {D : Type v₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [semiring D] [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 φ₃)
source
def alg_hom.to_linear_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) :
A →ₗ[R] B

R-Alg ⥤ R-Mod

Equations
Instances for alg_hom.to_linear_map
source
@[simp]
theorem alg_hom.to_linear_map_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (p : A) :
⇑(φ.to_linear_map) p = ⇑φ p
source
theorem alg_hom.to_linear_map_injective {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
function.injective alg_hom.to_linear_map
source
@[simp]
theorem alg_hom.comp_to_linear_map {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [comm_semiring R] [semiring A] [semiring B] [semiring C] [algebra R A] [algebra R B] [algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
(g.comp f).to_linear_map = g.to_linear_map.comp f.to_linear_map
source
@[simp]
theorem alg_hom.to_linear_map_id {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
(alg_hom.id R A).to_linear_map = linear_map.id
source
def alg_hom.of_linear_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [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 →ₐ[R] B

Promote a linear_map to an alg_hom by supplying proofs about the behavior on 1 and *.

Equations
source
@[simp]
theorem alg_hom.of_linear_map_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [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) :
⇑(alg_hom.of_linear_map f map_one map_mul) ᾰ = ⇑f ᾰ
source
@[simp]
theorem alg_hom.of_linear_map_to_linear_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (map_one : ⇑(φ.to_linear_map) 1 = 1) (map_mul : ∀ (x y : A), ⇑(φ.to_linear_map) (x * y) = ⇑(φ.to_linear_map) x * ⇑(φ.to_linear_map) y) :
alg_hom.of_linear_map φ.to_linear_map map_one map_mul = φ
source
@[simp]
theorem alg_hom.to_linear_map_of_linear_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [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) :
(alg_hom.of_linear_map f map_one map_mul).to_linear_map = f
source
@[simp]
theorem alg_hom.of_linear_map_id {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (map_one : ⇑linear_map.id 1 = 1) (map_mul : ∀ (x y : A), ⇑linear_map.id (x * y) = ⇑linear_map.id x * ⇑linear_map.id y) :
alg_hom.of_linear_map linear_map.id map_one map_mul = alg_hom.id R A
source
theorem alg_hom.map_smul_of_tower {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {R' : Type u_1} [has_smul R' A] [has_smul R' B] [linear_map.compatible_smul A B R' R] (r : R') (x : A) :
⇑φ (r • x) = r • ⇑φ x
source
theorem alg_hom.map_list_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (s : list A) :
⇑φ s.prod = (list.map ⇑φ s).prod
source
theorem alg_hom.End_mul {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (φ₁ φ₂ : A →ₐ[R] A) :
φ₁ * φ₂ = φ₁.comp φ₂
source
theorem alg_hom.End_one {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
1 = alg_hom.id R A
source
@[protected, instance]
def alg_hom.End {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
monoid (A →ₐ[R] A)
Equations
source
@[simp]
theorem alg_hom.one_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (x : A) :
⇑1 x = x
source
@[simp]
theorem alg_hom.mul_apply {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (φ ψ : A →ₐ[R] A) (x : A) :
⇑(φ * ψ) x = ⇑φ (⇑ψ x)
source
theorem alg_hom.algebra_map_eq_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) {y : R} {x : A} (h : ⇑(algebra_map R A) y = x) :
⇑(algebra_map R B) y = ⇑f x
source
@[protected]
theorem alg_hom.map_multiset_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (s : multiset A) :
⇑φ s.prod = (multiset.map ⇑φ s).prod
source
@[protected]
theorem alg_hom.map_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {ι : Type u_1} (f : ι → A) (s : finset ι) :
⇑φ (s.prod (λ (x : ι), f x)) = s.prod (λ (x : ι), ⇑φ (f x))
source
@[protected]
theorem alg_hom.map_finsupp_prod {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) {α : Type u_1} [has_zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A) :
⇑φ (f.prod g) = f.prod (λ (i : ι) (a : α), ⇑φ (g i a))
source
@[protected]
theorem alg_hom.map_neg {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [ring A] [ring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x : A) :
⇑φ (-x) = -⇑φ x
source
@[protected]
theorem alg_hom.map_sub {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [ring A] [ring B] [algebra R A] [algebra R B] (φ : A →ₐ[R] B) (x y : A) :
⇑φ (x - y) = ⇑φ x - ⇑φ y
source
def ring_hom.to_nat_alg_hom {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R →+* S) :
R →ₐ[ℕ] S

Reinterpret a ring_hom as an ℕ-algebra homomorphism.

Equations
source
def ring_hom.to_int_alg_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra ℤ R] [algebra ℤ S] (f : R →+* S) :
R →ₐ[ℤ] S

Reinterpret a ring_hom as a ℤ-algebra homomorphism.

Equations
source
def ring_hom.to_rat_alg_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra ℚ R] [algebra ℚ S] (f : R →+* S) :
R →ₐ[ℚ] S

Reinterpret a ring_hom as a ℚ-algebra homomorphism. This actually yields an equivalence, see ring_hom.equiv_rat_alg_hom.

Equations
source
@[simp]
theorem ring_hom.to_rat_alg_hom_to_ring_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra ℚ R] [algebra ℚ S] (f : R →+* S) :
↑(f.to_rat_alg_hom) = f
source
@[simp]
theorem alg_hom.to_ring_hom_to_rat_alg_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra ℚ R] [algebra ℚ S] (f : R →ₐ[ℚ] S) :
↑f.to_rat_alg_hom = f
source
def ring_hom.equiv_rat_alg_hom {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra ℚ R] [algebra ℚ S] :
(R →+* S) ≃ (R →ₐ[ℚ] S)

The equivalence between ring_hom and ℚ-algebra homomorphisms.

Equations
source
@[simp]
theorem ring_hom.equiv_rat_alg_hom_symm_apply {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra ℚ R] [algebra ℚ S] (self : R →ₐ[ℚ] S) :
⇑(ring_hom.equiv_rat_alg_hom.symm) self = self.to_ring_hom
source
@[simp]
theorem ring_hom.equiv_rat_alg_hom_apply {R : Type u_1} {S : Type u_2} [ring R] [ring S] [algebra ℚ R] [algebra ℚ S] (f : R →+* S) :
⇑ring_hom.equiv_rat_alg_hom f = f.to_rat_alg_hom
source
def algebra.of_id (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
R →ₐ[R] A

algebra_map as an alg_hom.

Equations
source
theorem algebra.of_id_apply {R : Type u} (A : Type v) [comm_semiring R] [semiring A] [algebra R A] (r : R) :
⇑(algebra.of_id R A) r = ⇑(algebra_map R A) r
source
def mul_semiring_action.to_alg_hom {M : Type u_1} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [monoid M] [mul_semiring_action M A] [smul_comm_class M R A] (m : M) :
A →ₐ[R] A

Each element of the monoid defines a algebra homomorphism.

This is a stronger version of mul_semiring_action.to_ring_hom and distrib_mul_action.to_linear_map.

Equations
source
@[simp]
theorem mul_semiring_action.to_alg_hom_apply {M : Type u_1} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [monoid M] [mul_semiring_action M A] [smul_comm_class M R A] (m : M) (a : A) :
⇑(mul_semiring_action.to_alg_hom R A m) a = m • a
source
theorem mul_semiring_action.to_alg_hom_injective {M : Type u_1} (R : Type u_3) (A : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [monoid M] [mul_semiring_action M A] [smul_comm_class M R A] [has_faithful_smul M A] :
function.injective (mul_semiring_action.to_alg_hom R A)