Extras for ring_theory.tensor_product #
This file in mathlib starts with some heterobasic results, but quickly drops back to forcing various rings or algebra to be equal. This isn't enough for us when trying to base change a quadratic form.
https://github.com/leanprover-community/mathlib4/pull/6035 adds some of these results to mathlib4.
The A-module structure on A ⊗[R] M #
def
tensor_product.algebra_tensor_module.map
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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]
[add_comm_monoid Q]
[module R Q]
(f : M →ₗ[A] P)
(g : N →ₗ[R] Q) :
tensor_product R M N →ₗ[A] tensor_product R P Q
Heterobasic tensor_product.map.
Equations
- tensor_product.algebra_tensor_module.map f g = tensor_product.algebra_tensor_module.lift ((show (Q →ₗ[R] tensor_product R P Q) →ₗ[A] N →ₗ[R] tensor_product R P Q, from {to_fun := λ (h : Q →ₗ[R] tensor_product R P Q), h.comp g, map_add' := _, map_smul' := _}).comp ((tensor_product.algebra_tensor_module.mk R A P Q).comp f))
theorem
tensor_product.algebra_tensor_module.map_apply
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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]
[add_comm_monoid Q]
[module R Q]
(f : M →ₗ[A] P)
(g : N →ₗ[R] Q)
(x : tensor_product R M N) :
⇑(tensor_product.algebra_tensor_module.map f g) x = ⇑(tensor_product.map (linear_map.restrict_scalars R f) g) x
@[simp]
theorem
tensor_product.algebra_tensor_module.map_tmul
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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]
[add_comm_monoid Q]
[module R Q]
(f : M →ₗ[A] P)
(g : N →ₗ[R] Q)
(m : M)
(n : N) :
@[simp]
theorem
tensor_product.algebra_tensor_module.map_id
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
[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] :
theorem
tensor_product.algebra_tensor_module.map_id_apply
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
[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]
(x : tensor_product R M N) :
theorem
tensor_product.algebra_tensor_module.map_comp
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
{P' : Type u_9}
{Q' : Type u_10}
[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]
[add_comm_monoid Q]
[module R Q]
[add_comm_monoid P']
[module R P']
[module A P']
[is_scalar_tower R A P']
[add_comm_monoid Q']
[module R Q']
(f : P →ₗ[A] P')
(f' : M →ₗ[A] P)
(g : Q →ₗ[R] Q')
(g' : N →ₗ[R] Q) :
tensor_product.algebra_tensor_module.map (f.comp f') (g.comp g') = (tensor_product.algebra_tensor_module.map f g).comp (tensor_product.algebra_tensor_module.map f' g')
theorem
tensor_product.algebra_tensor_module.map_map
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
{P' : Type u_9}
{Q' : Type u_10}
[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]
[add_comm_monoid Q]
[module R Q]
[add_comm_monoid P']
[module R P']
[module A P']
[is_scalar_tower R A P']
[add_comm_monoid Q']
[module R Q']
(f : P →ₗ[A] P')
(f' : M →ₗ[A] P)
(g : Q →ₗ[R] Q')
(g' : N →ₗ[R] Q)
(x : tensor_product R M N) :
⇑(tensor_product.algebra_tensor_module.map f g) (⇑(tensor_product.algebra_tensor_module.map f' g') x) = ⇑(tensor_product.algebra_tensor_module.map (f.comp f') (g.comp g')) x
theorem
tensor_product.algebra_tensor_module.map_add_left
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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]
[add_comm_monoid Q]
[module R Q]
(f₁ f₂ : M →ₗ[A] P)
(g : N →ₗ[R] Q) :
theorem
tensor_product.algebra_tensor_module.map_add_right
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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]
[add_comm_monoid Q]
[module R Q]
(f : M →ₗ[A] P)
(g₁ g₂ : N →ₗ[R] Q) :
theorem
tensor_product.algebra_tensor_module.map_smul_left
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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]
[add_comm_monoid Q]
[module R Q]
(r : A)
(f : M →ₗ[A] P)
(g : N →ₗ[R] Q) :
theorem
tensor_product.algebra_tensor_module.map_smul_right
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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]
[add_comm_monoid Q]
[module R Q]
(r : R)
(f : M →ₗ[A] P)
(g : N →ₗ[R] Q) :
def
tensor_product.algebra_tensor_module.map_bilinear
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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]
[add_comm_monoid Q]
[module R Q] :
Heterobasic map_bilinear
def
tensor_product.algebra_tensor_module.congr
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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]
[add_comm_monoid Q]
[module R Q]
(f : M ≃ₗ[A] P)
(g : N ≃ₗ[R] Q) :
tensor_product R M N ≃ₗ[A] tensor_product R P Q
Heterobasic tensor_product.congr.
Equations
@[simp]
theorem
tensor_product.algebra_tensor_module.congr_tmul
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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]
[add_comm_monoid Q]
[module R Q]
(f : M ≃ₗ[A] P)
(g : N ≃ₗ[R] Q)
(m : M)
(n : N) :
@[simp]
theorem
tensor_product.algebra_tensor_module.congr_symm_tmul
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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]
[add_comm_monoid Q]
[module R Q]
(f : M ≃ₗ[A] P)
(g : N ≃ₗ[R] Q)
(p : P)
(q : Q) :
def
tensor_product.algebra_tensor_module.rid
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[comm_semiring A]
[algebra R A] :
tensor_product R A R ≃ₗ[A] A
Equations
theorem
tensor_product.algebra_tensor_module.rid_apply
(R : Type u_1)
(A : Type u_2)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(a : A)
(r : R) :
⇑(tensor_product.algebra_tensor_module.rid R A) (a ⊗ₜ[R] r) = a * ⇑(algebra_map R A) r
def
tensor_product.algebra_tensor_module.left_comm
(R : Type u_1)
(A : Type u_2)
(M : Type u_5)
(P : Type u_7)
(Q : Type u_8)
[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 P]
[module R P]
[module A P]
[is_scalar_tower R A P]
[add_comm_monoid Q]
[module R Q] :
tensor_product A M (tensor_product R P Q) ≃ₗ[A] tensor_product A P (tensor_product R M Q)
Heterobasic tensor_product.left_comm.
Equations
- tensor_product.algebra_tensor_module.left_comm R A M P Q = let e₁ : tensor_product A M (tensor_product R P Q) ≃ₗ[A] tensor_product R (tensor_product A M P) Q := (tensor_product.algebra_tensor_module.assoc R A M Q P).symm, e₂ : tensor_product R (tensor_product A M P) Q ≃ₗ[A] tensor_product R (tensor_product A P M) Q := tensor_product.algebra_tensor_module.congr (tensor_product.comm A M P) 1, e₃ : tensor_product R (tensor_product A P M) Q ≃ₗ[A] tensor_product A P (tensor_product R M Q) := tensor_product.algebra_tensor_module.assoc R A P Q M in e₁.trans (e₂.trans e₃)
def
tensor_product.algebra_tensor_module.hom_tensor_hom_map
(R : Type u_1)
(A : Type u_2)
(M : Type u_5)
(N : Type u_6)
(P : Type u_7)
(Q : Type u_8)
[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]
[add_comm_monoid Q]
[module R Q] :
tensor_product R (M →ₗ[A] P) (N →ₗ[R] Q) →ₗ[A] tensor_product R M N →ₗ[A] tensor_product R P Q
@[simp]
theorem
tensor_product.algebra_tensor_module.hom_tensor_hom_map_apply
(R : Type u_1)
(A : Type u_2)
(M : Type u_5)
(N : Type u_6)
(P : Type u_7)
(Q : Type u_8)
[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]
[add_comm_monoid Q]
[module R Q]
(f : M →ₗ[A] P)
(g : N →ₗ[R] Q) :
⇑(tensor_product.algebra_tensor_module.hom_tensor_hom_map R A M N P Q) (f ⊗ₜ[R] g) = tensor_product.algebra_tensor_module.map f g
def
tensor_product.algebra_tensor_module.dual_distrib
(R : Type u_1)
(A : Type u_2)
(M : Type u_5)
(N : Type u_6)
[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] :
tensor_product R (module.dual A M) (module.dual R N) →ₗ[A] module.dual A (tensor_product R M N)
Equations
@[simp]
theorem
tensor_product.algebra_tensor_module.dual_distrib_apply
{R : Type u_1}
{A : Type u_2}
{M : Type u_5}
{N : Type u_6}
[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]
(f : module.dual A M)
(g : module.dual R N)
(m : M)
(n : N) :
@[simp]
theorem
tensor_product.algebra_tensor_module.uncurry'_apply
(R : Type u_1)
(A : Type u_2)
(N : Type u_6)
(P : Type u_7)
(Q : Type u_8)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
[add_comm_monoid N]
[module R N]
[add_comm_monoid P]
[module R P]
[module A P]
[is_scalar_tower R A P]
[add_comm_monoid Q]
[module R Q]
(f : N →ₗ[R] Q →ₗ[R] P) :
def
tensor_product.algebra_tensor_module.uncurry'
(R : Type u_1)
(A : Type u_2)
(N : Type u_6)
(P : Type u_7)
(Q : Type u_8)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
[add_comm_monoid N]
[module R N]
[add_comm_monoid P]
[module R P]
[module A P]
[is_scalar_tower R A P]
[add_comm_monoid Q]
[module R Q] :
A variant of algebra_tensor_module.uncurry, where only the outermost map is
A-linear.
Equations
- tensor_product.algebra_tensor_module.uncurry' R A N P Q = {to_fun := tensor_product.algebra_tensor_module.lift _, map_add' := _, map_smul' := _}
def
tensor_product.algebra_tensor_module.lcurry'
(R : Type u_1)
(A : Type u_2)
(N : Type u_6)
(P : Type u_7)
(Q : Type u_8)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
[add_comm_monoid N]
[module R N]
[add_comm_monoid P]
[module R P]
[module A P]
[is_scalar_tower R A P]
[add_comm_monoid Q]
[module R Q] :
A variant of algebra_tensor_module.lcurry, where only the outermost map is
A-linear.
Equations
- tensor_product.algebra_tensor_module.lcurry' R A N P Q = {to_fun := tensor_product.algebra_tensor_module.curry _, map_add' := _, map_smul' := _}
@[simp]
theorem
tensor_product.algebra_tensor_module.lcurry'_apply
(R : Type u_1)
(A : Type u_2)
(N : Type u_6)
(P : Type u_7)
(Q : Type u_8)
[comm_semiring R]
[comm_semiring A]
[algebra R A]
[add_comm_monoid N]
[module R N]
[add_comm_monoid P]
[module R P]
[module A P]
[is_scalar_tower R A P]
[add_comm_monoid Q]
[module R Q]
(f : tensor_product R N Q →ₗ[R] P) :
def
tensor_product.algebra_tensor_module.assoc'
(R : Type u_1)
(A : Type u_2)
(M : Type u_5)
(N : Type u_6)
(Q : Type u_8)
[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 Q]
[module R Q] :
tensor_product R (tensor_product R M N) Q ≃ₗ[A] tensor_product R M (tensor_product R N Q)
A variant of algebra_tensor_module.assoc, where only the outermost map is
A-linear.
Equations
- tensor_product.algebra_tensor_module.assoc' R A M N Q = linear_equiv.of_linear (tensor_product.algebra_tensor_module.lift (tensor_product.algebra_tensor_module.lift ((tensor_product.algebra_tensor_module.lcurry' R A N (tensor_product R M (tensor_product R N Q)) Q).comp (tensor_product.algebra_tensor_module.mk R A M (tensor_product R N Q))))) (tensor_product.algebra_tensor_module.lift ((tensor_product.algebra_tensor_module.uncurry' R A N (tensor_product R (tensor_product R M N) Q) Q).comp (tensor_product.algebra_tensor_module.curry (tensor_product.algebra_tensor_module.mk R A (tensor_product R M N) Q)))) _ _
def
tensor_product.algebra_tensor_module.right_comm
(R : Type u_1)
(A : Type u_2)
(M : Type u_5)
(P : Type u_7)
(Q : Type u_8)
[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 P]
[module R P]
[module A P]
[is_scalar_tower R A P]
[add_comm_monoid Q]
[module R Q] :
tensor_product R (tensor_product A M P) Q ≃ₗ[A] tensor_product A (tensor_product R M Q) P
A tensor product analogue of mul_right_comm.
Equations
- tensor_product.algebra_tensor_module.right_comm R A M P Q = linear_equiv.of_linear (tensor_product.algebra_tensor_module.lift (tensor_product.lift ((tensor_product.algebra_tensor_module.lcurry R A M Q (tensor_product A (tensor_product R M Q) P)).comp (tensor_product.algebra_tensor_module.mk A A (tensor_product R M Q) P).flip).flip)) (tensor_product.lift (tensor_product.algebra_tensor_module.lift ((linear_map.restrict_scalars R (tensor_product.lcurry A M P (tensor_product R (tensor_product A M P) Q))).comp (tensor_product.algebra_tensor_module.mk R A (tensor_product A M P) Q).flip).flip)) _ _
def
tensor_product.algebra_tensor_module.tensor_tensor_tensor_comm
(R : Type u_1)
(A : Type u_2)
(M : Type u_5)
(N : Type u_6)
(P : Type u_7)
(Q : Type u_8)
[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]
[add_comm_monoid Q]
[module R Q] :
tensor_product A (tensor_product R M N) (tensor_product R P Q) ≃ₗ[A] tensor_product R (tensor_product A M P) (tensor_product R N Q)
Heterobasic version of tensor_tensor_tensor_comm.
Equations
- tensor_product.algebra_tensor_module.tensor_tensor_tensor_comm R A M N P Q = ((tensor_product.algebra_tensor_module.assoc R A (tensor_product R M N) Q P).symm.trans (tensor_product.algebra_tensor_module.congr (tensor_product.algebra_tensor_module.right_comm R A M P N).symm 1)).trans (tensor_product.algebra_tensor_module.assoc' R A (tensor_product A M P) N Q)
@[simp]
theorem
tensor_product.algebra_tensor_module.tensor_tensor_tensor_comm_apply
(R : Type u_1)
(A : Type u_2)
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
{Q : Type u_8}
[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]
[add_comm_monoid Q]
[module R Q]
(m : M)
(n : N)
(p : P)
(q : Q) :
theorem
algebra.tensor_product.algebra_map_tmul_one
{R : Type u_1}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(r : R) :
⇑(algebra_map R A) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] ⇑(algebra_map R B) r
def
algebra.tensor_product.alg_hom_of_linear_map_tensor_product'
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{B : Type u_4}
{C : Type u_5}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[semiring C]
[algebra R A]
[algebra R B]
[algebra R C]
[algebra S A]
[algebra S C]
[algebra R S]
[smul_comm_class R S A]
[is_scalar_tower R S A]
[is_scalar_tower R S C]
(f : tensor_product R A B →ₗ[S] C)
(w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ⇑f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ⇑f (a₁ ⊗ₜ[R] b₁) * ⇑f (a₂ ⊗ₜ[R] b₂))
(w₂ : ∀ (r : S), ⇑f (⇑(algebra_map S A) r ⊗ₜ[R] 1) = ⇑(algebra_map S C) r) :
tensor_product R A B →ₐ[S] C
a stronger version of alg_hom_of_linear_map_tensor_product
@[simp]
theorem
algebra.tensor_product.alg_hom_of_linear_map_tensor_product'_apply
{R : Type u_1}
{A : Type u_3}
{B : Type u_4}
{C : Type u_5}
[comm_semiring R]
[semiring A]
[semiring B]
[semiring C]
[algebra R A]
[algebra R B]
[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.map'
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{B : Type u_4}
{C : Type u_5}
{D : Type u_6}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[semiring C]
[semiring D]
[algebra R A]
[algebra R B]
[algebra R C]
[algebra R D]
[algebra S A]
[algebra S C]
[algebra R S]
[smul_comm_class R S A]
[is_scalar_tower R S A]
[is_scalar_tower R S C]
(f : A →ₐ[S] C)
(g : B →ₐ[R] D) :
tensor_product R A B →ₐ[S] tensor_product R C D
a stronger version of map
@[simp]
theorem
algebra.tensor_product.map'_tmul
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{B : Type u_4}
{C : Type u_5}
{D : Type u_6}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[semiring C]
[semiring D]
[algebra R A]
[algebra R B]
[algebra R C]
[algebra R D]
[algebra S A]
[algebra S C]
[algebra R S]
[smul_comm_class R S A]
[is_scalar_tower R S A]
[is_scalar_tower R S C]
(f : A →ₐ[S] C)
(g : B →ₐ[R] D)
(a : A)
(b : B) :
def
algebra.tensor_product.include_left'
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
[algebra S A]
[algebra R S]
[smul_comm_class R S A]
[is_scalar_tower R S A] :
A →ₐ[S] tensor_product R A B
a stronger version of include_left
@[simp]
theorem
algebra.tensor_product.include_left'_apply
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{B : Type u_4}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
[algebra S A]
[algebra R S]
[smul_comm_class R S A]
[is_scalar_tower R S A]
(ᾰ : A) :
@[ext]
def
algebra.tensor_product.ext'
{R : Type u_1}
{S : Type u_2}
{A : Type u_3}
{B : Type u_4}
{C : Type u_5}
[comm_semiring R]
[comm_semiring S]
[semiring A]
[semiring B]
[semiring C]
[algebra R A]
[algebra R B]
[algebra R C]
[algebra S A]
[algebra S C]
[algebra R S]
[smul_comm_class R S A]
[is_scalar_tower R S A]
[is_scalar_tower R S C]
⦃f g : tensor_product R A B →ₐ[S] C⦄
(ha : f.comp algebra.tensor_product.include_left' = g.comp algebra.tensor_product.include_left')
(hb : (alg_hom.restrict_scalars R f).comp algebra.tensor_product.include_right = (alg_hom.restrict_scalars R g).comp algebra.tensor_product.include_right) :
f = g
a stronger version of ext