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) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] extends RingHom : Type (max v w)

• toFun : A → B
• map_one' : OneHom.toFun (↑↑↑s) 1 = 1
• map_mul' : ∀ (x y : A), OneHom.toFun (↑↑↑s) (x * y) = OneHom.toFun (↑↑↑s) x * OneHom.toFun (↑↑↑s) y
• map_zero' : OneHom.toFun (↑↑↑s) 0 = 0
• map_add' : ∀ (x y : A), OneHom.toFun (↑↑↑s) (x + y) = OneHom.toFun (↑↑↑s) x + OneHom.toFun (↑↑↑s) y
• commutes' : ∀ (r : R), OneHom.toFun (↑↑↑s) (↑(algebraMap R A) r) = ↑(algebraMap R B) r

Defining the homomorphism in the category R-Alg.

def «term_→ₐ_» : Lean.TrailingParserDescr

Defining the homomorphism in the category R-Alg.

Equations

• «term_→ₐ_» = Lean.ParserDescr.trailingNode `term_→ₐ_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₐ ") (Lean.ParserDescr.cat `term 25))

def «term_→ₐ[_]_» : Lean.TrailingParserDescr

Defining the homomorphism in the category R-Alg.

Equations

• One or more equations did not get rendered due to their size.

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] extends RingHomClass : Type (max (max u_1 u_3) u_4)

• coe : F → A → B
• coe_injective' : Function.Injective FunLike.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 (↑(algebraMap R A) r) = ↑(algebraMap R B) r

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

instance AlgHomClass.linearMapClass {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} [AlgHomClass F R A B] : LinearMapClass F R A B

Equations

• AlgHomClass.linearMapClass = let src := inst; SemilinearMapClass.mk (_ : ∀ (f : F) (r : R) (x : A), ↑f (r • x) = r • ↑f x)

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_4} [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 α →+* β.

Equations

• One or more equations did not get rendered due to their size.

instance AlgHomClass.coeTC {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} [AlgHomClass F R A B] : CoeTC F (A →ₐ[R] B)

Equations

• AlgHomClass.coeTC = { coe := AlgHomClass.toAlgHom }

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

Equations

• AlgHom.algHomClass = AlgHomClass.mk (_ : ∀ (f : A →ₐ[R] B) (r : R), OneHom.toFun (↑↑↑f) (↑(algebraMap R A) r) = ↑(algebraMap R B) r)

def AlgHom.Simps.apply {R : Type u_1} {α : Type u_2} {β : Type u_3} [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α →ₐ[R] β) : α → β

See Note [custom simps projection]

Equations

• AlgHom.Simps.apply f = ↑f

@[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} [AlgHomClass F R A B] (f : F) : ↑↑f = ↑f

@[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.toFun = ↑f

instance AlgHom.coeOutRingHom {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)

Equations

• AlgHom.coeOutRingHom = { coe := AlgHom.toRingHom }

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

Equations

• ↑f = ↑↑f

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)

Equations

• AlgHom.coeOutMonoidHom = { coe := AlgHom.toMonoidHom' }

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

Equations

• ↑f = ↑↑f

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)

Equations

• AlgHom.coeOutAddMonoidHom = { coe := AlgHom.toAddMonoidHom' }

@[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), OneHom.toFun (↑↑f) (↑(algebraMap R A) r) = ↑(algebraMap R B) r) : ↑{ toRingHom := f, commutes' := h } = ↑f

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), OneHom.toFun { toFun := f, map_one' := h₁ } (x * y) = OneHom.toFun { toFun := f, map_one' := h₁ } x * OneHom.toFun { toFun := f, map_one' := h₁ } y) (h₃ : OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0) (h₄ : ∀ (x y : A), OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) (x + y) = OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) x + OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) y) (h₅ : ∀ (r : R), OneHom.toFun (↑↑{ toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }) (↑(algebraMap R A) r) = ↑(algebraMap R B) r) : ↑{ toRingHom := { toMonoidHom := { toOneHom := { 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} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {f : A →+* B} (h : ∀ (r : R), OneHom.toFun (↑↑f) (↑(algebraMap R A) r) = ↑(algebraMap R B) r) : ↑{ toRingHom := f, commutes' := h } = f

@[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 = ↑f

@[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

@[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

@[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

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 FunLike.coe

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} {φ₂ : A →ₐ[R] B} : ↑φ₁ = ↑φ₂ ↔ φ₁ = φ₂

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

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

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

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} {φ₂ : A →ₐ[R] B} (H : φ₁ = φ₂) (x : A) : ↑φ₁ x = ↑φ₂ x

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 : A} {y : A} (h : x = y) : ↑φ x = ↑φ y

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} {φ₂ : A →ₐ[R] B} (H : ∀ (x : A), ↑φ₁ x = ↑φ₂ x) : φ₁ = φ₂

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} {φ₂ : A →ₐ[R] B} : φ₁ = φ₂ ↔ ∀ (x : A), ↑φ₁ x = ↑φ₂ x

