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 #

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

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
@[ext]

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

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

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_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
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

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

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

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

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

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

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

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

The tensor product of two R-algebras is 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] {S : Type u_1} [comm_semiring S] [algebra S A] [smul_comm_class R S A] (r : S) :
@[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
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] :

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

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

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

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

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

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

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

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

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

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

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

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

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

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 : tensor_product R 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 : tensor_product R B D) :

linear_map.mul' is an alg_hom on commutative rings.

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

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

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

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

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

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

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

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