mathlib documentation

ring_theory.tensor_product

The tensor product of R-algebras #

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 #

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 : M N) :
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 : M N →ₗ[A] 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
@[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 : M N →ₗ[A] P) (ᾰ : M) :
@[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] :

Just as tensor_product.mk_compr₂_inj 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].

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 : M N →ₗ[A] P} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)) :
g = h
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) :
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
@[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) (ᾰ : M N) :
@[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) :
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] :

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
@[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) :
@[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 : M N →ₗ[A] P) :
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] :

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
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] :

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
@[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) :
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] :

Heterobasic version of tensor_product.mk:

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

Equations
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] :
M P N ≃ₗ[A] M (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 #

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) :
A M →ₗ[A] A N

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

Equations
@[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) :
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) :
@[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) :
@[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] :
@[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) :
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] A M →ₗ[A] A N

base_change as a linear map.

Equations
@[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) :
@[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) :
@[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) :

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

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) :
A B →ₗ[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
@[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₂
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] :
A B →ₗ[R] A B →ₗ[R] A B

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

Equations
@[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₂
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 : A B →ₗ[R] A B →ₗ[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 : A B) :
(mul ((mul x) y)) z = (mul x) ((mul y) z)
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 : A B) :
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 : A B) :
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
@[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₂
@[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)
def algebra.tensor_product.tensor_algebra_map {R : Type u} [comm_semiring R] {A : Type v₁} [semiring A] [algebra R A] {B : Type v₂} [semiring B] [algebra R B] :
R →+* A B

The algebra map R →+* (A ⊗[R] B) giving A ⊗[R] B the structure of an R-algebra.

Equations
@[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] (r : R) :
(algebra_map R (A B)) r = (algebra_map R A) r ⊗ₜ[R] 1
@[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 : A B →ₐ[R] C} (H : ∀ (a : A) (b : B), g (a ⊗ₜ[R] b) = h (a ⊗ₜ[R] b)) :
g = h
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] A B

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

Equations
@[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) :
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] A B

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

Equations
@[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) :

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

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 : 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) :
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
@[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 : 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 : A B) :
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 : 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) :
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
@[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 : 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 : A B) :
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 : 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) :
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
@[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 : 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 : A B C) :
def algebra.tensor_product.lid (R : Type u) [comm_semiring R] (A : Type v₁) [semiring A] [algebra R A] :
R A ≃ₐ[R] A

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

Equations
@[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) :
def algebra.tensor_product.rid (R : Type u) [comm_semiring R] (A : Type v₁) [semiring A] [algebra R A] :
A R ≃ₐ[R] A

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

Equations
@[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) :
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] :
A B ≃ₐ[R] B A

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

Equations
@[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) :
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₂)
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) :
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) :
A C →ₐ[R] B D

The tensor product of a pair of algebra morphisms.

Equations
@[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) :
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) :
A C ≃ₐ[R] B D

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

Equations
@[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 : A C) :
@[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 : B D) :