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.

Notation #

A →ₐ[R] B : R-algebra homomorphism from A to 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 A →+* B :

Type (max v w)

Defining the homomorphism in the category R-Alg, denoted A →ₐ[R] B.

toFun : A → B
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 ((algebraMap R A) r) = (algebraMap R B) r

Instances For

source

def «term_→ₐ_» :

Lean.TrailingParserDescr

Defining the homomorphism in the category R-Alg, denoted A →ₐ[R] B.

Instances For

source

def «term_→ₐ[_]_» :

Lean.TrailingParserDescr

Defining the homomorphism in the category R-Alg, denoted A →ₐ[R] B.

Instances For

source

class AlgHomClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FunLike F A B] extends RingHomClass F A B :

Prop

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 ((algebraMap R A) r) = (algebraMap R B) r

Instances

source

@[instance 100]

instance AlgHomClass.linearMapClass {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] :

LinearMapClass F R A B

source

def AlgHomClass.toAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {F : Type u_5} [FunLike F A B] [AlgHomClass F R A B] (f : F) :

A →ₐ[R] B

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

Instances For

source

@[implicit_reducible]

instance AlgHom.funLike {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

FunLike (A →ₐ[R] B) A B

source

instance AlgHom.algHomClass {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

AlgHomClass (A →ₐ[R] B) R A B

source

@[simp]

theorem AlgHomClass.toLinearMap_toAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] (f : F) :

↑↑f = ↑f

source

def AlgHom.Simps.apply {R : Type u} {α : Type v} {β : Type w} [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α →ₐ[R] β) :

α → β

See Note [custom simps projection]

Instances For

source

@[simp]

theorem AlgHom.coe_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {F : Type u_1} [FunLike F A B] [AlgHomClass F R A B] (f : F) :

⇑↑f = ⇑f

source

@[simp]

theorem AlgHom.toFun_eq_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

(↑↑f.toRingHom).toFun = ⇑f

source

def AlgHom.toMonoidHom' {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

A →* B

Turn an algebra homomorphism into the corresponding multiplicative monoid homomorphism.

Instances For

source

@[implicit_reducible]

instance AlgHom.coeOutMonoidHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

CoeOut (A →ₐ[R] B) (A →* B)

source

def AlgHom.toAddMonoidHom' {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

A →+ B

Turn an algebra homomorphism into the corresponding additive monoid homomorphism.

Instances For

source

@[implicit_reducible]

instance AlgHom.coeOutAddMonoidHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

CoeOut (A →ₐ[R] B) (A →+ B)

source

@[simp]

theorem AlgHom.coe_mk {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {f : A →+* B} (h : ∀ (r : R), (↑↑f).toFun ((algebraMap R A) r) = (algebraMap R B) r) :

⇑{ toRingHom := f, commutes' := h } = ⇑f

source

theorem AlgHom.coe_mks {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {f : A → 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 ((algebraMap R A) r) = (algebraMap R B) r) :

⇑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ } = f

source

@[simp]

theorem AlgHom.coe_ringHom_mk {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {f : A →+* B} (h : ∀ (r : R), (↑↑f).toFun ((algebraMap R A) r) = (algebraMap R B) r) :

↑{ toRingHom := f, commutes' := h } = f

source

@[simp]

theorem AlgHom.toRingHom_eq_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

f.toRingHom = ↑f

source

@[simp]

theorem AlgHom.coe_toRingHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

⇑↑f = ⇑f

source

@[simp]

theorem AlgHom.coe_toMonoidHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

⇑↑f = ⇑f

source

@[simp]

theorem AlgHom.coe_toAddMonoidHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

⇑↑f = ⇑f

source

@[simp]

theorem AlgHom.toRingHom_toMonoidHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

↑↑f = ↑f

source

@[simp]

theorem AlgHom.toRingHom_toAddMonoidHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

↑↑f = ↑f

source

theorem AlgHom.coe_fn_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

Function.Injective DFunLike.coe

source

theorem AlgHom.coe_fn_inj {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {φ₁ φ₂ : A →ₐ[R] B} :

⇑φ₁ = ⇑φ₂ ↔ φ₁ = φ₂

source

theorem AlgHom.coe_ringHom_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

Function.Injective RingHomClass.toRingHom

source

theorem AlgHom.coe_monoidHom_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

Function.Injective MonoidHomClass.toMonoidHom

source

theorem AlgHom.coe_addMonoidHom_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

Function.Injective AddMonoidHomClass.toAddMonoidHom

source

theorem AlgHom.congr_fun {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {φ₁ φ₂ : A →ₐ[R] B} (H : φ₁ = φ₂) (x : A) :

φ₁ x = φ₂ x

source

theorem AlgHom.congr_arg {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {x y : A} (h : x = y) :

φ x = φ y

source

theorem AlgHom.ext {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {φ₁ φ₂ : A →ₐ[R] B} (H : ∀ (x : A), φ₁ x = φ₂ x) :

φ₁ = φ₂

source

theorem AlgHom.ext_iff {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {φ₁ φ₂ : A →ₐ[R] B} :

φ₁ = φ₂ ↔ ∀ (x : A), φ₁ x = φ₂ x

source

@[simp]

theorem AlgHom.mk_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [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 ((algebraMap R A) r) = (algebraMap R B) r) :

{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ } = f

source

@[simp]

theorem AlgHom.addHomMk_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

{ toFun := ⇑f, map_add' := ⋯ } = ↑f

source

@[simp]

theorem AlgHom.commutes {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (r : R) :

φ ((algebraMap R A) r) = (algebraMap R B) r

source

theorem AlgHom.comp_algebraMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :

(↑φ).comp (algebraMap R A) = algebraMap R B

source

def AlgHom.mk' {R : Type u} {A : Type v} {B : Type w} [CommSemiring 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 RingHom is R-linear, then it is an AlgHom.

Instances For

source

@[simp]

theorem AlgHom.coe_mk' {R : Type u} {A : Type v} {B : Type w} [CommSemiring 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) :

⇑(mk' f h) = ⇑f

source

def AlgHom.id (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :

A →ₐ[R] A

Identity map as an AlgHom.

Instances For

source

@[simp]

theorem AlgHom.coe_id (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :

⇑(AlgHom.id R A) = id

source

@[simp]

theorem AlgHom.id_toRingHom (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :

↑(AlgHom.id R A) = RingHom.id A

source

theorem AlgHom.id_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (p : A) :

(AlgHom.id R A) p = p

source

def AlgHom.comp {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring 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

If φ₁ and φ₂ are R-algebra homomorphisms with the domain of φ₁ equal to the codomain of φ₂, then φ₁.comp φ₂ is the algebra homomorphism x ↦ φ₁ (φ₂ x).

Instances For

source

@[simp]

theorem AlgHom.coe_comp {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring 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 AlgHom.comp_apply {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring 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 AlgHom.comp_toRingHom {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring 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 AlgHom.comp_id {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :

φ.comp (AlgHom.id R A) = φ

source

@[simp]

theorem AlgHom.id_comp {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :

(AlgHom.id R B).comp φ = φ

source

theorem AlgHom.comp_assoc {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} {D : Type v₁} [CommSemiring 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

instance AlgHom.instRingHomCompTripleComp {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] {φ₁ : B →ₐ[R] C} {φ₂ : A →ₐ[R] B} :

RingHomCompTriple φ₂.toRingHom φ₁.toRingHom (φ₁.comp φ₂).toRingHom

source

def AlgHom.toLinearMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :

A →ₗ[R] B

R-Alg ⥤ R-Mod

Instances For

source

@[simp]

theorem AlgHom.toLinearMap_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (p : A) :

φ.toLinearMap p = φ p

source

@[simp]

theorem AlgHom.coe_toLinearMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :

⇑φ.toLinearMap = ⇑φ

source

theorem AlgHom.toLinearMap_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

Function.Injective toLinearMap

source

@[simp]

theorem AlgHom.comp_toLinearMap {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring 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).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

source

@[simp]

theorem AlgHom.toLinearMap_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

(AlgHom.id R A).toLinearMap = LinearMap.id

source

@[simp]

theorem AlgHom.linearMapMk_toAddHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

{ toAddHom := ↑f, map_smul' := ⋯ } = f.toLinearMap

source

def AlgHom.ofLinearMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring 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 LinearMap to an AlgHom by supplying proofs about the behavior on 1 and *.

Instances For

source

@[simp]

theorem AlgHom.ofLinearMap_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring 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 : A) :

(ofLinearMap f map_one map_mul) a = f a

source

@[simp]

theorem AlgHom.ofLinearMap_toLinearMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [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) :

ofLinearMap φ.toLinearMap map_one map_mul = φ

source

@[simp]

theorem AlgHom.toLinearMap_ofLinearMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring 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) :

(ofLinearMap f map_one map_mul).toLinearMap = f

source

@[simp]

theorem AlgHom.ofLinearMap_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (map_one : LinearMap.id 1 = 1) (map_mul : ∀ (x y : A), LinearMap.id (x * y) = LinearMap.id x * LinearMap.id y) :

ofLinearMap LinearMap.id map_one map_mul = AlgHom.id R A

source

theorem AlgHom.map_smul_of_tower {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {R' : Type u_1} [SMul R' A] [SMul R' B] [LinearMap.CompatibleSMul A B R' R] (r : R') (x : A) :

φ (r • x) = r • φ x

source

@[implicit_reducible]

instance AlgHom.End {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

Monoid (A →ₐ[R] A)

source

theorem AlgHom.End_toSemigroup_toMul_mul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (φ₁ φ₂ : A →ₐ[R] A) :

φ₁ * φ₂ = φ₁.comp φ₂

source

theorem AlgHom.End_toOne_one {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

1 = AlgHom.id R A

source

@[simp]

theorem AlgHom.one_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) :

1 x = x

source

@[simp]

theorem AlgHom.mul_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (φ ψ : A →ₐ[R] A) (x : A) :

(φ * ψ) x = φ (ψ x)

source

@[simp]

theorem AlgHom.coe_pow {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (φ : A →ₐ[R] A) (n : ℕ) :

⇑(φ ^ n) = (⇑φ)^[n]

source

theorem AlgHom.algebraMap_eq_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) {y : R} {x : A} (h : (algebraMap R A) y = x) :

(algebraMap R B) y = f x

source

theorem AlgHom.cancel_right {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] {g₁ g₂ : B →ₐ[R] C} {f : A →ₐ[R] B} (hf : Function.Surjective ⇑f) :

g₁.comp f = g₂.comp f ↔ g₁ = g₂

source

theorem AlgHom.cancel_left {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] {g₁ g₂ : A →ₐ[R] B} {f : B →ₐ[R] C} (hf : Function.Injective ⇑f) :

f.comp g₁ = f.comp g₂ ↔ g₁ = g₂

source

def AlgHom.toEnd {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

(A →ₐ[R] A) →* Module.End R A

AlgHom.toLinearMap as a MonoidHom.

Instances For

source

@[simp]

theorem AlgHom.toEnd_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (φ : A →ₐ[R] A) :

toEnd φ = φ.toLinearMap

source

def IsScalarTower.toAlgHom (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] :

S →ₐ[R] A

In a tower, the canonical map from the middle element to the top element is an algebra homomorphism over the bottom element.

Instances For

source

theorem IsScalarTower.toAlgHom_apply (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (y : S) :

(toAlgHom R S A) y = (algebraMap S A) y

source

@[simp]

theorem IsScalarTower.coe_toAlgHom (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] :

↑(toAlgHom R S A) = algebraMap S A

source

@[simp]

theorem IsScalarTower.coe_toAlgHom' (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] :

⇑(toAlgHom R S A) = ⇑(algebraMap S A)

source

def Algebra.algHom (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] :

S →ₐ[R] A

The algebra morphism underlying algebraMap.

Instances For

source

theorem Algebra.algHom_apply (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (y : S) :

(IsScalarTower.toAlgHom R S A) y = (algebraMap S A) y

Alias of IsScalarTower.toAlgHom_apply.

source

@[simp]

theorem AlgHomClass.toRingHom_toAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {F : Type u_4} [FunLike F A B] [AlgHomClass F R A B] (f : F) :

↑↑f = ↑f

source

def RingHom.toNatAlgHom {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) :

R →ₐ[ℕ ] S

Reinterpret a RingHom as an ℕ-algebra homomorphism.

Instances For

source

@[simp]

theorem RingHom.toNatAlgHom_coe {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) :

⇑f.toNatAlgHom = ⇑f

source

theorem RingHom.toNatAlgHom_apply {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (x : R) :

f.toNatAlgHom x = f x

source

def RingHom.toIntAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) :

R →ₐ[ℤ ] S

Reinterpret a RingHom as a ℤ-algebra homomorphism.

Instances For

source

@[simp]

theorem RingHom.toIntAlgHom_coe {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) :

⇑f.toIntAlgHom = ⇑f

source

theorem RingHom.toIntAlgHom_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (x : R) :

f.toIntAlgHom x = f x

source

theorem RingHom.toIntAlgHom_injective {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] :

Function.Injective toIntAlgHom

source

def Algebra.ofId (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :

R →ₐ[R] A

AlgebraMap as an AlgHom.

Instances For

source

@[simp]

theorem Algebra.ofId_self {R : Type u} [CommSemiring R] :

ofId R R = AlgHom.id R R

source

@[simp]

theorem Algebra.toRingHom_ofId {R : Type u} (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :

↑(ofId R A) = algebraMap R A

source

@[simp]

theorem Algebra.ofId_apply {R : Type u} (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :

(ofId R A) r = (algebraMap R A) r

source

instance Algebra.subsingleton_id {R : Type u} (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :

Subsingleton (R →ₐ[R] A)

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

source

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

f = g

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

source

theorem Algebra.ext_id_iff {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {f g : R →ₐ[R] A} :

f = g ↔ True

source

@[simp]

theorem Algebra.comp_ofId {R : Type u} (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) :

φ.comp (ofId R A) = ofId R B

source

@[implicit_reducible]

instance Algebra.instMulDistribMulActionAlgHomUnits {R : Type u} (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :

MulDistribMulAction (A →ₐ[R] A) Aˣ

source

@[simp]

theorem Algebra.smul_units_def {R : Type u} (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] (f : A →ₐ[R] A) (x : Aˣ) :

f • x = (Units.map ↑f) x

source

theorem Algebra.algebraMapSubmonoid_map_eq {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (M : Submonoid R) {B : Type w} [Semiring B] [Algebra R B] (f : A →ₐ[R] B) :

Submonoid.map f (algebraMapSubmonoid A M) = algebraMapSubmonoid B M

source

theorem Algebra.algebraMapSubmonoid_le_comap {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (M : Submonoid R) {B : Type w} [Semiring B] [Algebra R B] (f : A →ₐ[R] B) :

algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (algebraMapSubmonoid B M)

source

def MulSemiringAction.toAlgHom {M : Type u_1} (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [MulSemiringAction M A] [SMulCommClass M R A] (m : M) :

A →ₐ[R] A

Each element of the monoid defines an algebra homomorphism.

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

Instances For

source

@[simp]

theorem MulSemiringAction.toAlgHom_apply {M : Type u_1} (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [MulSemiringAction M A] [SMulCommClass M R A] (m : M) (a : A) :

(toAlgHom R A m) a = m • a

source

theorem MulSemiringAction.toAlgHom_injective {M : Type u_1} (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [MulSemiringAction M A] [SMulCommClass M R A] [FaithfulSMul M A] :

Function.Injective (toAlgHom R A)

source

@[implicit_reducible]

instance uniqueOfRight {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [Semiring S] [Semiring T] [Algebra R S] [Algebra R T] [Subsingleton T] :

Unique (S →ₐ[R] T)

source

@[simp]

theorem AlgHom.default_apply {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [Semiring S] [Semiring T] [Algebra R S] [Algebra R T] [Subsingleton T] (x : S) :

default x = 0

Documentation

Mathlib.Algebra.Algebra.Hom

Homomorphisms of `R`-algebras #

Main definitions #

Notation #

Homomorphisms of R-algebras #

Main definitions #

Notation #

Homomorphisms of `R`-algebras #