Homomorphisms of R
-algebras #
This file defines bundled homomorphisms of R
-algebras.
Main definitions #
AlgHom R A B
: the type ofR
-algebra morphisms fromA
toB
.Algebra.ofId R A : R →ₐ[R] A
: the canonical map fromR
toA
, as anAlgHom
.
Notations #
A →ₐ[R] B
:R
-algebra homomorphism fromA
toB
.
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.
Instances For
Defining the homomorphism in the category R-Alg.
Instances For
Defining the homomorphism in the category R-Alg.
Instances For
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_one : ∀ (f : F), ↑f 1 = 1
- 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
.
Instances
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
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)
:
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
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]
:
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
@[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.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
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_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
@[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_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)
@[simp]
@[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)
:
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 φ₂ φ₃)
@[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.toLinearMap_id
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
AlgHom.toLinearMap (AlgHom.id R A) = LinearMap.id
@[simp]
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)
:
Promote a LinearMap
to an AlgHom
by supplying proofs about the behavior on 1
and *
.
Instances For
@[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.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]
:
@[simp]
theorem
AlgHom.one_apply
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(x : A)
:
↑1 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)
AlgebraMap
as an AlgHom
.
Instances For
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)
:
Each element of the monoid defines an algebra homomorphism.
This is a stronger version of MulSemiringAction.toRingHom
and
DistribMulAction.toLinearMap
.
Instances For
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]
: