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₁ : 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.
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
- 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 : 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) :
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) :
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
- algebra.tensor_product.semiring = {add := has_add.add (add_semigroup.to_has_add (A ⊗ B)), add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _, mul := λ (a b : 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] :
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] :
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 (A ⊗ B)) r = ⇑(algebra_map R A) r ⊗ₜ[R] 1
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 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] :
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] :
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] :
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 : 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.
@[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
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) :
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 : 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
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) :
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 : 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] :
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] :
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] :
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 (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]
(f : A →ₐ[R] B)
(g : C →ₐ[R] 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]
(f : A ≃ₐ[R] B)
(g : C ≃ₐ[R] 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 : 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 : B ⊗ D) :
⇑((algebra.tensor_product.congr f g).symm) x = ⇑(algebra.tensor_product.map ↑(f.symm) ↑(g.symm)) x