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 #

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 : 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 : 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 : M ⊗ N →ₗ[A] P) (ᾰ : M) :
⇑(tensor_product.algebra_tensor_module.curry f) ᾰ = (tensor_product.curry (linear_map.restrict_scalars R f)).to_fun ᾰ
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 : 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 : 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) :
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) (ᾰ : 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] 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 : 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] :
(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] 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] 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] :
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 #

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) :
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
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] A ⊗ M →ₗ[A] 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) :
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
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] :
A ⊗ B →ₗ[R] A ⊗ B →ₗ[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 : 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)
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] (x y z : 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
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) :
⇑(⇑algebra.tensor_product.mul (1 ⊗ₜ[R] 1)) x = x
source
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) :
⇑(⇑algebra.tensor_product.mul x) (1 ⊗ₜ[R] 1) = x
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 (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.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
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 (A ⊗ B)
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] (r : R) :
⇑(algebra_map R (A ⊗ B)) r = ⇑(algebra_map R 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 : 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] A ⊗ B

The 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] 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
@[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 (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 (A ⊗ B)
Equations

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 : 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
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 : 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) :
⇑(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 : 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
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 : 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) :
⇑(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 : 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
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 : 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) :
⇑(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] :
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] :
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] :
A ⊗ B ≃ₐ[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 : 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 (A ⊗ (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] :
A ⊗ B ⊗ C ≃ₐ[R] A ⊗ (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) :
A ⊗ C →ₐ[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) :
A ⊗ C ≃ₐ[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 : 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 : 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] :
S ⊗ S →ₐ[R] S

algebra.lmul' 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 = algebra.lmul' R
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) :
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
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)