mathlib3 documentation

ring_theory.tensor_product

The tensor product of R-algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Let R be a (semi)ring and A an R-algebra. In this file we:

Main declaration #

Implementation notes #

The heterobasic definitions below such as:

are just more general versions of the definitions already in linear_algebra/tensor_product. We could thus consider replacing the less general definitions with these ones. If we do this, we probably should still implement the less general ones as abbreviations to the more general ones with fewer type arguments.

The A-module structure on A ⊗[R] M #

source
theorem tensor_product.algebra_tensor_module.smul_eq_lsmul_rtensor {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] (a : A) (x : tensor_product R M N) :
a • x = ⇑(linear_map.rtensor N (⇑(algebra.lsmul R M) a)) x
source
def tensor_product.algebra_tensor_module.curry {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] (f : tensor_product R M N →ₗ[A] P) :
M →ₗ[A] N →ₗ[R] P

Heterobasic version of tensor_product.curry:

Given a linear map M ⊗[R] N →[A] P, compose it with the canonical bilinear map M →[A] N →[R] M ⊗[R] N to form a bilinear map M →[A] N →[R] P.

Equations
source
@[simp]
theorem tensor_product.algebra_tensor_module.curry_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] (f : tensor_product R M N →ₗ[A] P) (ᾰ : M) :
⇑(tensor_product.algebra_tensor_module.curry f) ᾰ = ⇑(tensor_product.curry (linear_map.restrict_scalars R f)) ᾰ
source
theorem tensor_product.algebra_tensor_module.restrict_scalars_curry {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] (f : tensor_product R M N →ₗ[A] P) :
linear_map.restrict_scalars R (tensor_product.algebra_tensor_module.curry f) = tensor_product.algebra_tensor_module.curry (linear_map.restrict_scalars R f)
source
@[ext]
theorem tensor_product.algebra_tensor_module.curry_injective {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] :
function.injective tensor_product.algebra_tensor_module.curry

Just as tensor_product.ext is marked ext instead of tensor_product.ext', this is a better ext lemma than tensor_product.algebra_tensor_module.ext below.

See note [partially-applied ext lemmas].

source
theorem tensor_product.algebra_tensor_module.ext {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] {g h : tensor_product R M N →ₗ[A] P} (H : ∀ (x : M) (y : N), ⇑g (x ⊗ₜ[R] y) = ⇑h (x ⊗ₜ[R] y)) :
g = h
source
def tensor_product.algebra_tensor_module.lift {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] (f : M →ₗ[A] N →ₗ[R] P) :
tensor_product R M N →ₗ[A] P

Heterobasic version of tensor_product.lift:

Constructing a linear map M ⊗[R] N →[A] P given a bilinear map M →[A] N →[R] P with the property that its composition with the canonical bilinear map M →[A] N →[R] M ⊗[R] N is the given bilinear map M →[A] N →[R] P.

Equations
source
@[simp]
theorem tensor_product.algebra_tensor_module.lift_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] (f : M →ₗ[A] N →ₗ[R] P) (ᾰ : tensor_product R M N) :
⇑(tensor_product.algebra_tensor_module.lift f) ᾰ = (tensor_product.lift (linear_map.restrict_scalars R f)).to_fun ᾰ
source
@[simp]
theorem tensor_product.algebra_tensor_module.lift_tmul {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] (f : M →ₗ[A] N →ₗ[R] P) (x : M) (y : N) :
⇑(tensor_product.algebra_tensor_module.lift f) (x ⊗ₜ[R] y) = ⇑(⇑f x) y
source
def tensor_product.algebra_tensor_module.uncurry (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] :
(M →ₗ[A] N →ₗ[R] P) →ₗ[A] tensor_product R M N →ₗ[A] P

Heterobasic version of tensor_product.uncurry:

Linearly constructing a linear map M ⊗[R] N →[A] P given a bilinear map M →[A] N →[R] P with the property that its composition with the canonical bilinear map M →[A] N →[R] M ⊗[R] N is the given bilinear map M →[A] N →[R] P.

Equations
source
@[simp]
theorem tensor_product.algebra_tensor_module.uncurry_apply (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] (f : M →ₗ[A] N →ₗ[R] P) :
⇑(tensor_product.algebra_tensor_module.uncurry R A M N P) f = tensor_product.algebra_tensor_module.lift f
source
@[simp]
theorem tensor_product.algebra_tensor_module.lcurry_apply (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] (f : tensor_product R M N →ₗ[A] P) :
⇑(tensor_product.algebra_tensor_module.lcurry R A M N P) f = tensor_product.algebra_tensor_module.curry f
source
def tensor_product.algebra_tensor_module.lcurry (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] :
(tensor_product R M N →ₗ[A] P) →ₗ[A] M →ₗ[A] N →ₗ[R] P

