Some lemmas about tensor_product #
@[protected]
theorem
tensor_product.ext_iff
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[module R M]
[module R N]
[module R P]
{g h : tensor_product R M N →ₗ[R] P} :
theorem
tensor_product.ext'_iff
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
{g h : tensor_product R (tensor_product R M N) Q →ₗ[R] P} :
@[simp]
theorem
tensor_product.map_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(f : M →ₗ[R] P)
(t : N →ₗ[R] Q)
(x : M)
(y : N) :
@[simp]
theorem
tensor_product.comm_commutes
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[comm_semiring R]
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
{g : tensor_product R M N →ₗ[R] P}
{h : tensor_product R M N →ₗ[R] Q} :
(tensor_product.comm R P Q).to_linear_map.comp (tensor_product.map g h) = (tensor_product.map h g).comp (tensor_product.comm R (tensor_product R M N) (tensor_product R M N)).to_linear_map
theorem
tensor_product.comm_commutes'
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{g : M →ₗ[R] M}
{h : M →ₗ[R] R} :
(tensor_product.comm R M R).to_linear_map.comp (tensor_product.map g h) = (tensor_product.map h g).comp (tensor_product.comm R M M).to_linear_map
theorem
tensor_product.assoc_comp_map
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{M₂ : Type u_4}
{N₂ : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid M₂]
[add_comm_monoid N₂]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R M₂]
[module R N₂]
[module R P]
[module R Q]
(f : M →ₗ[R] P)
(t : N →ₗ[R] Q)
(s : M₂ →ₗ[R] N₂) :
(tensor_product.assoc R P Q N₂).to_linear_map.comp (tensor_product.map (tensor_product.map f t) s) = (tensor_product.map f (tensor_product.map t s)).comp (tensor_product.assoc R M N M₂).to_linear_map
theorem
tensor_product.ext_threefold'
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
{g h : tensor_product R M (tensor_product R N P) →ₗ[R] Q}
(H : ∀ (x : M) (y : N) (z : P), ⇑g (x ⊗ₜ[R] (y ⊗ₜ[R] z)) = ⇑h (x ⊗ₜ[R] (y ⊗ₜ[R] z))) :
g = h
theorem
tensor_product.assoc_symm_comp_map
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{M₂ : Type u_4}
{N₂ : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid M₂]
[add_comm_monoid N₂]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R M₂]
[module R N₂]
[module R P]
[module R Q]
(f : M →ₗ[R] P)
(t : N →ₗ[R] Q)
(s : M₂ →ₗ[R] N₂) :
(tensor_product.assoc R P Q N₂).symm.to_linear_map.comp (tensor_product.map f (tensor_product.map t s)) = (tensor_product.map (tensor_product.map f t) s).comp (tensor_product.assoc R M N M₂).symm.to_linear_map
theorem
tensor_product.comm_map
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(f : M →ₗ[R] P)
(t : N →ₗ[R] Q) :
(tensor_product.comm R P Q).to_linear_map.comp (tensor_product.map f t) = (tensor_product.map t f).comp (tensor_product.comm R M N).to_linear_map
theorem
tensor_product.comm_symm_map
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[add_comm_monoid P]
[add_comm_monoid Q]
[module R M]
[module R N]
[module R P]
[module R Q]
(f : M →ₗ[R] P)
(t : N →ₗ[R] Q) :
(tensor_product.comm R P Q).symm.to_linear_map.comp (tensor_product.map t f) = (tensor_product.map f t).comp (tensor_product.comm R M N).symm.to_linear_map
@[protected]
theorem
tensor_product.map_sum
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid N₁]
[add_comm_monoid N₂]
[module R M₁]
[module R M₂]
[module R N₁]
[module R N₂]
(x : M₁ →ₗ[R] M₂)
{α : Type u_6}
(s : finset α)
(n : α → (N₁ →ₗ[R] N₂)) :
tensor_product.map x (s.sum (λ (a : α), n a)) = s.sum (λ (a : α), tensor_product.map x (n a))
theorem
tensor_product.sum_map
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid N₁]
[add_comm_monoid N₂]
[module R M₁]
[module R M₂]
[module R N₁]
[module R N₂]
{α : Type u_6}
(s : finset α)
(n : α → (N₁ →ₗ[R] N₂))
(x : M₁ →ₗ[R] M₂) :
tensor_product.map (s.sum (λ (a : α), n a)) x = s.sum (λ (a : α), tensor_product.map (n a) x)
@[protected]
theorem
tensor_product.map_smul
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid N₁]
[add_comm_monoid N₂]
[module R M₁]
[module R M₂]
[module R N₁]
[module R N₂]
(x : M₁ →ₗ[R] M₂)
(y : N₁ →ₗ[R] N₂)
(a : R) :
tensor_product.map x (a • y) = a • tensor_product.map x y
theorem
tensor_product.smul_map
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid N₁]
[add_comm_monoid N₂]
[module R M₁]
[module R M₂]
[module R N₁]
[module R N₂]
(x : M₁ →ₗ[R] M₂)
(y : N₁ →ₗ[R] N₂)
(a : R) :
tensor_product.map (a • x) y = a • tensor_product.map x y
theorem
tensor_product.add_map
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid N₁]
[add_comm_monoid N₂]
[module R M₁]
[module R M₂]
[module R N₁]
[module R N₂]
(x y : M₁ →ₗ[R] M₂)
(z : N₁ →ₗ[R] N₂) :
tensor_product.map (x + y) z = tensor_product.map x z + tensor_product.map y z
@[protected]
theorem
tensor_product.map_zero
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{N₁ : Type u_3}
{M₂ : Type u_4}
{N₂ : Type u_5}
[add_comm_monoid M₁]
[add_comm_monoid N₁]
[add_comm_monoid M₂]
[add_comm_monoid N₂]
[module R M₁]
[module R N₁]
[module R M₂]
[module R N₂]
(x : M₁ →ₗ[R] N₁) :
tensor_product.map x 0 = 0
@[protected]
theorem
tensor_product.zero_map
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{N₁ : Type u_3}
{M₂ : Type u_4}
{N₂ : Type u_5}
[add_comm_monoid M₁]
[add_comm_monoid N₁]
[add_comm_monoid M₂]
[add_comm_monoid N₂]
[module R M₁]
[module R N₁]
[module R M₂]
[module R N₂]
(x : M₁ →ₗ[R] N₁) :
tensor_product.map 0 x = 0
theorem
tensor_product.zero_tmul_zero
{R : Type u_1}
[comm_semiring R]
{M : Type u_2}
{N : Type u_3}
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N] :
theorem
tensor_product.map_mul'_commute_iff
{R : Type u_1}
{M : Type u_2}
{N : Type (max u_3 u_4)}
[comm_semiring R]
[non_unital_non_assoc_semiring M]
[non_unital_non_assoc_semiring N]
[module R M]
[module R N]
[smul_comm_class R M M]
[smul_comm_class R N N]
[is_scalar_tower R M M]
[is_scalar_tower R N N]
{f : M →ₗ[R] N} :
(linear_map.mul' R N).comp (tensor_product.map f f) = f.comp (linear_map.mul' R M) ↔ ∀ (x y : M), ⇑f (x * y) = ⇑f x * ⇑f y
theorem
alg_hom.commute_map_mul'
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_semiring R]
[semiring M]
[semiring N]
[algebra R M]
[algebra R N]
(f : M →ₐ[R] N) :
(linear_map.mul' R N).comp (algebra.tensor_product.map f f).to_linear_map = f.to_linear_map.comp (linear_map.mul' R M)
theorem
alg_hom.commute_map_mul'_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_semiring R]
[semiring M]
[semiring N]
[algebra R M]
[algebra R N]
(f : M →ₐ[R] N)
(x : tensor_product R M M) :
⇑(linear_map.mul' R N) (⇑(algebra.tensor_product.map f f) x) = ⇑f (⇑(linear_map.mul' R M) x)
theorem
tensor_product.map_add
{R : Type u_1}
[comm_semiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid N₁]
[add_comm_monoid N₂]
[module R M₁]
[module R M₂]
[module R N₁]
[module R N₂]
(x y : M₁ →ₗ[R] M₂)
(z : N₁ →ₗ[R] N₂) :
tensor_product.map z (x + y) = tensor_product.map z x + tensor_product.map z y