algebra.algebra.hom - mathlib docs

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)

to_fun : A → B
map_one' : self.to_fun 1 = 1
map_mul' : ∀ (x y : A), self.to_fun (x * y) = self.to_fun x * self.to_fun y
map_zero' : self.to_fun 0 = 0
map_add' : ∀ (x y : A), self.to_fun (x + y) = self.to_fun x + self.to_fun y
commutes' : ∀ (r : R), self.to_fun (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r

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)

coe : F → Π (a : A), (λ (_x : A), B) a
coe_injective' : function.injective alg_hom_class.coe
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 (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r

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

alg_hom_class.linear_map_class = {coe := alg_hom_class.coe _inst_6, coe_injective' := _, map_add := _, map_smulₛₗ := _}

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

alg_hom_class.alg_hom.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}}

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

alg_hom.has_coe_to_fun = {coe := alg_hom.to_fun _inst_7}

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

alg_hom.alg_hom_class = {coe := alg_hom.to_fun _inst_7, coe_injective' := _, map_mul := _, map_one := _, map_add := _, map_zero := _, commutes := _}

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

alg_hom.coe_ring_hom = {coe := alg_hom.to_ring_hom _inst_7}

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

alg_hom.coe_monoid_hom = {coe := λ (f : A →ₐ[R] B), ↑↑f}

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

alg_hom.coe_add_monoid_hom = {coe := λ (f : A →ₐ[R] B), ↑↑f}

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

alg_hom.mk' f h = {to_fun := ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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

alg_hom.id R A = {to_fun := (ring_hom.id A).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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

φ₁.comp φ₂ = {to_fun := (φ₁.to_ring_hom.comp ↑φ₂).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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

φ.to_linear_map = {to_fun := ⇑φ, map_add' := _, map_smul' := _}

Instances for alg_hom.to_linear_map

algebraic_geometry.structure_sheaf.is_localized_module_to_pushforward_stalk_alg_hom

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

alg_hom.of_linear_map f map_one map_mul = {to_fun := ⇑f, map_one' := map_one, map_mul' := map_mul, map_zero' := _, map_add' := _, commutes' := _}

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

alg_hom.End = {mul := alg_hom.comp _inst_6, mul_assoc := _, one := alg_hom.id R A _inst_6, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (A →ₐ[R] A)), npow_zero' := _, npow_succ' := _}

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

f.to_nat_alg_hom = {to_fun := ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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

f.to_int_alg_hom = {to_fun := f.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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

f.to_rat_alg_hom = {to_fun := f.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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

ring_hom.equiv_rat_alg_hom = {to_fun := ring_hom.to_rat_alg_hom _inst_4, inv_fun := alg_hom.to_ring_hom _inst_4, left_inv := _, right_inv := _}

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

algebra.of_id R A = {to_fun := (algebra_map R A).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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

mul_semiring_action.to_alg_hom R A m = {to_fun := λ (a : A), m • a, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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)

mathlib documentation

Homomorphisms of `R`-algebras #

Main definitions #

Notations #

Homomorphisms of R-algebras #

Main definitions #

Notations #

Homomorphisms of `R`-algebras #