Heterobasic version of tensor_product.lcurry:

Given a linear map M ⊗[R] N →[A] P, compose it with the canonical bilinear map M →[A] N →[R] M ⊗[R] N to form a bilinear map M →[A] N →[R] P.

Equations
source
def tensor_product.algebra_tensor_module.lift.equiv (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] :
(M →ₗ[A] N →ₗ[R] P) ≃ₗ[A] tensor_product R M N →ₗ[A] P

Heterobasic version of tensor_product.lift.equiv:

A linear equivalence constructing a linear map M ⊗[R] N →[A] P given a bilinear map M →[A] N →[R] P with the property that its composition with the canonical bilinear map M →[A] N →[R] M ⊗[R] N is the given bilinear map M →[A] N →[R] P.

Equations
source
@[simp]
theorem tensor_product.algebra_tensor_module.mk_apply (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] (ᾰ : M) :
⇑(tensor_product.algebra_tensor_module.mk R A M N) ᾰ = (tensor_product.mk R M N).to_fun ᾰ
source
def tensor_product.algebra_tensor_module.mk (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] :
M →ₗ[A] N →ₗ[R] tensor_product R M N

Heterobasic version of tensor_product.mk:

The canonical bilinear map M →[A] N →[R] M ⊗[R] N.

Equations
source
def tensor_product.algebra_tensor_module.assoc (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M] [add_comm_monoid N] [module R N] [add_comm_monoid P] [module R P] [module A P] [is_scalar_tower R A P] :
tensor_product R (tensor_product A M P) N ≃ₗ[A] tensor_product A M (tensor_product R P N)

Heterobasic version of tensor_product.assoc:

Linear equivalence between (M ⊗[A] N) ⊗[R] P and M ⊗[A] (N ⊗[R] P).

Equations

The base-change of a linear map of R-modules to a linear map of A-modules #

