mathlib documentation

ring_theory.tensor_product

The tensor product of R-algebras.

We construct the R-algebra structure on A ⊗[R] B, when A and B are both R-algebras, and provide the structure isomorphisms

The code for

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

@[instance]
def algebra.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] :

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.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} :
(∀ (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) :
(∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] b₁ * b₂) = (f (a₁ ⊗ₜ[R] b₁)) * f (a₂ ⊗ₜ[R] b₂))(∀ (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) :
(∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] b₁ * b₂) = (f (a₁ ⊗ₜ[R] b₁)) * f (a₂ ⊗ₜ[R] b₂))(∀ (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) :
(∀ (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₂))(∀ (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) :
(tensor_product.assoc R A B C) (((algebra_map R A) r ⊗ₜ[R] 1) ⊗ₜ[R] 1) = (algebra_map R (A (B C))) 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] :
(A →ₐ[R] B)(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] :
(A ≃ₐ[R] B)(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) :