@[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), OneHom.toFun { toFun := ↑f, map_one' := h₁ } (x * y) = OneHom.toFun { toFun := ↑f, map_one' := h₁ } x * OneHom.toFun { toFun := ↑f, map_one' := h₁ } y) (h₃ : OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0) (h₄ : ∀ (x y : A), OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) (x + y) = OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) x + OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) y) (h₅ : ∀ (r : R), OneHom.toFun (↑↑{ toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }) (↑(algebraMap R A) r) = ↑(algebraMap R B) r) : { toRingHom := { toMonoidHom := { toOneHom := { 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} [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

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) : RingHom.comp (↑φ) (algebraMap R A) = algebraMap R B

theorem AlgHom.map_add {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 : A) (s : A) : ↑φ (r + s) = ↑φ r + ↑φ s

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

theorem AlgHom.map_mul {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) (y : A) : ↑φ (x * y) = ↑φ x * ↑φ y

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

theorem AlgHom.map_pow {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) (n : ℕ) : ↑φ (x ^ n) = ↑φ x ^ n

theorem AlgHom.map_smul {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) (x : A) : ↑φ (r • x) = r • ↑φ x

theorem AlgHom.map_sum {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {ι : Type u_1} (f : ι → A) (s : Finset ι) : ↑φ (Finset.sum s fun x => f x) = Finset.sum s fun x => ↑φ (f x)

theorem AlgHom.map_finsupp_sum {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {α : Type u_1} [Zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A) : ↑φ (Finsupp.sum f g) = Finsupp.sum f fun i a => ↑φ (g i a)

theorem AlgHom.map_bit0 {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) : ↑φ (bit0 x) = bit0 (↑φ x)

theorem AlgHom.map_bit1 {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) : ↑φ (bit1 x) = bit1 (↑φ x)

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.

Equations

• One or more equations did not get rendered due to their size.

@[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) : ↑(AlgHom.mk' f h) = ↑f

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

Identity map as an AlgHom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[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

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

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

Composition of algebra homeomorphisms.

Equations

• One or more equations did not get rendered due to their size.

@[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) : ↑(AlgHom.comp φ₁ φ₂) = ↑φ₁ ∘ ↑φ₂

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) : ↑(AlgHom.comp φ₁ φ₂) p = ↑φ₁ (↑φ₂ p)

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) : ↑(AlgHom.comp φ₁ φ₂) = RingHom.comp ↑φ₁ ↑φ₂

@[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) : AlgHom.comp φ (AlgHom.id R A) = φ

@[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.comp (AlgHom.id R B) φ = φ

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) : AlgHom.comp (AlgHom.comp φ₁ φ₂) φ₃ = AlgHom.comp φ₁ (AlgHom.comp φ₂ φ₃)

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

Equations

• AlgHom.toLinearMap φ = { toAddHom := { toFun := ↑φ, map_add' := (_ : ∀ (x y : A), ↑φ (x + y) = ↑φ x + ↑φ y) }, map_smul' := (_ : ∀ (c : R) (x : A), ↑φ (c • x) = c • ↑φ x) }

@[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) : ↑(AlgHom.toLinearMap φ) p = ↑φ p

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 AlgHom.toLinearMap

@[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) : AlgHom.toLinearMap (AlgHom.comp g f) = LinearMap.comp (AlgHom.toLinearMap g) (AlgHom.toLinearMap f)

@[simp]

theorem AlgHom.toLinearMap_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : AlgHom.toLinearMap (AlgHom.id R A) = LinearMap.id

@[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) : ↑(AlgHom.ofLinearMap f map_one map_mul) a = ↑f a

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 *.

Equations

• One or more equations did not get rendered due to their size.

@[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 : ↑(AlgHom.toLinearMap φ) 1 = 1) (map_mul : ∀ (x y : A), ↑(AlgHom.toLinearMap φ) (x * y) = ↑(AlgHom.toLinearMap φ) x * ↑(AlgHom.toLinearMap φ) y) : AlgHom.ofLinearMap (AlgHom.toLinearMap φ) map_one map_mul = φ

@[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) : AlgHom.toLinearMap (AlgHom.ofLinearMap f map_one map_mul) = f

@[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) : AlgHom.ofLinearMap LinearMap.id map_one map_mul = AlgHom.id R A

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

theorem AlgHom.map_list_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (s : List A) : ↑φ (List.prod s) = List.prod (List.map (↑φ) s)

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

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

instance AlgHom.End {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : Monoid (A →ₐ[R] A)

Equations

• AlgHom.End = Monoid.mk (_ : ∀ (ϕ : A →ₐ[R] A), 1 * ϕ = ϕ) (_ : ∀ (ϕ : A →ₐ[R] A), ϕ * 1 = ϕ) npowRec

@[simp]

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

@[simp]

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

theorem AlgHom.map_multiset_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (s : Multiset A) : ↑φ (Multiset.prod s) = Multiset.prod (Multiset.map (↑φ) s)

theorem AlgHom.map_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {ι : Type u_1} (f : ι → A) (s : Finset ι) : ↑φ (Finset.prod s fun x => f x) = Finset.prod s fun x => ↑φ (f x)

theorem AlgHom.map_finsupp_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {α : Type u_1} [Zero α] {ι : Type u_2} (f : ι →₀ α) (g : ι → α → A) : ↑φ (Finsupp.prod f g) = Finsupp.prod f fun i a => ↑φ (g i a)

theorem AlgHom.map_neg {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (x : A) : ↑φ (-x) = -↑φ x

theorem AlgHom.map_sub {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [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} [Semiring R] [Semiring S] (f : R →+* S) : R →ₐ[ℕ] S

Reinterpret a RingHom as an ℕ-algebra homomorphism.

Equations

• One or more equations did not get rendered due to their size.

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

Reinterpret a RingHom as a ℤ-algebra homomorphism.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RingHom.toRatAlgHom_toRingHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) : ↑(RingHom.toRatAlgHom f) = f

@[simp]

theorem AlgHom.toRingHom_toRatAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →ₐ[ℚ] S) : RingHom.toRatAlgHom ↑f = f

@[simp]

theorem RingHom.equivRatAlgHom_symm_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (self : R →ₐ[ℚ] S) : ↑RingHom.equivRatAlgHom.symm self = ↑self

@[simp]

theorem RingHom.equivRatAlgHom_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) : ↑RingHom.equivRatAlgHom f = RingHom.toRatAlgHom f

def RingHom.equivRatAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] : (R →+* S) ≃ (R →ₐ[ℚ] S)

The equivalence between RingHom and ℚ-algebra homomorphisms.

Equations

• One or more equations did not get rendered due to their size.

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

AlgebraMap as an AlgHom.

Equations

• One or more equations did not get rendered due to their size.

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

@[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) : ↑(MulSemiringAction.toAlgHom R A m) a = m • a

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 DistribMulAction.toLinearMap.

Equations

• One or more equations did not get rendered due to their size.

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 (MulSemiringAction.toAlgHom R A)