source
def linear_map.base_change {R : Type u_1} (A : Type u_2) {M : Type u_4} {N : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (f : M →ₗ[R] N) :
tensor_product R A M →ₗ[A] tensor_product R A N

base_change A f for f : M →ₗ[R] N is the A-linear map A ⊗[R] M →ₗ[A] A ⊗[R] N.

Equations
source
@[simp]
theorem linear_map.base_change_tmul {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (f : M →ₗ[R] N) (a : A) (x : M) :
⇑(linear_map.base_change A f) (a ⊗ₜ[R] x) = a ⊗ₜ[R] ⇑f x
source
theorem linear_map.base_change_eq_ltensor {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (f : M →ₗ[R] N) :
⇑(linear_map.base_change A f) = ⇑(linear_map.ltensor A f)
source
@[simp]
theorem linear_map.base_change_add {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (f g : M →ₗ[R] N) :
linear_map.base_change A (f + g) = linear_map.base_change A f + linear_map.base_change A g
source
@[simp]
theorem linear_map.base_change_zero {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] :
linear_map.base_change A 0 = 0
source
@[simp]
theorem linear_map.base_change_smul {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (r : R) (f : M →ₗ[R] N) :
linear_map.base_change A (r • f) = r • linear_map.base_change A f
source
def linear_map.base_change_hom (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] :
(M →ₗ[R] N) →ₗ[R] tensor_product R A M →ₗ[A] tensor_product R A N

base_change as a linear map.

Equations
source
@[simp]
theorem linear_map.base_change_hom_apply (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N] (f : M →ₗ[R] N) :
⇑(linear_map.base_change_hom R A M N) f = linear_map.base_change A f
source
@[simp]
theorem linear_map.base_change_sub {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [comm_ring R] [ring A] [algebra R A] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (f g : M →ₗ[R] N) :
linear_map.base_change A (f - g) = linear_map.base_change A f - linear_map.base_change A g
source
@[simp]
theorem linear_map.base_change_neg {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [comm_ring R] [ring A] [algebra R A] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (f : M →ₗ[R] N) :
linear_map.base_change A (-f) = -linear_map.base_change A f

The R-algebra structure on A ⊗[R] B #

source
def algebra.tensor_product.mul_aux {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] (a₁ : A) (b₁ : B) :
tensor_product R A B →ₗ[R] tensor_product R A B

(Implementation detail) The multiplication map on A ⊗[R] B, for a fixed pure tensor in the first argument, as an R-linear map.

Equations
source
@[simp]
theorem algebra.tensor_product.mul_aux_apply {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] (a₁ a₂ : A) (b₁ b₂ : B) :
⇑(algebra.tensor_product.mul_aux a₁ b₁) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)
source
def algebra.tensor_product.mul {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] :
tensor_product R A B →ₗ[R] tensor_product R A B →ₗ[R] tensor_product R A B

(Implementation detail) The multiplication map on A ⊗[R] B, as an R-bilinear map.

Equations
source
@[simp]
theorem algebra.tensor_product.mul_apply {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] (a₁ a₂ : A) (b₁ b₂ : B) :
⇑(⇑algebra.tensor_product.mul (a₁ ⊗ₜ[R] b₁)) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)
source
theorem algebra.tensor_product.mul_assoc' {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] (mul : tensor_product R A B →ₗ[R] tensor_product R A B →ₗ[R] tensor_product R A B) (h : ∀ (a₁ a₂ a₃ : A) (b₁ b₂ b₃ : B), ⇑(⇑mul (⇑(⇑mul (a₁ ⊗ₜ[R] b₁)) (a₂ ⊗ₜ[R] b₂))) (a₃ ⊗ₜ[R] b₃) = ⇑(⇑mul (a₁ ⊗ₜ[R] b₁)) (⇑(⇑mul (a₂ ⊗ₜ[R] b₂)) (a₃ ⊗ₜ[R] b₃))) (x y z : tensor_product R A B) :
⇑(⇑mul (⇑(⇑mul x) y)) z = ⇑(⇑mul x) (⇑(⇑mul y) z)
source
@[protected]
theorem algebra.tensor_product.mul_assoc {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] (x y z : tensor_product R A B) :
⇑(⇑algebra.tensor_product.mul (⇑(⇑algebra.tensor_product.mul x) y)) z = ⇑(⇑algebra.tensor_product.mul x) (⇑(⇑algebra.tensor_product.mul y) z)
source
@[protected]
theorem algebra.tensor_product.one_mul {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] (x : tensor_product R A B) :
⇑(⇑algebra.tensor_product.mul (1 ⊗ₜ[R] 1)) x = x
source
@[protected]
theorem algebra.tensor_product.mul_one {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] (x : tensor_product R A B) :
⇑(⇑algebra.tensor_product.mul x) (1 ⊗ₜ[R] 1) = x
source
@[protected, instance]
def algebra.tensor_product.tensor_product.has_one {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] :
has_one (tensor_product R A B)
Equations
source
@[protected, instance]
def algebra.tensor_product.tensor_product.add_monoid_with_one {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] :
add_monoid_with_one (tensor_product R A B)
Equations
source
@[protected, instance]
def algebra.tensor_product.tensor_product.semiring {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] :
semiring (tensor_product R A B)
Equations
source
theorem algebra.tensor_product.one_def {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] :
1 = 1 ⊗ₜ[R] 1
source
@[simp]
theorem algebra.tensor_product.tmul_mul_tmul {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] (a₁ a₂ : A) (b₁ b₂ : B) :
a₁ ⊗ₜ[R] b₁ * a₂ ⊗ₜ[R] b₂ = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)
source
@[simp]
theorem algebra.tensor_product.tmul_pow {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] (a : A) (b : B) (k : ℕ) :
a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)
source
def algebra.tensor_product.include_left_ring_hom {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] :
A →+* tensor_product R A B

The ring morphism A →+* A ⊗[R] B sending a to a ⊗ₜ 1.

Equations
source
@[simp]
theorem algebra.tensor_product.include_left_ring_hom_apply {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] (a : A) :
⇑algebra.tensor_product.include_left_ring_hom a = a ⊗ₜ[R] 1
source
@[protected, instance]
def algebra.tensor_product.is_scalar_tower_right {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {S : Type u_1} [monoid S] [distrib_mul_action S A] [is_scalar_tower S A A] [smul_comm_class R S A] :
is_scalar_tower S (tensor_product R A B) (tensor_product R A B)
source
@[protected, instance]
def algebra.tensor_product.smul_comm_class_right {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {S : Type u_1} [monoid S] [distrib_mul_action S A] [smul_comm_class S A A] [smul_comm_class R S A] :
smul_comm_class S (tensor_product R A B) (tensor_product R A B)
source
@[protected, instance]
def algebra.tensor_product.left_algebra {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {S : Type u_1} [comm_semiring S] [algebra S A] [smul_comm_class R S A] :
algebra S (tensor_product R A B)
Equations
source
@[protected, instance]
def algebra.tensor_product.tensor_product.algebra {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] :
algebra R (tensor_product R A B)

The tensor product of two R-algebras is an R-algebra.

Equations
source
@[simp]
theorem algebra.tensor_product.algebra_map_apply {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {S : Type u_1} [comm_semiring S] [algebra S A] [smul_comm_class R S A] (r : S) :
⇑(algebra_map S (tensor_product R A B)) r = ⇑(algebra_map S A) r ⊗ₜ[R] 1
source
@[ext]
theorem algebra.tensor_product.ext {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] {g h : tensor_product R A B →ₐ[R] C} (H : ∀ (a : A) (b : B), ⇑g (a ⊗ₜ[R] b) = ⇑h (a ⊗ₜ[R] b)) :
g = h
source
def algebra.tensor_product.include_left {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] :
A →ₐ[R] tensor_product R A B

The R-algebra morphism A →ₐ[R] A ⊗[R] B sending a to a ⊗ₜ 1.

Equations
source
@[simp]
theorem algebra.tensor_product.include_left_apply {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] (a : A) :
⇑algebra.tensor_product.include_left a = a ⊗ₜ[R] 1
source
def algebra.tensor_product.include_right {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] :
B →ₐ[R] tensor_product R A B

The algebra morphism B →ₐ[R] A ⊗[R] B sending b to 1 ⊗ₜ b.

Equations
source
@[simp]
theorem algebra.tensor_product.include_right_apply {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] (b : B) :
⇑algebra.tensor_product.include_right b = 1 ⊗ₜ[R] b
source
theorem algebra.tensor_product.include_left_comp_algebra_map {R : Type u_1} {S : Type u_2} {T : Type u_3} [comm_ring R] [comm_ring S] [comm_ring T] [algebra R S] [algebra R T] :
algebra.tensor_product.include_left.to_ring_hom.comp (algebra_map R S) = algebra.tensor_product.include_right.to_ring_hom.comp (algebra_map R T)
source
@[protected, instance]
def algebra.tensor_product.tensor_product.ring {R : Type u} [comm_ring R] {A : Type v₁} [ring A] [algebra R A] {B : Type v₂} [ring B] [algebra R B] :
ring (tensor_product R A B)
Equations
source
@[protected, instance]
def algebra.tensor_product.tensor_product.comm_ring {R : Type u} [comm_ring R] {A : Type v₁} [comm_ring A] [algebra R A] {B : Type v₂} [comm_ring B] [algebra R B] :
comm_ring (tensor_product R A B)
Equations
source
@[reducible]
def algebra.tensor_product.right_algebra {R : Type u} [comm_ring R] {A : Type v₁} [comm_ring A] [algebra R A] {B : Type v₂} [comm_ring B] [algebra R B] :
algebra B (tensor_product R A B)

S ⊗[R] T has a T-algebra structure. This is not a global instance or else the action of S on S ⊗[R] S would be ambiguous.

Equations
source
@[protected, instance]
def algebra.tensor_product.right_is_scalar_tower {R : Type u} [comm_ring R] {A : Type v₁} [comm_ring A] [algebra R A] {B : Type v₂} [comm_ring B] [algebra R B] :
is_scalar_tower R B (tensor_product R A B)

We now build the structure maps for the symmetric monoidal category of R-algebras.

source
def algebra.tensor_product.alg_hom_of_linear_map_tensor_product {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] (f : tensor_product R A B →ₗ[R] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ⇑f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ⇑f (a₁ ⊗ₜ[R] b₁) * ⇑f (a₂ ⊗ₜ[R] b₂)) (w₂ : ∀ (r : R), ⇑f (⇑(algebra_map R A) r ⊗ₜ[R] 1) = ⇑(algebra_map R C) r) :
tensor_product R A B →ₐ[R] C

Build an algebra morphism from a linear map out of a tensor product, and evidence of multiplicativity on pure tensors.

Equations
source
@[simp]
theorem algebra.tensor_product.alg_hom_of_linear_map_tensor_product_apply {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] (f : tensor_product R A B →ₗ[R] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ⇑f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ⇑f (a₁ ⊗ₜ[R] b₁) * ⇑f (a₂ ⊗ₜ[R] b₂)) (w₂ : ∀ (r : R), ⇑f (⇑(algebra_map R A) r ⊗ₜ[R] 1) = ⇑(algebra_map R C) r) (x : tensor_product R A B) :
⇑(algebra.tensor_product.alg_hom_of_linear_map_tensor_product f w₁ w₂) x = ⇑f x
source
def algebra.tensor_product.alg_equiv_of_linear_equiv_tensor_product {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] (f : tensor_product R A B ≃ₗ[R] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ⇑f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ⇑f (a₁ ⊗ₜ[R] b₁) * ⇑f (a₂ ⊗ₜ[R] b₂)) (w₂ : ∀ (r : R), ⇑f (⇑(algebra_map R A) r ⊗ₜ[R] 1) = ⇑(algebra_map R C) r) :
tensor_product R A B ≃ₐ[R] C

Build an algebra equivalence from a linear equivalence out of a tensor product, and evidence of multiplicativity on pure tensors.

Equations
source
@[simp]
theorem algebra.tensor_product.alg_equiv_of_linear_equiv_tensor_product_apply {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] (f : tensor_product R A B ≃ₗ[R] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ⇑f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ⇑f (a₁ ⊗ₜ[R] b₁) * ⇑f (a₂ ⊗ₜ[R] b₂)) (w₂ : ∀ (r : R), ⇑f (⇑(algebra_map R A) r ⊗ₜ[R] 1) = ⇑(algebra_map R C) r) (x : tensor_product R A B) :
⇑(algebra.tensor_product.alg_equiv_of_linear_equiv_tensor_product f w₁ w₂) x = ⇑f x
source
def algebra.tensor_product.alg_equiv_of_linear_equiv_triple_tensor_product {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] {D : Type v₄} [semiring D] [algebra R D] (f : tensor_product R (tensor_product R A B) C ≃ₗ[R] D) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C), ⇑f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) = ⇑f (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) * ⇑f (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂)) (w₂ : ∀ (r : R), ⇑f (⇑(algebra_map R A) r ⊗ₜ[R] 1 ⊗ₜ[R] 1) = ⇑(algebra_map R D) r) :
tensor_product R (tensor_product R A B) C ≃ₐ[R] D

Build an algebra equivalence from a linear equivalence out of a triple tensor product, and evidence of multiplicativity on pure tensors.

Equations
source
@[simp]
theorem algebra.tensor_product.alg_equiv_of_linear_equiv_triple_tensor_product_apply {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] {D : Type v₄} [semiring D] [algebra R D] (f : tensor_product R (tensor_product R A B) C ≃ₗ[R] D) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C), ⇑f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) = ⇑f (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) * ⇑f (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂)) (w₂ : ∀ (r : R), ⇑f (⇑(algebra_map R A) r ⊗ₜ[R] 1 ⊗ₜ[R] 1) = ⇑(algebra_map R D) r) (x : tensor_product R (tensor_product R A B) C) :
⇑(algebra.tensor_product.alg_equiv_of_linear_equiv_triple_tensor_product f w₁ w₂) x = ⇑f x
source
@[protected]
def algebra.tensor_product.lid (R : Type u) [comm_semiring R] (A : Type v₁) [semiring A] [algebra R A] :
tensor_product R R A ≃ₐ[R] A

The base ring is a left identity for the tensor product of algebra, up to algebra isomorphism.

Equations
source
@[simp]
theorem algebra.tensor_product.lid_tmul (R : Type u) [comm_semiring R] (A : Type v₁) [semiring A] [algebra R A] (r : R) (a : A) :
⇑(algebra.tensor_product.lid R A) (r ⊗ₜ[R] a) = r • a
source
@[protected]
def algebra.tensor_product.rid (R : Type u) [comm_semiring R] (A : Type v₁) [semiring A] [algebra R A] :
tensor_product R A R ≃ₐ[R] A

The base ring is a right identity for the tensor product of algebra, up to algebra isomorphism.

Equations
source
@[simp]
theorem algebra.tensor_product.rid_tmul (R : Type u) [comm_semiring R] (A : Type v₁) [semiring A] [algebra R A] (r : R) (a : A) :
⇑(algebra.tensor_product.rid R A) (a ⊗ₜ[R] r) = r • a
source
@[protected]
def algebra.tensor_product.comm (R : Type u) [comm_semiring R] (A : Type v₁) [semiring A] [algebra R A] (B : Type v₂) [semiring B] [algebra R B] :
tensor_product R A B ≃ₐ[R] tensor_product R B A

The tensor product of R-algebras is commutative, up to algebra isomorphism.

Equations
source
@[simp]
theorem algebra.tensor_product.comm_tmul (R : Type u) [comm_semiring R] (A : Type v₁) [semiring A] [algebra R A] (B : Type v₂) [semiring B] [algebra R B] (a : A) (b : B) :
⇑(algebra.tensor_product.comm R A B) (a ⊗ₜ[R] b) = b ⊗ₜ[R] a
source
theorem algebra.tensor_product.adjoin_tmul_eq_top (R : Type u) [comm_semiring R] (A : Type v₁) [semiring A] [algebra R A] (B : Type v₂) [semiring B] [algebra R B] :
algebra.adjoin R {t : tensor_product R A B | ∃ (a : A) (b : B), a ⊗ₜ[R] b = t} = ⊤
source
theorem algebra.tensor_product.assoc_aux_1 {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C) :
⇑(tensor_product.assoc R A B C) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) = ⇑(tensor_product.assoc R A B C) (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) * ⇑(tensor_product.assoc R A B C) (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂)
source
theorem algebra.tensor_product.assoc_aux_2 {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] (r : R) :
⇑(tensor_product.assoc R A B C) (⇑(algebra_map R A) r ⊗ₜ[R] 1 ⊗ₜ[R] 1) = ⇑(algebra_map R (tensor_product R A (tensor_product R B C))) r
source
@[protected]
def algebra.tensor_product.assoc (R : Type u) [comm_semiring R] (A : Type v₁) [semiring A] [algebra R A] (B : Type v₂) [semiring B] [algebra R B] (C : Type v₃) [semiring C] [algebra R C] :
tensor_product R (tensor_product R A B) C ≃ₐ[R] tensor_product R A (tensor_product R B C)

