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 #
alg_hom R A B
: the type ofR
-algebra morphisms fromA
toB
.algebra.of_id R A : R →ₐ[R] A
: the canonical map fromR
toA
, as analg_hom
.
Notations #
@[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
@[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
@[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
@[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ₛₗ := _}
@[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] :
@[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] :
Equations
- alg_hom.has_coe_to_fun = {coe := alg_hom.to_fun _inst_7}
@[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 := _}
@[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] :
Equations
- alg_hom.coe_ring_hom = {coe := alg_hom.to_ring_hom _inst_7}
@[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) :
@[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
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] :
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] :
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] :
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] :
@[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) :
@[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
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
@[protected]
@[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
@[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
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
@[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) = φ
@[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 φ = φ
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] :
@[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
@[simp]
theorem
alg_hom.to_linear_map_id
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
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) :
Promote a linear_map
to an alg_hom
by supplying proofs about the behavior on 1
and *
.
@[simp]
@[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 = φ
@[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
@[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
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
@[protected, instance]
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' := _}
@[simp]
theorem
alg_hom.one_apply
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A) :
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
@[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) :
@[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 ι) :
@[protected]
def
ring_hom.equiv_rat_alg_hom
{R : Type u_1}
{S : Type u_2}
[ring R]
[ring S]
[algebra ℚ R]
[algebra ℚ 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 := _}
algebra_map
as an alg_hom
.
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
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) :
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
.
@[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
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] :