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
R ⊗[R] A ≃ₐ[R] AA ⊗[R] R ≃ₐ[R] AA ⊗[R] B ≃ₐ[R] B ⊗[R] A
The code for
((A ⊗[R] B) ⊗[R] C) ≃ₐ[R] (A ⊗[R] (B ⊗[R] C))is written and compiles, but takes longer than the-T100000time limit, so is currently commented out.
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 → (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.
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
- algebra.tensor_product.mul = tensor_product.lift {to_fun := λ (a₁ : A), {to_fun := λ (b₁ : B), algebra.tensor_product.mul_aux a₁ b₁, map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _}
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) :
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) :
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) :
@[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] :
semiring (tensor_product R A B)
Equations
- algebra.tensor_product.semiring = {add := has_add.add (add_semigroup.to_has_add (tensor_product R A B)), add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _, mul := λ (a b : tensor_product R A B), ⇑(⇑algebra.tensor_product.mul a) b, mul_assoc := _, one := 1 ⊗ₜ[R] 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
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] :
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 →+* tensor_product R A B
The algebra map R →+* (A ⊗[R] B) giving A ⊗[R] B the structure of an R-algebra.
@[instance]
def
algebra.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)
Equations
- algebra.tensor_product.algebra = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := {to_fun := algebra.tensor_product.tensor_algebra_map.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
@[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 (tensor_product R A B)) r = ⇑(algebra_map R A) r ⊗ₜ[R] 1
@[ext]
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 algebra morphism A →ₐ[R] A ⊗[R] B sending a to a ⊗ₜ 1.
@[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] tensor_product R A B
The algebra morphism B →ₐ[R] A ⊗[R] B sending b to 1 ⊗ₜ b.
@[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) :
@[instance]
def
algebra.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
- algebra.tensor_product.ring = {add := add_comm_group.add tensor_product.add_comm_group, add_assoc := _, zero := add_comm_group.zero tensor_product.add_comm_group, zero_add := _, add_zero := _, neg := add_comm_group.neg tensor_product.add_comm_group, add_left_neg := _, add_comm := _, mul := semiring.mul algebra.tensor_product.semiring, mul_assoc := _, one := semiring.one algebra.tensor_product.semiring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
@[instance]
def
algebra.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
- algebra.tensor_product.comm_ring = {add := ring.add algebra.tensor_product.ring, add_assoc := _, zero := ring.zero algebra.tensor_product.ring, zero_add := _, add_zero := _, neg := ring.neg algebra.tensor_product.ring, add_left_neg := _, add_comm := _, mul := ring.mul algebra.tensor_product.ring, mul_assoc := _, one := ring.one algebra.tensor_product.ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
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) :
Build an algebra morphism from a linear map out of a tensor product, and evidence of multiplicativity on pure tensors.
@[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
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) :
Build an algebra equivalence from a linear equivalence out of a tensor product, and evidence of multiplicativity on pure tensors.
@[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
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) :
Build an algebra equivalence from a linear equivalence out of a triple tensor product, and evidence of multiplicativity on pure tensors.
@[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) :
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
@[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] :
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
@[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] :
tensor_product R A B ≃ₐ[R] tensor_product 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) :
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
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) → (tensor_product R A C →ₐ[R] tensor_product R B D)
The tensor product of a pair of algebra morphisms.
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) → (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
- algebra.tensor_product.congr f g = alg_equiv.of_alg_hom (algebra.tensor_product.map ↑f ↑g) (algebra.tensor_product.map ↑(f.symm) ↑(g.symm)) _ _
@[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
@[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