The associator for tensor product of R-algebras, as an algebra isomorphism.

Equations
source
@[simp]
theorem algebra.tensor_product.assoc_tmul {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] (a : A) (b : B) (c : C) :
⇑(algebra.tensor_product.assoc R A B C) (a ⊗ₜ[R] b ⊗ₜ[R] c) = a ⊗ₜ[R] (b ⊗ₜ[R] c)
source
def algebra.tensor_product.map {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] {D : Type v₄} [semiring D] [algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) :
tensor_product R A C →ₐ[R] tensor_product R B D

The tensor product of a pair of algebra morphisms.

Equations
source
@[simp]
theorem algebra.tensor_product.map_tmul {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] {D : Type v₄} [semiring D] [algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) (a : A) (c : C) :
⇑(algebra.tensor_product.map f g) (a ⊗ₜ[R] c) = ⇑f a ⊗ₜ[R] ⇑g c
source
@[simp]
theorem algebra.tensor_product.map_comp_include_left {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] {D : Type v₄} [semiring D] [algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) :
(algebra.tensor_product.map f g).comp algebra.tensor_product.include_left = algebra.tensor_product.include_left.comp f
source
@[simp]
theorem algebra.tensor_product.map_comp_include_right {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] {D : Type v₄} [semiring D] [algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) :
(algebra.tensor_product.map f g).comp algebra.tensor_product.include_right = algebra.tensor_product.include_right.comp g
source
theorem algebra.tensor_product.map_range {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] {D : Type v₄} [semiring D] [algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) :
(algebra.tensor_product.map f g).range = (algebra.tensor_product.include_left.comp f).range ⊔ (algebra.tensor_product.include_right.comp g).range
source
def algebra.tensor_product.congr {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] {D : Type v₄} [semiring D] [algebra R D] (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) :
tensor_product R A C ≃ₐ[R] tensor_product R B D

