Tensor products of algebra maps as linear maps #
The tensor product Algebra.TensorProduct.map f g of two algebra maps is, as a function, the
tensor product TensorProduct.map of their underlying linear maps. This file records that
identity pointwise, and its consequence for a tensor product of linear maps applied after a tensor
product of algebra maps: the result is the tensor product of the two composites. These are the
forms needed to evaluate linear functionals on one tensor factor after an algebra map has been
applied to the other.
theorem
Algebra.TensorProduct.map_apply_eq_map
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{C : Type u_4}
{D : Type u_5}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Semiring C]
[Semiring D]
[Algebra R A]
[Algebra R B]
[Algebra R C]
[Algebra R D]
(f : A →ₐ[R] C)
(g : B →ₐ[R] D)
(z : TensorProduct R A B)
:
The tensor product of two algebra maps acts as the tensor product of their underlying linear maps.
theorem
TensorProduct.map_algebraTensorProduct_map
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{C : Type u_4}
{D : Type u_5}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Semiring C]
[Semiring D]
[Algebra R A]
[Algebra R B]
[Algebra R C]
[Algebra R D]
{M : Type u_6}
{N : Type u_7}
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
(f₂ : C →ₗ[R] M)
(g₂ : D →ₗ[R] N)
(f₁ : A →ₐ[R] C)
(g₁ : B →ₐ[R] D)
(z : TensorProduct R A B)
:
(map f₂ g₂) ((Algebra.TensorProduct.map f₁ g₁) z) = (map (f₂ ∘ₗ f₁.toLinearMap) (g₂ ∘ₗ g₁.toLinearMap)) z
A tensor product of linear maps applied after a tensor product of algebra maps is the tensor product of the two composites.