Construct an isomorphism between tensor products of R-algebras from isomorphisms between the tensor factors.

Equations
source
@[simp]
theorem algebra.tensor_product.congr_apply {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] {D : Type v₄} [semiring D] [algebra R D] (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) (x : tensor_product R A C) :
⇑(algebra.tensor_product.congr f g) x = ⇑(algebra.tensor_product.map ↑f ↑g) x
source
@[simp]
theorem algebra.tensor_product.congr_symm_apply {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] {C : Type v₃} [semiring C] [algebra R C] {D : Type v₄} [semiring D] [algebra R D] (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) (x : tensor_product R B D) :
⇑((algebra.tensor_product.congr f g).symm) x = ⇑(algebra.tensor_product.map ↑(f.symm) ↑(g.symm)) x
source
def algebra.tensor_product.lmul' (R : Type u_1) {S : Type u_4} [comm_semiring R] [comm_semiring S] [algebra R S] :
tensor_product R S S →ₐ[R] S

linear_map.mul' is an alg_hom on commutative rings.

Equations
source
theorem algebra.tensor_product.lmul'_to_linear_map {R : Type u_1} {S : Type u_4} [comm_semiring R] [comm_semiring S] [algebra R S] :
(algebra.tensor_product.lmul' R).to_linear_map = linear_map.mul' R S
source
@[simp]
theorem algebra.tensor_product.lmul'_apply_tmul {R : Type u_1} {S : Type u_4} [comm_semiring R] [comm_semiring S] [algebra R S] (a b : S) :
⇑(algebra.tensor_product.lmul' R) (a ⊗ₜ[R] b) = a * b
source
@[simp]
theorem algebra.tensor_product.lmul'_comp_include_left {R : Type u_1} {S : Type u_4} [comm_semiring R] [comm_semiring S] [algebra R S] :
(algebra.tensor_product.lmul' R).comp algebra.tensor_product.include_left = alg_hom.id R S
source
@[simp]
theorem algebra.tensor_product.lmul'_comp_include_right {R : Type u_1} {S : Type u_4} [comm_semiring R] [comm_semiring S] [algebra R S] :
(algebra.tensor_product.lmul' R).comp algebra.tensor_product.include_right = alg_hom.id R S
source
def algebra.tensor_product.product_map {R : Type u_1} {A : Type u_2} {B : Type u_3} {S : Type u_4} [comm_semiring R] [semiring A] [semiring B] [comm_semiring S] [algebra R A] [algebra R B] [algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) :
tensor_product R A B →ₐ[R] S

If S is commutative, for a pair of morphisms f : A →ₐ[R] S, g : B →ₐ[R] S, We obtain a map A ⊗[R] B →ₐ[R] S that commutes with f, g via a ⊗ b ↦ f(a) * g(b).

Equations
source
@[simp]
theorem algebra.tensor_product.product_map_apply_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} {S : Type u_4} [comm_semiring R] [semiring A] [semiring B] [comm_semiring S] [algebra R A] [algebra R B] [algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) (a : A) (b : B) :
⇑(algebra.tensor_product.product_map f g) (a ⊗ₜ[R] b) = ⇑f a * ⇑g b
source
theorem algebra.tensor_product.product_map_left_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {S : Type u_4} [comm_semiring R] [semiring A] [semiring B] [comm_semiring S] [algebra R A] [algebra R B] [algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) (a : A) :
⇑(algebra.tensor_product.product_map f g) (⇑algebra.tensor_product.include_left a) = ⇑f a
source
@[simp]
theorem algebra.tensor_product.product_map_left {R : Type u_1} {A : Type u_2} {B : Type u_3} {S : Type u_4} [comm_semiring R] [semiring A] [semiring B] [comm_semiring S] [algebra R A] [algebra R B] [algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) :
(algebra.tensor_product.product_map f g).comp algebra.tensor_product.include_left = f
source
theorem algebra.tensor_product.product_map_right_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {S : Type u_4} [comm_semiring R] [semiring A] [semiring B] [comm_semiring S] [algebra R A] [algebra R B] [algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) (b : B) :
⇑(algebra.tensor_product.product_map f g) (⇑algebra.tensor_product.include_right b) = ⇑g b
source
@[simp]
theorem algebra.tensor_product.product_map_right {R : Type u_1} {A : Type u_2} {B : Type u_3} {S : Type u_4} [comm_semiring R] [semiring A] [semiring B] [comm_semiring S] [algebra R A] [algebra R B] [algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) :
(algebra.tensor_product.product_map f g).comp algebra.tensor_product.include_right = g
source
theorem algebra.tensor_product.product_map_range {R : Type u_1} {A : Type u_2} {B : Type u_3} {S : Type u_4} [comm_semiring R] [semiring A] [semiring B] [comm_semiring S] [algebra R A] [algebra R B] [algebra R S] (f : A →ₐ[R] S) (g : B →ₐ[R] S) :
(algebra.tensor_product.product_map f g).range = f.range ⊔ g.range
source
def algebra.tensor_product.product_left_alg_hom {R : Type u_1} {A : Type u_2} {A' : Type u_3} {B : Type u_4} {S : Type u_5} [comm_semiring R] [comm_semiring A] [semiring A'] [semiring B] [comm_semiring S] [algebra R A] [algebra R A'] [algebra A A'] [is_scalar_tower R A A'] [algebra R B] [algebra R S] [algebra A S] [is_scalar_tower R A S] (f : A' →ₐ[A] S) (g : B →ₐ[R] S) :
tensor_product R A' B →ₐ[A] S

If A, B are R-algebras, A' is an A-algebra, then the product map of f : A' →ₐ[A] S and g : B →ₐ[R] S is an A-algebra homomorphism.

Equations
source
@[simp]
theorem algebra.tensor_product.product_left_alg_hom_apply {R : Type u_1} {A : Type u_2} {A' : Type u_3} {B : Type u_4} {S : Type u_5} [comm_semiring R] [comm_semiring A] [semiring A'] [semiring B] [comm_semiring S] [algebra R A] [algebra R A'] [algebra A A'] [is_scalar_tower R A A'] [algebra R B] [algebra R S] [algebra A S] [is_scalar_tower R A S] (f : A' →ₐ[A] S) (g : B →ₐ[R] S) (ᾰ : tensor_product R A' B) :
⇑(algebra.tensor_product.product_left_alg_hom f g) ᾰ = (algebra.tensor_product.product_map (alg_hom.restrict_scalars R f) g).to_ring_hom.to_fun ᾰ
source
noncomputable def algebra.tensor_product.basis_aux {k : Type u_1} [comm_ring k] (R : Type u_2) [ring R] [algebra k R] {M : Type u_3} [add_comm_monoid M] [module k M] {ι : Type u_4} (b : basis ι k M) :
tensor_product k R M ≃ₗ[k] ι →₀ R

Given a k-algebra R and a k-basis of M, this is a k-linear isomorphism R ⊗[k] M ≃ (ι →₀ R) (which is in fact R-linear).

Equations
source
theorem algebra.tensor_product.basis_aux_tmul {k : Type u_1} [comm_ring k] {R : Type u_2} [ring R] [algebra k R] {M : Type u_3} [add_comm_monoid M] [module k M] {ι : Type u_4} (b : basis ι k M) (r : R) (m : M) :
⇑(algebra.tensor_product.basis_aux R b) (r ⊗ₜ[k] m) = r • finsupp.map_range ⇑(algebra_map k R) _ (⇑(b.repr) m)
source
theorem algebra.tensor_product.basis_aux_map_smul {k : Type u_1} [comm_ring k] {R : Type u_2} [ring R] [algebra k R] {M : Type u_3} [add_comm_monoid M] [module k M] {ι : Type u_4} (b : basis ι k M) (r : R) (x : tensor_product k R M) :
⇑(algebra.tensor_product.basis_aux R b) (r • x) = r • ⇑(algebra.tensor_product.basis_aux R b) x
source
noncomputable def algebra.tensor_product.basis {k : Type u_1} [comm_ring k] (R : Type u_2) [ring R] [algebra k R] {M : Type u_3} [add_comm_monoid M] [module k M] {ι : Type u_4} (b : basis ι k M) :
basis ι R (tensor_product k R M)

Given a k-algebra R, this is the R-basis of R ⊗[k] M induced by a k-basis of M.

Equations
source
@[simp]
theorem algebra.tensor_product.basis_repr_tmul {k : Type u_1} [comm_ring k] {R : Type u_2} [ring R] [algebra k R] {M : Type u_3} [add_comm_monoid M] [module k M] {ι : Type u_4} (b : basis ι k M) (r : R) (m : M) :
⇑((algebra.tensor_product.basis R b).repr) (r ⊗ₜ[k] m) = r • finsupp.map_range ⇑(algebra_map k R) _ (⇑(b.repr) m)
source
@[simp]
theorem algebra.tensor_product.basis_repr_symm_apply {k : Type u_1} [comm_ring k] {R : Type u_2} [ring R] [algebra k R] {M : Type u_3} [add_comm_monoid M] [module k M] {ι : Type u_4} (b : basis ι k M) (r : R) (i : ι) :
⇑((algebra.tensor_product.basis R b).repr.symm) (finsupp.single i r) = r ⊗ₜ[k] ⇑(b.repr.symm) (finsupp.single i 1)
source
def module.End_tensor_End_alg_hom {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
tensor_product R (module.End R M) (module.End R N) →ₐ[R] module.End R (tensor_product R M N)

The algebra homomorphism from End M ⊗ End N to End (M ⊗ N) sending f ⊗ₜ g to the tensor_product.map f g, the tensor product of the two maps.

Equations
source
theorem module.End_tensor_End_alg_hom_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] (f : module.End R M) (g : module.End R N) :
⇑module.End_tensor_End_alg_hom (f ⊗ₜ[R] g) = tensor_product.map f g
source
theorem subalgebra.finite_dimensional_sup {K : Type u_1} {L : Type u_2} [field K] [comm_ring L] [algebra K L] (E1 E2 : subalgebra K L) [finite_dimensional K ↥E1] [finite_dimensional K ↥E2] :
finite_dimensional K ↥(E1 ⊔ E2)
source
def tensor_product.algebra.module_aux {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] :
tensor_product R A B →ₗ[R] M →ₗ[R] M

An auxiliary definition, used for constructing the module (A ⊗[R] B) M in tensor_product.algebra.module below.

Equations
source
theorem tensor_product.algebra.module_aux_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] (a : A) (b : B) (m : M) :
⇑(⇑tensor_product.algebra.module_aux (a ⊗ₜ[R] b)) m = a • b • m
source
@[protected]
def tensor_product.algebra.module {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] [smul_comm_class A B M] :
module (tensor_product R A B) M

If M is a representation of two different R-algebras A and B whose actions commute, then it is a representation the R-algebra A ⊗[R] B.

An important example arises from a semiring S; allowing S to act on itself via left and right multiplication, the roles of R, A, B, M are played by ℕ, S, Sᵐᵒᵖ, S. This example is important because a submodule of S as a module over S ⊗[ℕ] Sᵐᵒᵖ is a two-sided ideal.

NB: This is not an instance because in the case B = A and M = A ⊗[R] A we would have a diamond of smul actions. Furthermore, this would not be a mere definitional diamond but a true mathematical diamond in which A ⊗[R] A had two distinct scalar actions on itself: one from its multiplication, and one from this would-be instance. Arguably we could live with this but in any case the real fix is to address the ambiguity in notation, probably along the lines outlined here: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234773.20base.20change/near/240929258

Equations
source
theorem tensor_product.algebra.smul_def {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] [semiring A] [semiring B] [module A M] [module B M] [algebra R A] [algebra R B] [is_scalar_tower R A M] [is_scalar_tower R B M] [smul_comm_class A B M] (a : A) (b : B) (m : M) :
a ⊗ₜ[R] b • m = a • b • m